Utilisateur:TV974/Brouillon

Fichier:Yaabot certikos2.jpg

CertiKOS: Une nouvelle approche de composition pour la construction de noyaux d'OS concurrents certifiés.

(Résumé introductif) (Synthèse du contenue de la page Wiki) CertiKOS est un projet développé par Zhong Shao, professeur à l'Université de Yale, dans le Connecticut. Zhong Shao, accompagné d'une équipe de 6 autres chercheurs, ont développé un hyperviseur, puis un noyau, permettant de sécuriser les informations qui transitent sur une infrastructure virtualisée.

Motivations et enjeux

Idées à dev: Contexte des usages (domaine info), Problèmes de sécurités, sécurisation, "Solutions" existantes. Certifier formellement un système NB: Dans chaque partie remonter des citations avec les ref biblio. Ca donne la matière pour fabriquer le contenu du paragraphe. Eviter absolument 1 citation par paragraphe. Il faut plusieurs citation ou exemples.

[idée: Construire des piles de logiciels système fiables et sécurisées | Multiplications des usages/outils dépendants de Logiciels (OS) : Voiture, Drone, cloud, Smarphone, Ordinateur, avion, banque.] Les noyaux et les hyperviseurs de système d'exploitation (OS) constituent l'épine dorsale des systèmes logiciels critiques pour la sécurité dans le monde..

Les Noyaux, Systèmes d'exploitations, Hyperviseurs (etc…) sont des logiciels/programmes. Une succession de lignes de code qui une fois compilée et interprétée par la machine rendent un service à l’utilisateur. Ils se retrouvent aujourd'hui dans nos Smartphones, voitures, drones, ordinateurs, avions, domitique... Ils constituent l'épine dorsale des systèmes logiciels et un élément particulièrement critiques pour la sécurité dans le monde.. Il s'agit également d'un enjeux financé important. A titre d'exemple, selont TMR le marché des systèmes embarqués dans le monde, qui pesait près de 153 milliard de dollard en 2014, pourrait passé à près de 223 milliard en 2021. Cependant, ces systèmes ne permettent pas toujours à la machine de rendre le service pour lequel ils ont été conçu, soit lié à des défauts d’écriture dans le code, soit à des défauts de conception ou voir même à des interactions avec d’autres logiciels.

[idée: illustration avec exemples de failles (US-CERT, CERT)]

Selon Edsger Dijkstra "Les tests de programme peuvent être utilisés pour montrer la présence de bugs, mais jamais pour montrer leur absence". La manière la plus trivial de vérifier du logiciel consisterait à vérifier chaque ligne de code et à tester tous les scénarios possibles. Bien que cette solution soit réalisable, elle devient très vite fastidieuse au fil de l’accumulation des lignes de codes. L’alternative consisterait en une vérification par méthode formelle (déductive), selon les contributeurs de seL4 « Une vérification formelle complète est le seul moyen connu de garantir qu'un système est exempt d'erreurs de programmation.» . Certikos se positionne ouvertement dans cette optique dans le but de certifier un OS plutôt que d’en faire une vérficiation. [•Qualité des preuves formelles. ] .

La philosophie de Certikos

Rappel rapide sur SO/kernel(...). Rappel sur méthode Formelle, informelle. Idée à dev: En quoi c'est compliqué de certifié? (effort de preuve). Comment certifier?(L'approche de certikos). Partir de qu'il ont fait et montré comment ils l'ont implémenté?

Certification d'un Noyau

Idée à dev:

Certikos a pour objectif de certifier un OS. Cette notion est basé sur la prouvabilité de la vérification par machine, de manière explicite et formelle. Cet effort de preuve est d'autant plus compliqué lorsqu'on s'attache à la qualité de la preuve. Plus cette dernière est étayée, précise, moins elle est devient sujet à controverse. Certikos s'y employe notamment à l'aide de l'assistant de preuve de Coq et à la définition d'un raffinement contextuel fort . Ce raffinement contextuel a pour but de définir des spécifications précises donnant lieu à de comportements observables. (Ces spécifications vont être transformées en formules logiques. En prouvant de manière mathématique ces formules, on est alors en mesure de certifié le programme.) Certikos défini des spécifications riches et détaillées en s'appuyant sur la notion de spécifications profondes . Ce niveau raffinement contextuel permet de décomposer la vérification de l'OS en plusieurs sous taches plus petite et elles même contrôlable sur la base de leurs spécifications profondes. [A certified abstraction layer consists of a language construct (L1;M;L2) and a mechanized proof object showing that the layer implementation M, built on top of the interface L1 (the underlay), is a contextual refinement of the desirable interface L2 above (the overlay). A deep specification (L2) of a module (M) captures everything contextually observable about running the module over its underlay (L1). Once we have certified M with a deep specification L2, there is no need to ever look at M again, and any property about M can be proved using L2 alone.]=>Fonctionnement similaire aux PKI à mon sens, à creuser.

Définition des Spécifications

Idée à dev: Identifier démêler les interactions; Raffinement contextuel (identifier différents comportements observables pour différentes propriétés de progression);Primitives, Deeps Spécifications.

Le provider de solutions avait accès aux VM via le logiciel de supervision. Cela pouvait créer une première faille de sécurité, car celui-ci pouvait avoir accès aux informations concernant les espaces mémoires alloués à chaque client. Ce problème est traité par CertiKOS, en effet le provider n'a plus d'accès direct aux ressources allouées aux clients, il ne fait qu’attribuer des ressources, ou les révoquer. Le logiciel de supervision est alors considéré comme un client, avec quelques droits supplémentaires.

Allocation des ressources selon CertiKOS

• Allocation CPU :

CertiKOS alloue les ressources de la CPU de manière spatiale, à la granularité de base. Dans la conception actuelle, CertiKOS affecte simplement un invité à chaque cœur, bien que les extensions futures puissent affecter les processeurs de manière plus flexible. CertiKOS fournit des interfaces pour le logiciel de gestion permettant d'allouer des cœurs de processeur aux clients et de les révoquer.

• Allocation RAM et Disques :

CertiKOS extrait à la fois la RAM et les disques en tant qu'espace mémoire pour les logiciels de gestion non fiables et les invités. Le noyau ne comprend aucun système de fichiers, laissant cette fonctionnalité au logiciel invité non approuvé. CertiKOS expose uniquement les interfaces prenant en charge la délégation et l’accès protégé à la mémoire et au stockage sur disque.

• Allocation Interfaces :

CertiKOS présente des interfaces permettant au logiciel de gestion du fournisseur de donner aux clients un accès à l’infrastructure de réseau partagé du fournisseur. La conception actuelle suppose que le matériel du serveur fournit suffisamment de cartes réseau physiques et / ou de cartes réseau virtualisées pour dédier au moins une carte réseau à chaque client sans multiplexage logiciel. CertiKOS pourrait être amélioré à l’avenir pour fournir son propre multiplexage dynamique des interfaces réseau, mais ce n’est pas une priorité absolue, car la virtualisation de la carte réseau basée sur le matériel devient de plus en plus courante et peu coûteuse.

Bibliographie

• (en) A. Vaynberg et Z. Shao, « Compositional Verification of a Baby Virtual Memory Manager », Springer, Berlin, Heidelberg, vol. 7679,‎ 2012, ??-?? (ISBN 978-3-642-35308-6, DOI 10.1007/978-3-642-35308-6_13)
• (en) N. Jomaa, D. Nowak, G. Grimaud et S. Hym, « Formal Proof of Dynamic Memory Isolation Based on MMU », IEEE Xplore,‎ août 2016 (ISBN 978-1-5090-1764-5, DOI 10.1109/TASE.2016.28)
• (en) R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S-C. Weng et H. Zhang, « Deep Specifications and Certified Abstraction Layers », The ACM Digital Library,‎ janvier 2015 (ISBN 978-1-4503-3300-9, DOI 10.1145/2676726.2676975)
• (en) B. C. Pierce, « The science of deep specification (keynote) », The ACM Digital Library,‎ octobre 2016 (ISBN 978-1-4503-4437-1, DOI 10.1145/2984043.2998388)
• (en) A. W. Appel, L. Beringer, A. Chlipala, B. C. Pierce, Z. Shao, S. Weirich et S. Zdancewic, « Position paper: the science of deep specification », the Royal Society,‎ septembre 2017 (DOI 10.1098/rsta.2016.0331)
• (en) H. Liang, J. Hoffmann, X. Feng et Z. Shao, « Characterizing Progress Properties of Concurrent Objects via Contextual Refinements », Springer,‎ 2013 (ISBN 978-3-642-40184-8, DOI 10.1007/978-3-642-40184-8_17)
• (en) L. Gu, A. Vaynberg, B. Ford, Z. Shao et D. Costanzo, « CertiKOS: a certified kernel for secure cloud computing », The ACM Digital Library,‎ juillet 2011 (ISBN 978-1-4503-1179-3, DOI 10.1145/2103799.2103803)
• (en) R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim, V. Sjöberg et D. Costanzo, « CertiKOS: an extensible architecture for building certified concurrent OS kernels », The ACM Digital Library,‎ novembre 2016 (ISBN 978-1-931971-33-1)
• (en) G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T Sewell, H. Tuch et S. Winwood, « seL4: Formal Verification of an OS Kernel », the Association for Computing Machinery,‎ octobre 2009 (ISBN 978-1-60558-752-3, DOI 10.1145/1629575.1629596)
• (en) A. Ferraiuolo, A. Baumann, C. Hawblitzel et B. Parno, « Komodo: Using verification to disentangle secure-enclave hardware from software », The ACM Digital Library,‎ octobre 2017 (ISBN 978-1-4503-5085-3, DOI 10.1145/3132747.3132782)
• (en) A. W. Appel, « Modular Verification for Computer Security », IEEE Xplore,‎ août 2016, ??-?? (ISBN 978-1-5090-2607-4, DOI 10.1109/CSF.2016.8)
• (en) G. Malecha, D. Ricketts, M. M. Alvarez et S. Lerner, « Towards foundational verification of cyber-physical systems », IEEE Xplore,‎ avril 2016 (ISBN 978-1-5090-4304-0, DOI 10.1109/SOSCYPS.2016.7580000)
• (en) P. Kalagiakos et M. Bora, « Cloud security tactics: Virtualization and the VMM », IEEE Xplore,‎ décembre 2012, ??-?? (ISBN 978-1-4673-1740-5, DOI 10.1109/ICAICT.2012.6398491)
• (en) E. Dijkstra, « Structured programming », The ACM Digital Library,‎ janvier 1979, ??-?? (ISBN 0-917072-14-6)
• (en) A. Rakshit, « Cloud Security Issues », IEEE Xplore,‎ septembre 2009, p. 517- 520 (ISBN 978-0-7695-3811-2, DOI 10.1109/SCC.2009.84)
• N. Jomaa, S. Hym et D. Novak, « La conception d’un noyau orientée par sa preuve d’isolation mémoire », Compas 2018, vol. Juillet 2018,‎ 2018, ??-?? (DOI ??, HAL hal-01819955)

Transparency Market Research, « Global Embedded Systems Market Rises at 6.4% CAGR; Automotive Industry Powers Growth », sur Transparency Market Research, novembre 2018 (consulté en décembre 2018).

Liens Externes

Bulletin d'information: Failles informatiques https://www.us-cert.gov/ https://www.cert.ssi.gouv.fr

• (en) US CERT, « VMware-Releases-Security-Updates », novembre 2018
• (en) US CERT, « Microsoft-Releases-November-2018-Security-Updates », novembre 2018
• (en) US CERT, « Cisco-Releases-Security-Updates », novembre 2018
• (en) US CERT, « Apple-Releases-Security-Updates-iCloud-iOS », novembre 2018
• (en) US CERT, « Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors », novembre 2018
• FR CERT, « Multiples vulnérabilités de fuite d’informations dans des processeurs », janvier 2018
• FR CERT, « Vulnérabilité dans Wallix AdminBastion », octobre 2018
• FR CERT, « Multiples vulnérabilités dans le noyau Linux d’Ubuntu », écembre 2018
• (en) R. Gu, « My Current Work on CertiKOS »
• (en) « Toyota's killer firmware: Bad design and its consequences », octobre 2013