Utilisateur:Simo.93/Brouillon

Noyau de système d'exploitation formellement prouvé

---

Un noyau de système d'exploitation formellement prouvé (ou Formal Verification of an OS Kernel, le terme anglophone) est un noyau dont on a prouvé de façon mathématique que celui-ci ne possédait aucuns défauts 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ème d'exploitation apparait dans les années 70. En effet, les programmes informatique étant convertible mathématiquement, l’envie de prouver qu’ils sont correct est automatiquement apparût. Et cela est fait de manière formelle afin que cela puisse être vérifié/ checké par une machine.

Plusieures méthodes existent afin de prouver formellement que ces noyaux sont sans erreurs : tel que le Vérification de modèles ou le Démonstration automatique de théorèmes. Mais ces méthodes seuls ne suffisent pas, des outils de vérification viennent les compléter : on parle d’outils comme Spin ou ComFoRT qui sont des models checkeurs ou alors via des langages formel comme Hasquel ou Coq. Via ces méthodes et ces outils, différents critères doivent être respectés. En fonction du nombre de critère validé, un niveau d’assurance est donné au noyau. Plus le niveau est élévé, plus le noyau est garanti.

Historiquement, le 1er 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 la haute performance.

Le fait de prouver qu’un Système d'exploitation est formellement correct est une preuve de fiabilité : cela prouve que son noyau peut résister à tout type de situation. C’est aussi une preuve de sécuritée.

Mais il est à noter que la vérification formelle d’un Système d'exploitation est encore en développement et comporte actuellement en 2016 de nombreuses lacunes : on prouve qu’un Système d'exploitation est fonctionellement correcte, pas qu’il soit parfait notamment au niveau de la sécuritée.

Généralités

Définitions

Système d'exploitation

Prouver formellement qu’un Système d'exploitation est sécurisé et sans faille est un sujet de recherche de plus de 30 ans. 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 garanti sans erreurs. 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 convertit 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ème d'exploitation peut amener à une forte augmentation de la complexité ainsi qu’à une baisse des performances et des fonctionnalités.

Méthodes de vérifications

Schéma vérification formelle

Vérification de modèles

Il faut tout d'abord noté que le Vérification de modèles ne travaille pas directement sur le noyau de le Système d'exploitation. Dans un premier temps, il faut formaliser le noyau sous forme de modèle. En effet, le but du 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, peut importe l'erreur qui va survenir, cela ne fera pas crasher 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 moderne vu qu'ils sont assez volumineux en taille : cela prend énormément de temps . On va plutot l'utiliser sur des noyaux de petites taille, essentiellement des micronoyaux. On va plutot utiliser cette méthode pour vérifier certaines règles de sécurités 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érallement fait manuellement, or 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é. Certains diront qu'elle n'est pas adapté à la vérification formelle d'un noyau d'un Système d'exploitation.

theorem proving

Article principal (version anglophone)

Contrairement au Vérification de modèles, le but du "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'il confirme ces propriétés.

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

• La taille du noyau ne compte pas vu qu'une preuve mathématique peut gérer de très grand 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.

A noter que comparer au 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

Article principale (version anglophone)

La preuve par le code (PCC pour Proof-carrying code, version anglophone), est un framework pour les mécanismes de vérification des language 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 langague de programmation lui-même. On va trouver deux types de PCC :

• PCC conventionnel
• PCC fondationel

Le point négatif de cette méthode : est que cela ne fonctionne uniquement que s'il n'y a pas 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 (USA). 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é 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és 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 assurent 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. A noter que le nombre de noyau ayant atteint ce niveau est extrêmement faible. Parmis 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érifications 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 consommé é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 conséquent. 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.

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 binaires d'application réels, 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 formele spécification, et les Propriétés, sont Exprimé par TLC.

Exemple d'OS formellement prouvés

SeL4

Design et méthode de prototypage rapide de SeL4

Il fait partie de la famille des micronoyau, ses derniers sont plus critiqués que n’importe quel autre système. Il adopte une approche de partitionnement qui fournit une forte isolation totale d’applications. il a subit 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 10000 lignes de codes, exécutable sur différent plateforme : X86 et ARM l’avantage du Sel4 est qu’il fournit le partitionnement nécessaires pour soutenir des logiciels mixte.

Intérêts de la vérification formelle d'OS

Sécurité

La sécurité et la fiabilité d'un système informatique Ne peut être aussi bonne que celle de l'opéra-Système d'exploitation (OS). Le noyau, défini comme la Partie du système exécutant dans les zones les plus Mode 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. La sagesse générale veut que les bogues dans n'importe quelle base de code importante soient inévitables. 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 langages 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.

La technique utilisé pour la vérification formelle est interactive, assistée et vérifiée par machine. Spécifiquement, nous utilisons le théorème prover Isabelle / HOL La démonstration du théorème interactif nécessite l'intervention humaine et la créativité pour construire et guider la preuve. Cependant, il a l'avantage qu'il n'est pas contraint à des propriétés spécifiques ou nite, des espaces d'état réalisables, contrairement à des méthodes plus automatisées telles que l'analyse statique ou la vérification de modèle. La propriété que nous prouvons est fonctionnelle correcte dans le sens le plus fort. Formellement, nous montrons raffinement. Une preuve de raffinement établit une correspondance entre une représentation de haut niveau (abstraite) et une représentation de bas niveau (concrète ou raffinée) d'un système. La correspondance établie par la preuve de raffinement garantit que toutes les propriétés logiques de Ho-are du modèle abstrait tiennent également pour le modèle raffiné. Cela signifie que si une propriété de sécurité est prouvée dans la logique Ho-are à propos du modèle abstrait (pas toutes les propriétés de sécurité peuvent être), le raffinement garantit que la même propriété est valable pour le code source du noyau.

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, Coq, PVS, [[1]] 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 ex. 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 langague
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

Bibliographie

• (en) Thomas Hallgren, Jones Mark P, Rebekah Leslie et Andrew Tolmach, « A principled approach to operating system construction in Haskell », ACM, vol. Volume 40,‎ septembre 2005, p. 116-128 (ISBN 1-59593-064-7, DOI 10.1145/1090189.1086380)
• Harvey Tuch, Gerwin Klein et Gernot Heiser, « OS Verification -- Now! », usenix, vol. Volume 10,‎ juin 2005, p. 2-2 (lire en ligne)
• (en) Gerwin Klein, Kevin Elphinstone et Gernot Heiser, « seL4: formal verification of an OS kernel », ACM,‎ octobre 2009, p. 207-220 (ISBN 978-1-60558-752-3, DOI 10.1145/1629575.1629596)
• (en) Bernard Blackham, Yao ShiShi et Sudipta Chattopadhyay, « Timing Analysis of a Protected Operating System Kernel », IEEE,‎ décembre 2011, p. 1052-8725 (ISSN 1052-8725, DOI 10.1109/RTSS.2011.38)

• (en) Chuchang Liu et Mehmet.A Orgunb, Verification of reactive systems using temporal logic with clocks, 1999, 1-32 p. (DOI 10.1016/S0304-3975(99)00008-0)
• (en) Kevin Elphinstone1, Gerwin Klein, Philip Derrin, Timothy Roscoe2 et Gernot Heiser, « Towards a Practical, Verified Kernel », usenix.org,‎ avril 2007 (lire en ligne)
• (en) Freek Wiedijk, « Comparing mathematical provers », usenix.org,‎ 2003 (ligne=http://cs.ru.nl/~freek/comparison/diffs.pdf)
• (en) T. Vickers Benzel, « Analysis of a Kemel Verification », IEEE Symposium,‎ avril-mai 1984, p. 125-125 (ISSN 1540-7993, DOI 10.1109/SP.1984.10015)
  Security and Privacy, 1984 IEEE Symposium on
• (en) O. Ganea, F. Pop, C. Dobre et V. Cristea, « Specification and Validation of a Real-Time Simple Parallel Kernel for Dependable Distributed Systems », EIDWT,‎ septembre 2012, p. 320-325 (ISBN 978-1-4673-1986-7, DOI 10.1109/EIDWT.2012.48)
  Emerging Intelligent Data and Web Technologies (EIDWT), 2012 Third International Conference on
• (en) J. Gorski et A. Wardzinski, « Formal specification and verification of a real-time kernel », Euromicro,‎ juin 1994, p. 205-211 (ISBN 0-8186-6340-5, DOI 10.1109/EMWRTS.1994.336841)
  Real-Time Systems, 1994. Proceedings., Sixth Euromicro Workshop on
• (en) G. Naeser et K. Lundqvist, « Component-based approach to run-time kernel specification and verification », Euromicro,‎ juillet 2005, p. 68-76 (ISSN 1068-3070, DOI 10.1109/ECRTS.2005.11)
  Real-Time Systems, 2005. (ECRTS 2005). Proceedings. 17th Euromicro Conference on
• (en) B. L. Di Vito, P. H. Palmquist, E. R. Anderson et M. L. Johnston, « Specification and verification of the ASOS kernel », IEEE Computer Society Symposium,‎ mai 1990, p. 61-74 (ISBN 0-8186-2060-9, DOI 10.1109/RISP.1990.63839)
  Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on
• (en) R. M. Tol, « A small real-time kernel proven correct », Real-Time Systems Symposium,‎ décembre 1992, p. 227-230 (ISBN 0-8186-3195-3, DOI 10.1109/REAL.1992.242659)
  Real-Time Systems Symposium, 1992
• (en) T. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, X. Gao et G. Klein, « seL4: From General Purpose to a Proof of Information Flow Enforcement », IEEE Symposium,‎ mai 2013, p. 415-429 (ISSN 1081-6011, DOI 10.1109/SP.2013.35)
  Security and Privacy (SP), 2013 IEEE Symposium on
• (en) G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski et G. Heiser, « Comprehensive Formal Verification of an OS Microkernel », ACM Trans. Comput. Syst.,‎ février 2014, p. 70 (DOI 10.1145/2560537)
• (en) Y. Zhang, Y. Dong, H. Hong et F Zhang, « Code Formal Verification of Operation System », I.J.Computer Network and Information Security,‎ octobre 2010
  http://www.mecs-press.net/ijcnis/ijcnis-v2-n2/IJCNIS-V2-N2-2.pdf
• (en) A. W. Appel, « Foundational proof-carrying code », Logic in Computer Science,‎ juin 2001, p. 25-34 (ISSN 1043-6871, DOI 10.1109/FITS.2003.1264926)
  Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on
• (en) Gernot Heiser, Toby Murray et Gerwin Klein, « It's Time for Trustworthy Systems », IEEE Computer Society,‎ avril 2012, p. 67-70 (ISSN 1540-7993, DOI 10.1109/MSP.2012.41)
  Secure Syst. Group, IBM Res. Div. Zurich
• (en) Steven H. VanderLeest, « The open source, formally-proven seL4 microkernel : considerations for use in avionics », IEEE Computer Society,‎ 25-29 sept 2016 (ISSN 2155-7209, DOI 10.1109/MSP.2012.41, lire en ligne)
  conference
• (en) Gerwin Klein, « seL4: formal verification of an OS kernel », ACM digital library,‎ 11-14 october 2009, p. 207-220 (ISBN 978-1-60558-752-3, DOI 10.1145/1629575.1629596)
• (en) Bernard Beckert, Daniel Bruns et Sarah Grebing, « Mind the Gap: Formal Verification and the Common Criteria (Discussion Paper) », EasyChair, vol. 3,‎ 2012, p. 4-12 (ISSN 2398-7340, lire en ligne)
• (en) Gerwin Klein, « Correct OS kernel? Proof? done! », Usenix.org, vol. 34,‎ décembre 2009 (lire en ligne)
• (en) Gerwin Klein, Harvey Tuch et Gernot Heiser, « OS Verification -- Now! », Proceedings of the 10th conference on Hot Topics in Operating Systems, vol. 10,‎ juin 2005, p. 2-2 (lire en ligne)