Noyau de système d'exploitation formellement prouvé

Prouver formellement qu’un système d'exploitation est sécurisé et sans failles est un sujet de recherche de plus de 30 ans[1]. En effet, on ne peut être assuré de la sécurité et la fiabilité d’un système informatique uniquement si son système d'exploitation est garantie sans erreur. Il est à noter que le noyau qui est exécuté dans le mode le plus privilégié dans le processeur, à des accès illimités au matériel. Par conséquent, la moindre erreur dans le noyau de l’OS peut compromettre toute la légitimité du reste du système.

Un système d'exploitation, au même titre que n’importe quel code informatique, peut-être converti mathématiquement, et donc, si l’on souhaite s’assurer que celui-ci est sans erreur, il suffit de le prouver.

Il est possible de pousser la robustesse et la sécurité au point de garantir l’absence de bugs ainsi que la présence de très hautes propriétés de sécurités, mais cela avec de très petits noyaux. En effet, il est inévitable d’avoir des erreurs dans un code informatique, par conséquent plus la taille du code est élevée, plus la possibilité d’avoir des erreurs est grande. Évidemment, la réduction parfois radicale de la taille des systèmes d'exploitation peut amener à une forte augmentation de la complexité ainsi qu’à une baisse des performances et des fonctionnalités.

Il y a deux aspects d'un noyau que l'on peut souhaiter vérifier.

Le premier aspect est la sécurité du noyau. Celle-ci comprend la confidentialité des informations auxquelles le noyau a accès, ainsi que l'intégrité du noyau, où quel code peut être exécuté et ce qu'il peut réaliser.

Le second aspect concerne la sûreté du noyau. Pour des applications critiques où la sécurité d'usagers peut être en jeu, comme dans l'aéronautique, il est vital de garantir certaines propriétés. Ces propriétés peuvent être le respect de contraintes temporelles comme un temps de réaction limite à un événement extérieur[2].

Il faut tout d'abord noter que la Vérification de modèles ne travaille pas directement sur le noyau du système d'exploitation. Dans un premier temps, il faut formaliser le noyau sous forme de modèle. En effet, le but de la Vérification de modèles va être d'explorer de manière exhaustive ce modèle afin de vérifier que le noyau supporte n'importe quel état qui peut se présenter. C'est-à-dire, peu importe l'erreur qui va survenir, cela ne fera pas planter l'OS.

De ce fait, Vérification de modèles n'est pas une méthode qui pourra être efficace sur des noyaux d'OS modernes vu qu'ils sont assez volumineux en taille : cela prend énormément de temps. On va plutôt l'utiliser sur des noyaux de petite taille, essentiellement des micronoyaux.

On va plutôt utiliser cette méthode pour vérifier certaines règles de sécurité ou bien des propriétés bien précises. De plus, vu qu'il a fallu transposer le noyau sous forme de modèle, ce qui est fait généralement fait manuellement, cela prend du temps et est sujet à erreurs.

Certains outils comme SLAM, peuvent travailler directement sur le noyau, mais ils ne peuvent vérifier que de simples propriétés, or cela n'est pas suffisant pour prouver que le système est correct.

En conséquence, Vérification de modèles n'est pas une méthode qui est souvent utilisée.

Contrairement à la Vérification de modèles, le but de theorem proving va être d'exprimer les propriétés du noyau et son modèle de façon logique. Ensuite, on va en déduire une preuve mathématique et vérifier qu'elle confirme ces propriétés.

Cette méthode a de grands avantages par rapport à la Vérification de modèles :

• La taille du noyau ne compte pas vu qu'une preuve mathématique peut gérer de très grands nombres. On peut donc appliquer cette méthode sur tous types d'OS : en particulier les plus complexes et les plus fonctionnels.
• Via cette méthode, la vérification des preuves mathématiques peut se faire de manière automatique : peu importe que cette preuve soit compliquée à résoudre pour un humain, un model checker peut le faire sans soucis.

À noter que comparée à la Vérification de modèles, cette méthode requiert plus d'interaction humaine, mais cela peut justement être sa force : cela permet de savoir que le système est correct mais aussi pourquoi.

La preuve par le code (en) (en anglais, PCC pour Proof-carrying code), est un framework pour les mécanismes de vérification des langages de programmation.

Dans la même logique que le theorem proving, la PCC créée et vérifie une preuve mathématique mais à partir du langage de programmation lui-même.

Se trouve deux types de PCC :

• PCC conventionnel
• PCC fondationnel

Le point négatif de cette méthode est qu'il ne doit pas y avoir d'erreurs dans l'outil de vérification.

Les critères communs (CC ou Common Criteria for Information Technology Security Evaluation, version anglophone) sont reconnus mondialement comme un standard pour la sécurité informatique depuis 1999[3], et cela a attisé l’intérêt des chercheurs pour les méthodes formelles ces dernières années.

Ils remplacent les standards précédents : ITSEC (Europe) et TCSEC (États-Unis). Ils sont reconnus par 24 pays et administrés par les autorités locales de ces pays.

Au niveau de la validation, les CC sont plus orienté produit et moins orientées procédures que les anciens standards. Ils distinguent les responsabilités des développeurs de celle des évaluateurs[4]. Cela dit, ils représentent une forte avancée vers la sécurité des produits informatiques.

Il y a 7 niveaux d'évaluations (EALs ou Evaluation Assurance Levels, version anglophone) dans les CC ou le niveau 7 est le plus élevé. Ces niveaux définissent un niveau de qualité des produits, mais surtout assure une très forte rigueur dans la mise en place des mesures de sécurité des produits informatiques.

En ce qui concerne les noyaux d'OS, le niveau de sécurité le plus haut atteint est le niveau 6, la majorité atteint généralement le niveau 4. À noter que le nombre de noyaux ayant atteint ce niveau est extrêmement faible. Parmi eux, nous allons trouver :

Cependant, bien que les méthodes de vérification formelles assurent une haute fiabilité, une vérification au niveau du code n'est pas requise par les critères communs[4].

De plus, les critères communs sont considérés consommé étant trop coûteux, produisent trop de paperasse et adhèrent à un modèle de procès légal

Les outils de preuve formelle mécanisée (vérifiée par ordinateur) ne sont pas encore aussi pratiques à utiliser qu'ils le pourraient, donc faire une preuve formelle complète c'est un travail très important. Coq est un outil basé sur l'idée qu'un système de typage suffisamment puissant peut aussi devenir un système de preuve. On peut donc écrire des preuves et des programmes dans un même langage (mais est donc très contraignant pour la programmation), et il y a aussi un langage spécialisé pour écrire des preuves automatisées, c'est-à-dire en fait écrire un petit programme qui trouve tout seul la preuve, au lieu de construire directement l'arbre de preuve[5].

Il existe d'autres outils de preuve formelle, Twelf en particulier est réputé pour être un peu plus facile à utiliser (et, en contrepartie, un peu plus restreint et moins généraliste).

Haskell est un outil pour développer simultanément une spécification du noyau et une implémentation de référence pour l'évaluation et le test. La mise en œuvre peut être utilisée en conjonction avec un simulateur pour exécuter un binaire d'application réelles, tandis que la spécification génère une entrée à un probateur de théorème interactif pour la preuve formelle de propriétés. La spécification Haskell sert de support pour le prototypage itératif de la mise en œuvre ainsi que pour le modèle de système pour les équipes de modélisation de noyau et formelles, c'est-à-dire que la spécification Haskell forme un pont entre les équipes améliorant le flux d'idées, avec une faible barrière d'entrée pour les deux. De plus, l'implémentation de référence, lorsqu'elle est couplée à un simulateur, peut être utilisée pour exécuter des binaires natifs[6].

ImProve est un langage impératif simple avec des affectations variables et des énoncés conditionnels. Les assertions ImProve sont vérifiées formellement en utilisant la vérification de modèle SMT. Pour la mise en œuvre et la simulation du système, ImProve compile vers C, Ada, Simulink et Modelica. TLC est un outil adapté pour la spécification de réactif systèmes. Le comportement d'un réactif système est décrit par une spécification formelle, et les propriétés, sont exprimées par TLC[7].

Design et méthode de prototypage rapide de SeL4

Il fait partie de la famille des micronoyaux. Il adopte une approche de partitionnement qui fournit une forte isolation totale d’applications. Il a subi la Worst Case Execution Time, cette dernière devenue indispensable dans la vérification des systèmes, a essayé de tester les limites du Sel4[8].

Le Sel4 comporte 10 000 lignes de code, exécutable sur différentes plateformes : X86 et ARM. L' avantage du Sel4 est qu’il fournit le partitionnement nécessaire pour soutenir des logiciels mixtes[9].

La sécurité et la fiabilité d'un système informatique ne peuvent être aussi bonne que celle du système d'exploitation (OS). Le noyau, défini comme la partie du système s'exécutant dans les zones les plus profondes du processeur, dispose d'un accès illimité au matériel.

Par conséquent, tout défaut dans la mise en œuvre du noyau risque de compromettre le bon fonctionnement du reste du système.

Il est évidemment inévitable d'avoir des bogues dans un code important. En conséquence, lorsque la sécurité ou la fiabilité est primordiale, l'approche habituelle est de réduire la quantité de code privilégié, afin de minimiser l'exposition aux bugs. C'est l'une des principales motivations derrière les noyaux de sécurité et les noyaux de séparation, l'approche MILS, les microkernels et les kernels d'isolement, l'utilisation de petits hyperviseurs comme base de confiance minimale, ainsi que les systèmes qui exigent l'utilisation de langage de type sécurisé Tous les codes, à l'exception d'un noyau sale. De même, le critère commun au niveau d'évaluation le plus strict exige que le système sous évaluation ait une conception simple.

Avec des noyaux vraiment petits, il devient possible de renforcer la sécurité et la robustesse, au point où il est possible de garantir l'absence de bugs. Ceci peut être réalisé par une vérification formelle vérifiée par machine, fournissant une preuve mathématique que la mise en œuvre du noyau est conforme à sa spécification et exempte de défauts de mise en œuvre induits par le programmeur.

seL4 est le tout premier noyau OS à finalité générale qui est entièrement vérifié pour la correction fonctionnelle. En tant que tel, c'est une plate-forme de fiabilité sans précédent, qui permettra la construction de systèmes hautement sécurisés et fiables sur le dessus.

La propriété fonctionnelle correcte que nous prouvons pour seL4 est beaucoup plus forte et plus précise que ce que les techniques automatisées telles que la vérification de modèles, l'analyse statique ou les implémentations du noyau dans des langages de type sécurité peuvent atteindre. Nous analysons non seulement les aspects spécifiques du noyau, tels que l'exécution sûre, mais aussi fournir une spécification complète et la preuve du comportement précis du noyau[10].

Il y a cependant une limite à la portée de la preuve d'un noyau. La preuve de l'"exactitude" d'un noyau est valide si les axiomes sur lesquels elle repose sont valides.

Parmi ces axiomes, il peut y avoir le bon fonctionnement du matériel qui exécutera le noyau[11].

Une possibilité est alors d'exécuter le noyau sur un matériel qui ne valide pas les axiomes sur lesquels a été fondée la preuve pour tenter d'attaquer le noyau. Il est aussi possible de provoquer des fautes dans celui-ci, par exemple en causant une surchauffe, et d'en extraire des informations. Un dernier exemple serait d'exploiter des spécificités du matériel qui n'ont pas été couvertes par la preuve pour permettre des attaques par canaux auxiliaires. Un exemple serait que les timings du matériel ne soient pas considérés dans la vérification et que celle-ci ne puisse garantir l'absence de canal caché, qui pourrait permettre de véhiculer des informations.

La compréhension de la spécification du noyau peut également être attaquée. Cela peut mettre en évidence des comportements du noyau qui n'avaient pas été interprétés.

Un aspect évident de la vérification est le coût de la preuve, cela dépend évidemment la nature du changement, en particulier la quantité de code qu'il modifie, le nombre d'invariants qu'il applique et son degré de localisation[12].

Depuis les premières tentatives de vérification du noyau, il y a eu des améliorations spectaculaires dans la puissance des outils de démonstration de théorèmes disponibles. Des assistants de vérification comme ACL2 (en), Coq, PVS, HOL et Isabelle ont été utilisés dans un certain nombre de vérifications réussies, allant des mathématiques et des logiques aux microprocesseurs, aux compilateurs et aux plateformes de programmation complètes comme JavaCard.

Cela a entraîné une réduction significative du coût de la vérification formelle et une diminution du seuil de faisabilité. En même temps, les avantages potentiels se sont accrus, donnés par exemple le déploiement accru de systèmes embarqués dans des situations critiques ou de vie ou les énormes enjeux créés par la nécessité de protéger les droits de propriété intellectuelle évalués à des milliards[13].