Location via proxy:   [ UP ]  
[Report a bug]   [Manage cookies]                
Aller au contenu

CertiKOS

Ajouter des liens
Un article de Wikipédia, l'encyclopédie libre.

CertiKOS est un projet développé par Zhong Shao, professeur à l'Université de 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 Coq) 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

[modifier | modifier le code]

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[1]. International Data Corporation (IDC) rapporte qu'il s'est vendu près de 355.2 millions de smartphones dans le monde, au 3e trimestre 2018[2], 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[3]. 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[4]. 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[5], ou même à des interactions avec d’autres logiciels[6]. 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é[7] (voir liens externes: "Bulletins d'informations, failles de sécurité"[8],[9],[10],[11],[12],[13],[14],[15],). 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[1]. 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"[16]. 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.»[17]. Ces derniers ont notamment été les premiers à produire une preuve de correction fonctionnelle pour un micro-noyau[18],[19]. 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[20]. 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[20],[21]. CertiKOS cherche également à produire un noyau certifié, capable de prendre en charge la simultanéité et des machines multi-cœurs[22].

La philosophie de Certikos

[modifier | modifier le code]

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

[modifier | modifier le code]
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[23],[24]. L'équipe de seL4[17] a été la première à construire une preuve de correction fonctionnelle, pour un micro-noyau[18],[19]. CertiKOS s'y emploie aussi, notamment à l'aide de l'assistant de preuve de Coq et à la définition d'un raffinement contextuel fort[25],[26].

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[27],[28].

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)[18],[29]. 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[30].

Spécifications profondes

[modifier | modifier le code]

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[31]. 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.

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[31],[20].

Il possible de représenter le concept de spécification avec les exemples suivants :

  • une spécification simple: L’eau pure bout à 100 °C.
  • approche en spécification profonde : L’eau pure bout à 100 °C à une pression atmosphérique de 1,013 bar.

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[18],[20]. 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[18].

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

[modifier | modifier le code]

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[17]. Tout langage de programmation constitue en soi une couche d’abstraction car il n’est pas directement interprétable par la machine.

Afin de certifier cette nouvelle couche d’abstraction, pour assurer le bon fonctionnement d'un [noyau, il faut donc certifier que les lignes de codes vont pouvoir être compilées correctement, de manière à n'engendrer aucun bug. C’est dans ce but que CertiKOS fait appel à CompCertX «CompCert eXtended», développé par Gu et al[32],[33] et basé sur CompCert[34]. L'utilisation de CompCert ne permet pas de prouver l'exactitude de la compilation des couches individuelles ou des modules utilisés par CertiKOS. Ce dernier ne peut le faire que pour des programmes entiers. C’est pourquoi, il a été adapté[18].

CompCertX implémente ClightX (une variante du langage source de CompCert, Clight) et un langage assembleur, LAsm. La sémantique opérationnelle de CompCertX, comme CompCert, est donnée par des relations de transition en petites étapes, disposant d'états initiaux et finaux. Cependant, s’agissant de couches individuelles ou de modules, et non de programmes entiers, la définition de ces états a dû être adaptée. Pour l’état initial par exemple, CompCertX prend la mémoire initiale, la liste des arguments et le pointeur de la fonction à appeler comme paramètres. Pour l'état final, c’est la valeur de retour et l'état de la mémoire, lorsque nous quittons la fonction, qui servent de paramètres. L’état final de la mémoire est observable car il est renvoyé à l’appelant. Ainsi dans CompCertX, il est nécessaire dans les diagrammes de simulation de prendre en compte les transformations de la mémoire, lors de la mise en relation des états finaux[32].

La Certification des couches d'abstraction dans CertiKOS est gérée et délivrée par CompCertX (du code source à l’assemblage). Cependant l'assembleur CompCertX permettant de convertir un assemblage en code machine, n'est pas vérifié. L’exactitude du vérificateur d’épreuve Coq et de son mécanisme d’extraction de code, est supposée[35].

Implémentation de CertiKOS

[modifier | modifier le code]

Au travers d'un Hyperviseur Certifié

[modifier | modifier le code]

Avec le développement important des solutions de stockage et d'hébergement de type Cloud (Amazon EC2, Salesforce CRM, Rackspace), il devenait de plus en plus important de sécuriser ces données afin que les clients puissent avoir confiance en ces solutions. Cependant, il était complexe de certifier qu'un hyperviseur était 100% sécurisé, de par sa complexité et sa taille. Il était donc impossible de certifier et garantir que son fonctionnement serait correct[36].

L'une des premières faille de sécurité dans un environnement cloud est le logiciel de management en lui-même[37]. En effet, ce logiciel permet de faire de l'allocation et de la révocation de ressources sur les serveurs mis à disposition pour héberger les données, et celui-ci peut donc éventuellement avoir accès aux informations que se trouvent sur les serveurs.

Le logiciel de gestion du fournisseur utilise les interfaces de délégation du noyau approuvé pour allouer et révoquer des ressources conformément à la politique du fournisseur. À son tour, le noyau approuvé met à jour ses enregistrements de propriété afin de restreindre de manière appropriée l'accès aux ressources de chaque domaine non approuvé à l'aide de techniques de protection et de virtualisation standard.

Allocation des ressources avec un hyperviseur certifié

Allocation, Gestion et Révocation des ressources selon l'Hyperviseur CertiKOS

  • Allocation CPU :

CertiKOS alloue les ressources de la CPU de manière spatiale, à la granularité de base. Lors de la première ébauche de CertiKOS, un Cœur du CPU était affecté à un invité. Par la suite, l'hyperviseur CertiKOS a été ajusté afin de rendre l'allocation CPU plus flexible. CertiKOS fournit des interfaces pour le logiciel de gestion permettant d'allouer des cœurs de processeur aux clients et de les révoquer.

  • Allocation RAM et Disques :

CertiKOS extrait à la fois la RAM et les disques en tant qu'espace mémoire pour les logiciels de gestion non fiables et les invités. Le noyau ne comprend aucun système de fichiers, laissant cette fonctionnalité au logiciel invité non approuvé. CertiKOS expose uniquement les interfaces prenant en charge la délégation et l’accès protégé à la mémoire et au stockage sur disque.

  • Allocation Interfaces :

CertiKOS présente des interfaces permettant au logiciel de gestion du fournisseur de donner aux clients un accès à l’infrastructure de réseau partagé du fournisseur. La conception actuelle suppose que le matériel du serveur fournit suffisamment de cartes réseau physiques et / ou de cartes réseau virtualisées pour dédier au moins une carte réseau à chaque client sans multiplexage logiciel. CertiKOS pourrait être amélioré à l’avenir pour fournir son propre multiplexage dynamique des interfaces réseau, mais ce n’est pas une priorité absolue, car la virtualisation de la carte réseau basée sur le matériel devient de plus en plus courante et peu coûteuse.

Au moment de l'exécution, CertiKOS utilise ses enregistrements de propriété pour vérifier l'autorisation sur toutes les demandes d'accès explicites et pour configurer des mécanismes de protection basés sur le matériel, tels que le matériel MMU et IOMMU. De cette manière, CertiKOS applique l'isolation des ressources entre les applications et évite les fuites d'informations.

Au travers d'un Noyau Certifié: mCertiKOS, mC2

[modifier | modifier le code]

Une fois l'Hyperviseur développé, les chercheurs se sont confrontés à quelques difficultés. En effet, leur hyperviseur n'était pas forcément adapté à un noyau standard Linux ou autre. Cela rendait donc l'utilisation de l'hyperviseur obsolète. Ils ont alors décidé de développer entièrement un noyau (Kernel), allegé par rapport à un noyau Linux, mais permettant de valider le bon fonctionnement de leur hyperviseur. De plus, pour développer ce noyau, ils ont également utilisé les méthodes de Certification, de telle sorte que le noyau soit également vérifié et que l'hyperviseur donne un rendement optimal.

Grâce à sa sémantique de composition de couches, CertiKOS a débouché sur plusieurs noyaux certifiés, dont les plus aboutis sont mCertikos et mC2. Mc2 est capable de prendre en charge des machines multi-cœurs et la simultanéité, ainsi que l’entrelacement d’exécution de modules noyau et utilisateur, sur différentes couches d'abstraction[32],[22]. Le noyau mC2 est une évolution de mCertikos développé à l’origine, dans le cadre d’un vaste projet de recherche, financé par la DARPA, pour des véhicules terrestres sans pilote[38]. Ce dernier est pensé de manière séquentielle, en 4 modules totalisant 28 couches d’abstraction certifiées pour sa version basique, et de 5 modules totalisant 37 couches d’abstraction certifiées pour sa version avec hyperviseur[39]. Chaque couche est compilée et certifiée par CompCertX. Ce noyau représente 3 000 lignes de code et permet de démarrer un système Linux.

Découpage des modules des noyaux mCertiKOS

En partant de mCertikos, et en y ajoutant différentes fonctionnalités (modules), telles que la gestion de la mémoire dynamique, la prise en charge des conteneurs pour le contrôle de la consommation de ressources, la prise en charge de la virtualisation du matériel Intel, la mémoire partagée IPC, verrous IPC, ticket et MCS synchrones (un spinlock par exclusion mutuelle) (etc..)[40], Certikos a fait naitre mC2.

Le noyau mC2 est quant à lui, une version plus évoluée, qui comprend 6 500 lignes d’assemblage C et x86. Il prouve que l'exactitude fonctionnelle d'un noyau de système d'exploitation simultané complet et polyvalent, avec un verrouillage à grain fin (MCS), est possible[22].

Le noyau mC2 comprend un socle fondamental de spécifications réduit, afin de simplifier le processus de révision et de limiter les erreurs. Ce socle représente près de 1 400 lignes, dont 943 lignes pour les couches les plus basses, constituant la théorie axiomatique de la machine physique, et 450 lignes pour les interfaces d'appel système abstraites. En dehors de ce socle, des spécifications supplémentaires existent : 5 246 lignes, pour les différentes fonctions du noyau et près de 40 000 lignes, pour définir différents théorèmes, lemmes, et invariants[41].

CertiKOS a permis de prouver la propriété de raffinement contextuel de son noyau mC2, par rapport à une spécification profonde de haut niveau. Ce raffinement est défini de la façon suivante : pour tout programme (P), l’interaction du noyau (K) et de P, dans la sémantique de la machine x86, implique le même comportement que P dans la sémantique de la machine mC2: ∀P, [ [P⋉K] ]x86 ⊆ [ [P] ]mC2[42]. La propriété d’équivalence de comportement pour P est donc dérivable. Toutes les interruptions et les appels système suivent strictement les spécifications de haut niveau. Ils sont toujours exécutés en toute sécurité (et se termine éventuellement) comme l'indique cette propriété de correction fonctionnelle. Il n'y a pas de dépassement de mémoire tampon, pas d'attaque par injection de code, de dépassement d'entier ou d'accès de pointeur nul, etc[43].

Le noyau mC2 n'est pas encore aussi complet qu'un système Linux. Il manque actuellement d'un système de stockage certifié. De plus, il s'appuie sur un chargeur de démarrage qui initialise les CPU et les périphériques qui n'est pas encore vérifié[43].

Références

[modifier | modifier le code]
  1. ↑ a et b LinuxFoundation 2017, p. 3
  2. ↑ Auffray 2018, p. 1.
  3. ↑ TMR 2018, p. 1.
  4. ↑ Shao 2016, p. 653.
  5. ↑ Toyota 2013, p. 1.
  6. ↑ Dennis Burke All Circuits are Busy Now: The 1990 AT&T Long Distance Network Collapse.
  7. ↑ Kalagiakos 2012, p. 6.
  8. ↑ US-CERT et 2018 VMware-Releases-Security-Updates.
  9. ↑ US-CERT et 2018 Microsoft-Releases-November-2018-Security-Updates.
  10. ↑ US-CERT et 2018 Cisco-Releases-Security-Updates.
  11. ↑ US-CERT et 2018 Apple-Releases-Security-Updates-iCloud-iOS.
  12. ↑ US-CERT et 2018 Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors.
  13. ↑ FR-CERT et 2018 Multiples vulnérabilités de fuite d’informations dans des processeurs.
  14. ↑ FR-CERT et 2018 Vulnérabilité dans Wallix AdminBastion.
  15. ↑ FR-CERT et 2018 Multiples vulnérabilités dans le noyau Linux d’Ubuntu.
  16. ↑ Dijkstra 1979, p. 6.
  17. ↑ a b et c Klein 2009, p. 207
  18. ↑ a b c d e et f Gu 2015, p. 596-2
  19. ↑ a et b Shao 2016, p. 666
  20. ↑ a b c et d Shao 2016, p. 655
  21. ↑ De Millo 1979, p. 279.
  22. ↑ a b et c Shao 2016, p. 654
  23. ↑ Guithub Le théorème des quatre couleurs et les preuves informatisées.
  24. ↑ CNRS Un ordinateur pour vérifier les preuves mathématiques.
  25. ↑ Shao 2016, p. 607.
  26. ↑ Appel 2016, p. 2.
  27. ↑ Gu 2015, p. 595-1.
  28. ↑ Pierce 2016, p. 1.
  29. ↑ Shao 2016, p. 654-2.
  30. ↑ Shao 2016, p. 658.
  31. ↑ a et b Gu 2015, p. 595
  32. ↑ a b et c Gu 2015, p. 604
  33. ↑ Shao 2016, p. 656.
  34. ↑ The CompCert C verified compiler 2018, p. 1.
  35. ↑ Shao 2016, p. 657-5.
  36. ↑ Vaynberg2011 2011, p. 4.
  37. ↑ Vaynberg2011 2011, p. 2.
  38. ↑ Shao 2016, p. 656-657.
  39. ↑ Gu 2015, p. 596.
  40. ↑ Shao 2016, p. 663.
  41. ↑ Shao 2016, p. 664.
  42. ↑ Shao 2016, p. 655-655.
  43. ↑ a et b Shao 2016, p. 657

Bibliographie

[modifier | modifier le code]

Liens externes

[modifier | modifier le code]

Bulletin d'information : failles informatiques https://www.us-cert.gov/ https://www.cert.ssi.gouv.fr

v · m
Apple
Mac OS Classic
Dérivés de NeXTSTEP
Dérivés de BeOS
DOS
IBM
Microsoft Windows
Fondés sur MS-DOS
Branche NT
ReactOS Foundation
Branche NT (GPL/LGPL/AGPL) non-Microsoft
POSIX / Unix
AT&T / Laboratoires Bell
BSD
GNU Hurd
Linux (liste)
Autres dérivés
Dérivés d'AmigaOS
Dérivés du TOS
D’importance historique
Mobile
Noyau Linux
Autres noyaux
Embarqués
Pour capteur en réseau
Pour carte à puce
Temps réel
Autres systèmes
Pour une liste complète, voir la liste des systèmes d’exploitation et la catégorie « Système d’exploitation ».
Ce document provient de « https://fr.wikipedia.org/w/index.php?title=CertiKOS&oldid=212292887 ».