Un noyau de système d'exploitation formellement prouvé (ou , terme anglophone) est un noyau pour lequel on a prouvé de façon mathématique que celui-ci ne possédait aucun défaut de conception. Cette vérification dite « formelle » est définie en fonction de plusieurs critères appelés critères communs.
L’idée de la vérification formelle des systèmes d'exploitation apparaît dans les années 1970. Avec l'énoncé de la correspondance de Curry-Howard, les programmes informatiques peuvent être définis formellement comme des objets mathématiques. La preuve de correction de ces programmes, équivalente à une preuve d'un théorème mathématique, devient alors possible. Pour pouvoir prouver de manière automatique, il est nécessaire de disposer d'une spécification formelle du comportement attendu du programme.
Plusieurs méthodes existent afin de prouver formellement que ces noyaux sont sans erreurs. On peut citer la Vérification de modèles ou la Démonstration automatique de théorèmes. Mais ces méthodes seules ne suffisent pas. Elles sont complétées par des outils de vérification comme Spin ou ComFoRT , qui sont des "model checkers", ou par des langages formels comme Haskell ou Rocq. À cette fin, différents critères doivent être respectés. En fonction du nombre de critères validés, un niveau d’assurance est donné au noyau. Plus le niveau est élevé, plus le noyau est garanti.
Historiquement, le premier système d'exploitation formellement prouvé est le sel4. Ce projet a été complété en 2009. Il s’agit d’un micronoyau de la famille L4 conçu pour offrir des mécanismes de sécurité forts tout en conservant une haute performance.
Prouver qu’un système d'exploitation est formellement correct vise à offrir une garantie de fiabilité en démontrant que son noyau peut résister à de nombreuses situations. La vérification formelle d’un système d'exploitation est encore en développement et fait l'objet de travaux de recherche.
Généralités
Définitions Système d'exploitation
Prouver formellement qu’un système d'exploitation est sécurisé et sans failles est un sujet de recherche de plus de 30 ans: la sécurité et la fiabilité d’un système informatique ne sont assurées que si son système d'exploitation est sans erreur. Le noyau, qui est exécuté dans le mode le plus privilégié du processeur, a des accès illimités au matériel. La moindre erreur dans le noyau du système d'exploitation peut compromettre toute la légitimité du reste du système. Il est possible de spécifier formellement le fonctionnement du noyau.
Il est possible de maximiser la robustesse et la sécurité au point de garantir l’absence de bugs. La présence de propriétés assurant un haut niveau de sécurité du système peut être établie, mais cela n’est possible qu’avec des noyaux de petite taille. Il est inévitable d’avoir des erreurs dans un code informatique, et plus la taille du code est élevée, plus le nombre de bugs est grand. É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.
Méthodes formelles
Objectifs de la preuve La preuve peut chercher à démontrer 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, ou quel code peut être exécuté et ce qu'il peut réaliser.
Elle peut aussi montrer la sûreté du noyau. Pour des applications critiques où la sécurité des usagers peut être en jeu, par exemple 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 limité à un événement extérieur.
Méthodes de vérifications
Vérification de modèles
Pour un noyau formalisé sous forme de modèle, on peut utiliser la Vérification de modèles : Cette méthode explorera le modèle afin de vérifier certaines règles de sécurité ou bien des propriétés bien précises. Cela n'est généralement pas suffisant pour prouver que le système est correct.
Cette méthode ne pourra être efficace que sur des noyaux de petite taille (essentiellement des micronoyaux), mais pas sur des noyaux d'OS modernes : ils sont souvent trop volumineux pour une formalisation, généralement manuelle.
En conséquence, la Vérification de modèles n'est pas une méthode qui est souvent utilisée.
Démonstration par preuve mathématique Contrairement à la Vérification de modèles, la démonstration par preuve mathématique (ou theorem proving) exprime les propriétés du noyau et son modèle de façon logique. Une preuve mathématique est déduite du modèle, confirmant ou non les propriétés recherchées.
Cette méthode a de grands avantages par rapport à la Vérification de modèles : La taille du noyau ne compte pas : une preuve mathématique peut gérer de très grands nombres. On peut donc appliquer cette méthode sur tous types de noyaux. 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.
Preuve par le code La (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.
Critères communs
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, 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és produit et moins orientés procédures que les anciens standards. Ils distinguent les responsabilités des développeurs de celle des évaluateurs. 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 , 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, on peut trouver : Nom OS Niveau CC Année Mac OS X 3 2005 Windows 2008 Server 4 2009 Novell SUSE Linux Enterprise Server 4 (?) Oracle Solaris 4 (?) Red Hat Enterprise Linux 5 4 2007 Red Hat Enterprise Linux 6 4 2014 Green Hills INTEGRITY-178B 6 2008
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.
De plus, les critères communs sont considérés comme étant trop coûteux, produisent trop de paperasse et .
Outils de vérifications
Langages formels 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 est un travail très important. Rocq 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 écrire un programme qui trouve tout seul la preuve, au lieu de construire directement l'arbre de preuve.
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éelle, tandis que la spécification génère une entrée à un de théorème interactif pour la preuve formelle de propriétés. , 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.
Vérification de modèles 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 systèmes réactifs. Le comportement d'un système réactif est décrit par une spécification formelle, et les propriétés, sont exprimées par TLC.
Exemple d'OS formellement prouvés
SeL4
Il fait partie de la famille des micronoyaux. Il adopte une approche de partitionnement qui fournit une isolation totale d’applications. Il a subi la Worst Case Execution Time, cette dernière devenue indispensable dans la vérification des systèmes, afin de tester les limites du Sel4.
Le Sel4 comporte et peut être exécuté sur différentes plateformes : X86 et ARM. L'avantage du Sel4 est qu’il fournit le partitionnement nécessaire pour soutenir des logiciels mixtes.
Intérêts de la vérification formelle d'OS
Sécurité La sécurité et la fiabilité d'un système informatique ne peuvent être aussi bonnes que celles 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 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é
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 plateforme de fiabilité sans précédent, .