# Noyau de système d'exploitation formellement prouvé

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

## 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.
Un système d'exploitation peut être défini formellement comme n'importe quel autre programme : 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é, mais cela avec de très petits noyaux. 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.

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

### 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é produit et moins orientées 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 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 :
| 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 adhèrent à un modèle de procès légal.

## 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 c'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 en fait écrire un petit 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é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.

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

## 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, a essayé de tester les limites du Sel4.
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.

## 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 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 prouvée pour seL4 est beaucoup plus forte et précise que ce que peuvent atteindre 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é. Non seulement les aspects spécifiques du noyau, tels que l'exécution sûre, sont analysés, mais une spécification complète et une preuve du comportement précis du noyau sont également fournies.

#### Limites de la preuve

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

### Coûts

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.
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), Rocq, 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.

## Historique

| Années | Projet | Plus haut niveau | Plus bas niveau | Specs | Preuves | Outils de vérification | Approche |
| (?) - 1980 | UCLA Secure Unix | Modèle de sécurité | Pascal | 20% | 20% | XIVIUS | Alphard |
| 1973 – 1983 | PSDOS | Niveau application | Code source | 17 couches | 0% | SPECIAL | HDM |
| (?) - 1987 | KIT | Tâches isolés | Assembleur | 100% | 100% | Boyer Moore | Equivalence d’interpreteur |
| 2001 – 2008 | VFiasco/Rodin | Ne crash pas | C++ | 70% | 0% | PVS | Compilateur sémantique |
| 2004 – (?) | EROS/Coyotos | Modèle de sécurité | BitC | Modèle de sécurité | 0% | ACL2 | Basé sur le langage |
| 2004 - (2008) | Verisoft | Niveau application | Gate level | 100% | 75% | Isabelle | Complètement persuasif |
| 2005 – (2008) | L4.SeL4 | Modèle de sécurité | C/Assembleur | 100% | 70% | Isabelle | Performances, production de code |