CertiKOS

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

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.

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

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.

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