CertiKOS est un projet développé par Zhong Shao, professeur à l'université Yale, dans le Connecticut, avec la participation d'une équipe de 6 autres chercheurs. CertiKOS (Certified Kit Operating System) est un outil méthodologique de conception et de développement de systèmes d’exploitation certifiés. Son approche se fait autour de la définition et la Certification de couches d'abstraction, elles-mêmes basées sur la sémantique de spécification riche (spécifications profondes). Ces procédés répondent à ce qui peut être considéré comme une loi fondamentale, un raffinement contextuel fort. Cette méthodologie permet non seulement de certifier toute la sémantique (par l'assistant de preuve de Rocq) mais également de certifier la compilation grâce à l'utilisation de CompCertX. CertiKOS permet de développer un hyperviseur et plusieurs noyaux certifiés, dont mC2. Ce dernier prenant en charge des processeurs multi-cœurs, ainsi que l'exécution entrelacée de modules noyau / utilisateur sur différentes couches d'abstraction (la simultanéité) .
Motivations et enjeux Les noyaux, systèmes d’exploitation, hyperviseurs (etc.) sont des logiciels/programmes, une succession de lignes de code, qui une fois compilée et interprétée par la machine, rend un service à l’utilisateur. Ils se retrouvent aujourd'hui dans nos smartphones, voitures, drones, ordinateurs, avions, systèmes bancaires ou domotiques... Selon le rapport 2017 de The Linux Foundation, le Système d'exploitation Linux exécute près de 90 % de la charge de travail du cloud public, couvre 62 % de la part de marché de la technologie embarquée et 99 % de celle des superordinateurs. Il est présent sur 82 % des smartphones. International Data Corporation (IDC) rapporte qu'il s'est vendu près de 355.2 millions de smartphones dans le monde, au trimestre 2018, soit près de 45 smartphones par seconde. L'impact est donc important mais l'enjeu financier est également présent. À titre d'exemple, selon The Transparency Market Research (TMR), le marché des systèmes embarqués dans le monde, qui pesait près de 153 milliard de dollars en 2014, pourrait passer à près de 223 milliard dollars en 2021. L’omniprésence et la dépendance croissante de nos sociétés modernes à ces différents systèmes, rendent incontournable l'élaboration des logiciels fiables et sécurisés.
Les systèmes d'exploitation constituent l'épine dorsale des systèmes logiciels et des éléments particulièrement critiques, pour la sécurité dans le monde. En effet, ces systèmes ne permettent pas toujours à la machine de rendre le service pour lequel ils sont conçus. Cela peut être dû à des défauts d’écriture dans le code, des défauts de conception, ou même à des interactions avec d’autres logiciels. Ces défauts peuvent donner lieu à des bugs. L'exploitation de certains de ces défauts peut également permettre à des tiers d'en détourner l'usage pour récupérer des données et nuire au fonctionnement des systèmes. Ces défauts constituent alors des failles de sécurité (voir liens externes: "Bulletins d'informations, failles de sécurité"). Ces défauts sont mis en exergue par une vérification du code, leur correction se fait par l'intermédiaire de patchs correctifs. Cette solution triviale implique de passer en revue chaque ligne de code et de tester tous les scénarios possibles. Bien que cette solution soit réalisable, elle devient très vite fastidieuse et exponentielle au fil de l’accumulation des lignes de code. À titre d'exemple, le noyau Linux Version 4.13 contient 24.766.703 de lignes de codes. Selon Edsger W. Dijkstra, "Les tests de programme peuvent être utilisés pour montrer la présence de bugs, mais jamais pour montrer leur absence". L’alternative réside en une vérification par méthode formelle (déductive). Selon les contributeurs de seL4 « Une vérification formelle complète est le seul moyen connu de garantir qu'un système est exempt d'erreurs de programmation.». Ces derniers ont notamment été les premiers à produire une preuve de correction fonctionnelle pour un micro-noyau. CertiKOS se positionne ouvertement dans cette optique, afin de certifier un système d'exploitation, plutôt que d’en faire une vérification triviale. Cependant, il ne se focalise pas sur cet unique objectif. Il tente d'offrir la meilleure méthodologie pour concevoir et développer des systèmes d'exploitation performants, fiables et sûrs. CertiKOS cherche également à produire un noyau certifié, capable de prendre en charge la simultanéité et des machines multi-cœurs.
La philosophie de Certikos Le système d’exploitation, ou OS (Operating System), est un ensemble de programmes faisant l'interface entre le matériel de l'ordinateur et les programmes utilisateurs. Il constitue la colonne vertébrale d'un système informatique. Ce système est construit et repose sur la base d'un noyau (Kernel en Anglais), qui gère les ressources matérielles. Ce dernier offre des mécanismes d'abstraction entre les logiciels et les matériels.
La certification d’un programme consiste à prouver, sur la base d’une méthode formelle, que le programme effectue, sans se tromper et dans tous les cas possibles, la tâche qui lui est confiée. Cette méthode repose sur une analyse statique du programme, permettant de raisonner rigoureusement afin de démontrer la validité d’un programme par rapport à ses spécifications. Le raisonnement se fait sur la sémantique du programme.
Certification du Noyau vignette|440x440px|Représentation du principe de raffinement contextuel de CertiKOS CertiKOS a pour objectif de certifier un système d'exploitation. Cette notion est basée sur la prouvabilité de la vérification par machine, de manière explicite et formelle. Cet effort de preuve est d'autant plus compliqué, au regard porté sur la qualité de la preuve et du risque de la controverse. L'équipe de seL4 a été la première à construire une preuve de correction fonctionnelle, pour un micro-noyau. CertiKOS s'y emploie aussi, notamment à l'aide de l'assistant de preuve de Rocq et à la définition d'un raffinement contextuel fort.
La méthodologie de CertiKOS intervient dès l'étape de conceptualisation du système et cherche notamment à définir des spécifications précises, donnant lieu à des comportements observables. Ces spécifications sont transformées en formules logiques. En prouvant de manière mathématique ces formules, on est alors en mesure de certifier le programme. L'utilisation de Certikos vise à définir des spécifications riches et détaillées, en s'appuyant sur la notion de spécifications profondes, à travers une superposition de différentes couches d'abstraction logiques.
Le raffinement contextuel de CertiKOS indique que l’implémentation de chaque fonction du noyau, se comporte comme sa spécification dans toute interaction entre le noyau et le programme (contexte utilisateur). Ainsi, en considérant K pour le noyau, P pour le programme et S pour la spécification fonctionnelle du noyau, la combinaison des codes de K et P affine S et P. CertiKOS cherche à décomposer la vérification de l'OS en plusieurs sous tâches, plus petites et elles-mêmes contrôlables, sur la base de leurs spécifications profondes. C’est donc la Certification de ces différentes couches d’abstraction, qui permettent de certifier l’OS. La définition du raffinement contextuel dans CertiKOS est définie de la façon suivante: prenons L0 et L1 comme deux interfaces (couches d’abstraction) et P pour un programme. L0 affine contextuellement L1, si et seulement si pour tous P, P est valide sur L1, peu importe la configuration. Le raffinement contextuel implique également que pour tous P, P est valide sur L1, peu importe la configuration, et que tout comportement observable de P sur L0, sous certaines configurations, est également observé sur L1, peu importe la configuration.
Spécifications profondes Les systèmes d'exploitation constituent une multitude de superposition de couches d'abstraction: noyaux (Kernel), pilotes (Drivers ), Hyperviseurs (etc..). Chacune de ces couches constituent une interface, qui masque les détails de mise en œuvre d'un ensemble de fonctionnalités de la couche sous-jacente. Les programmes clients construits au-dessus de chaque couche peuvent être compris uniquement en fonction de leurs interfaces et indépendamment de l'implémentation de la couche. Malgré leur importance évidente, les couches d'abstraction ont été généralement traitées comme un concept de système; elles n'ont presque jamais été formellement spécifiées ou vérifiées. Cela rend difficile l'établissement de propriétés de corrections fortes et la mise à l'échelle de la vérification de programmes, sur plusieurs couches. L’importance de définir précisément les spécifications fonctionnelles des différentes couches d’abstraction, est intimement liée à la Certification de ces dernières. alt=|vignette|515x515px|Vulgarisation de l'indépendance d'implémentation de la Spécification Profonde Cependant il s’agit de certifier un ensemble, donc de prendre en compte les relations entre les couches. C’est pourquoi CertiKOS définit des spécifications plus riches, les spécifications profondes. Ces spécifications prennent en compte l’implémentation sous-jacente, en capture les fonctionnalités précises mais aussi, les effets éventuels de l’implémentation sur ses contextes clients.
Il possible de représenter le concept de spécification avec les exemples suivants : une spécification simple: L’eau pure bout à . approche en spécification profonde : L’eau pure bout à à une pression atmosphérique de .
Cet exemple illustre, de manière simple, l’aspect détaillé de la spécification profonde. L’objectif de la richesse des détails de la spécification profonde, est de capturer précisément les comportements observables dans le contexte d'implémentation mais indépendamment de celui-ci. Prenons deux implémentations (par exemple, M1 et M2) de la même spécification profonde (par exemple, L), elles doivent avoir des comportements contextuellement équivalents. Cette propriété d'indépendance d'implémentation des spécifications profondes rend possible la vérification modulaire des propriétés de correction, à l'instar des spécifications de type ou de programmation par contrat.
Indépendance d'implémentation de la Spécification Profonde (tentative de vulgarisation) : Considérons le système de freinage (pédale de freins) d’une voiture comme une interface (L1), entre le conducteur (P) et les plaquettes de frein (Interface L0). R, traduisant la relation contextuelle entre L1 et M(1 et 2), est représenté par la pression de la pédale. La spécification profonde de l’interface L1 est l’ABS, M1 (module noyau qui implémente l’interface L1 sur la base de sa spécification) est une voiture Citroen C1. Enfin, M2 (module noyau qui implémente l’interface L1 sur la base de sa spécification) est une voiture Citroen C3. M1 et M2 auront en fonction la pression de P sur le frein, avec la possibilité du déclenchement de l’ABS.
Certification du code informatique: CompCertX CertiKOS s’emploie à concevoir des micronoyaux car leurs vérifications est par essence moins lourde. Les noyaux de systèmes d'exploitations ne sont, ni plus ni moins, que des programmes informatiques écrits dans un langage de programmation C et/ou en langage de programmation assembleur. Tout langage de programmation constitue en soi une couche d’abstraction car il n’est pas directement interprétable par la machine.