Noyau de système d'exploitation formellement prouvé
De Wikipedia, l'encyclopédie encyclopedia
Un noyau de système d'exploitation formellement prouvé (ou Formal Verification of an OS Kernel, 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.
Cet article n’est pas rédigé dans un style encyclopédique ().
Vous pouvez améliorer sa rédaction !
Certaines informations figurant dans cet article ou cette section devraient être mieux reliées aux sources mentionnées dans les sections « Bibliographie », « Sources » ou « Liens externes » ().
Vous pouvez améliorer la vérifiabilité en associant ces informations à des références à l'aide d'appels de notes.
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 des langages formels comme Haskell ou Coq doivent les compléter. A 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 recherches.