Utilisateur:TV974/Brouillon

Une page de Wikipédia, l'encyclopédie libre.

CertiKOS est un projet développé par Zhong Shao, professeur à l'Université de Yale, dans le Connecticut, avec la participation d'une équipe de 6 autres chercheurs. CertiKOS (Certified Kit Operating System) est un outil méthodologique de conception et de développement de systèmes d’exploitations certifiés. Son approche se fait autour de la définition et la certifications de couches d' abstractions, elles-mêmes basées sur la sémantique de spécification riches(spécifications profondes). Ces procédés répondent à ce qui peut être considéré comme une loi fondamentale, un raffinement contextuel fort. Cette méthodologie permet non seulement de certifier toute la sémantique (par l' assistant de preuve de Coq) mais également de certifier la compilation grâce à l'utilisation de CompCertX. CertiKOS permet de développer un hyperviseur et plusieurs noyaux certifiés, dont mC2. Ce dernier prenant en charge des processeurs multi-cœurs, ainsi que la l'exécution entrelacée de modules noyau / utilisateur sur différentes couches d'abstraction (la simultanéité) .


Motivations et enjeux[modifier | modifier le code]

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, rend un service à l’utilisateur. Ils se retrouvent aujourd'hui dans nos Smartphones, voitures, drones, ordinateurs, avions, systèmes bancaires, domotiques... Selon le rapport 2017 de The Linux Foundation, le système d'exploitation Linux exécute près de 90% de la charge de travail du cloud public, couvre 62% de la part de marché de la technologie embarquée et 99% de celle des superordinateurs. Il est présent sur 82% des smartphones[1]. International Data Corporation (IDC) rapporte qu'il s'est vendu près de 355.2 millions de smartphones dans le monde, au 3ème trimestre 2018[2], soit près de 45 smartphones par secondes. L'impact est donc important mais l'enjeu financier est également présent. A titre d'exemple, selon The Transparency Market Research (TMR), le marché des systèmes embarqués dans le monde, qui pesait près de 153 milliard de dollars en 2014, pourrait passer à près de 223 milliard dollars en 2021[3]. L’omniprésence et la dépendance croissante de nos sociétés modernes à ces différents systèmes, rendent incontournable l'élaboration des logiciels fiables et sécurisés.

Les systèmes d'exploitations constituent l'épine dorsale des systèmes logiciels et des éléments particulièrement critiques, pour la sécurité dans le monde[4]. En effet, ces systèmes ne permettent pas toujours à la machine de rendre le service pour lequel ils sont conçu. Cela peut être dû à des défauts d’écriture dans le code, des défauts de conception[5], ou voire même à des interactions avec d’autres logiciels. Ces défauts peuvent donner lieu à des bugs. L'exploitation de certains des ces défauts peut également permettre à des tiers, d'en détourner les usages pour récupérer des données et ou nuire au fonctionnement des systèmes. Ces défauts constituent alors des failles de sécurités [6] (voir liens externes: "Bulletins d'informations,failles de sécurités"). Ces défauts sont mis en exergue par une vérification du code, leurs corrections se font par l'intermédiaire de patchs correctifs. Cette solution triviale implique de passer en revu chaque ligne de code et de tester tous les scénarios possibles. Bien que cette solution soit réalisable, elle devient très vite fastidieuse et exponentielle au fil de l’accumulation des lignes de codes. A titre d'exemple, le noyau Linux Version 4.13 contient 24.766.703 de lignes de codes [7]. Selon Edsger Dijkstra "Les tests de programme peuvent être utilisés pour montrer la présence de bugs, mais jamais pour montrer leur absence" [8]. L’alternative réside 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'erreur de programmation.» [9]. Ces derniers ont notamment été les premiers à produire une preuve de correction fonctionnelle pour un micro-noyau [10],[11]. CertiKOS se positionne ouvertement dans cette optique, afin de certifier un OS, plutôt que d’en faire une vérification triviale[12]. Cependant, il ne se focalise pas sur cet unique objectif. Il tente d'offrir la meilleure méthodologie pour concevoir et développer des systèmes d'exploitations performants, fiables et sûrs[13],[14]. CertiKOS cherche également à produire un noyau certifié, capable de prendre en charge la simultanéité et des machines multi-cœurs[15].

La philosophie de Certikos[modifier | modifier le code]

Le système d'exploitation, ou OS (Operating System), est un ensemble de programmes faisant l'interface entre le matériel de l'ordinateur et les programmes utilisateurs. Il constitue la colonne vertébrale d'un système informatique. Ce système est construit et repose sur la base d'un Noyau (Kernel en Anglais), qui gère les ressources matérielles. Ce dernier offre des mécanismes d' abstractions entre les logiciels et les matériels.

La certification d’un programme consiste à prouver, sur la base d’une méthode formelle, que le programme effectue sans se tromper et dans tous les cas possibles, la tache qui lui est confiée. Cette méthode repose sur une analyse statique du programme, permettant de raisonner rigoureusement afin de démontrer la validité d’un programme, par rapport à ses spécifications. Le raisonnement se fait sur la sémantique du programme.

Certification du Noyau[modifier | modifier le code]

Représentation du principe de raffinement contextuel de CertiKOS

CertiKOS a pour objectif de certifier un OS. Cette notion est basée 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 devient sujet à controverse. L'équipe de seL4 [16] a été la première à construire une preuve de correction fonctionnelle, pour un micro-noyau [17],[18]. CertiKOS s'y emploie aussi, notamment à l'aide de l' assistant de preuve de Coq et à la définition d'un raffinement contextuel fort[19],[20].

La méthodologie de CertiKOS intervient dès l'étape de conceptualisation du système et cherche notamment à définir des spécifications précises, donnant lieu à des comportements observables. Ces spécifications sont transformées en formules logiques. En prouvant de manière mathématique ces formules, on est alors en mesure de certifier le programme. L'utilisation de Certikos vise à définir des spécifications riches et détaillées, en s'appuyant sur la notion de spécifications profondes, à travers une superposition de différentes couches d'abstractions logiques[21],[22].

Le raffinement contextuel de CertiKOS indique que l’implémentation de chaque fonction du noyau, se comporte comme sa spécification dans toute interaction entre le Noyau et le programme (contexte utilisateur)[23],[24]. Ainsi, en considérant K pour le noyau, P pour le programme et S pour la spécification fonctionnelle du noyau, la combinaison des codes de K et P affine S et P. CertiKOS cherche à décomposer la vérification de l'OS en plusieurs sous taches, plus petites et elles mêmes contrôlables, sur la base de leurs spécifications profondes. C’est donc la certification de ces différentes couches d’abstractions, qui permettent de certifier l’OS. La définition du raffinement contextuel dans CertiKOS est définie de la façon suivante: prenons L0 et L1 comme deux interfaces (couches d’abstractions) et P pour un programme. L0 affine contextuellement L1, si et seulement si pour tous P, P est valide sur L1, peu importe la configuration. Le raffinement contextuel implique également que pour tous P, P est valide sur L1, peu importe la configuration, et que tout comportement observable de P sur L0, sous certaines configurations, est également observé sur L1, peu importe la configuration. [25]

(CertiKOS permet de certifier qu'entre chaque couches de fonctionnement, les fonctions à exécuter soient réalisées de manière attendue. Il ne doit pas y avoir d'altération d'état entre le niveau N et le niveau N-1.)

Spécifications profondes[modifier | modifier le code]

Les systèmes d'exploitations constituent une multitude de superposition de couches d'abstraction: noyaux (Kernel), pilotes (Drivers ), Hyperviseurs (etc..). Chacune de ces couches constituent une interface, qui masque les détails de mise en œuvre d'un ensemble de fonctionnalités de la couche sous-jacente. Les programmes clients construits au-dessus de chaque couche peuvent être compris uniquement en fonction de leurs interfaces et indépendamment de l'implémentation de la couche. Malgré leur importance évidente, les couches d'abstraction ont été généralement traitées comme un concept de système; elles n'ont presque jamais été formellement spécifiées ou vérifiées [26]. Cela rend difficile l'établissement de propriétés de corrections fortes et la mise à l'échelle de la vérification de programme, sur plusieurs couches. L’importance de définir précisément les spécifications fonctionnelles des différentes couches d’abstractions, est intimement liée à la certification de ces dernières.

Vulgarisation de l'indépendance d'implémentation de la Spécification Profonde

Cependant il s’agit de certifier un ensemble, donc de prendre en compte les relations entre les couches. C’est pourquoi CertiKOS définit des spécifications plus riches, les spécifications profondes. Ces spécifications prennent en compte l’implémentation sous-jacente, en capture les fonctionnalités précises mais aussi, les effets éventuels de l’implémentation sur ses contextes clients. [27],[28].

On peut considérer les exemples suivants (tentative de vulgarisation) :

* une spécification simple: L’eau pure boue à 100°C.

* Approche en spécification profonde : L’eau pure boue à 100°C à une pression atmosphérique de 1,013 bar.

Cet exemple illustre de manière simple, l’aspect détaillé de la spécification profonde. L’objectif de la richesse des détails de la spécification profonde, est de capturer précisément les comportements observables dans le contexte d'implémentation mais indépendamment de celui-ci. Prenons deux implémentations (par exemple, M1 et M2) de la même spécification profonde (par exemple, L), elles doivent avoir des comportements contextuellement équivalents. [29],[30]. Cette propriété d'indépendance d'implémentation des spécifications profondes rend possible la vérification modulaire des propriétés de corrections, à l'instar des spécifications de type ou de programmation par contrat [31].

Indépendance d'implémentation de la Spécification Profonde (tentative de vulgarisation) : Considérons le système de freinage (pédale de freins) d’une voiture comme une interface (L1), entre le conducteur (P) et les plaquettes de freins(Interface L0). R, traduisant la relation contextuelle entre L1 et M(1 et 2), est représenté par la pression de la pédale. La spécification profonde de l’interface L1 est l’ABS, M1 (module noyau qui implémente l’interface L1 sur la base de sa spécification) est une voiture Citroen C1. Enfin, M2 (module noyau qui implémente l’interface L1 sur la base de sa spécification) est une voiture Citroen C3. M1 et M2 auront en fonction la pression de P sur le frein, avec la possibilité du déclenchement de l’ABS.

Certification du code informatique: CompCertX[modifier | modifier le code]

CertiKOS s’emploie à concevoir des micronoyaux car leurs vérifications est par essence moins lourde. Les noyaux de systèmes d'exploitations ne sont, ni plus ni moins, que des programmes informatiques écrits dans un langage de programmation (ex : langage C) et/ou en assembleur. Tout langage de programmation constitue en soi une couche d’abstraction car il n’est pas directement interprétable par la machine.

Afin de certifier cette nouvelle couche d’abstraction, pour assurer le bon fonctionnement d'un noyau, il faut donc certifier que les lignes de codes vont pouvoir être compilées correctement, de manière à ne générer aucun bug. C’est dans ce but que CertiKOS fait appel à CompCertX «CompCert eXtended», développé par Gu et al [32],[33] et basé sur CompCert [34]. L'utilisation de CompCert ne permet pas de prouver l'exactitude de la compilation des couches individuelles ou des modules utilisés par CertiKOS. Ce dernier ne peut le faire que pour des programmes entiers. C’est pourquoi, il a été adapté [35].

CompCertX implémente ClightX (une variante du langage source de CompCert,Clight) et un langage assembleur, LAsm. La sémantique opérationnelle de CompCertX, comme CompCert, est donnée par des relations de transition en petites étapes, disposant d'états initiaux et finaux. Cependant, s’agissant de couches individuelles ou de modules, et non de programmes entiers, la définition de ces états a dû être adaptée. Pour l’état initial par exemple, CompCertX prend la mémoire initiale, la liste des arguments et le pointeur de la fonction à appeler comme paramètres. Pour l'état final, c’est la valeur de retour et l'état de la mémoire, lorsque nous quittons la fonction, qui servent de paramètres. L’état final de la mémoire est observable car il est renvoyé à l’appelant. Ainsi dans CompCertX, il est nécessaire dans les diagrammes de simulation de prendre en compte les transformations de la mémoire, lors de la mise en relation des états finaux [36].

La certification des couches d’abstractions dans CertiKOS est gérée et délivrée par CompCertX (du code source à l’assemblage). Cependant l'assembleur CompCertX permettant de convertir un assemblage en code machine, n'est pas vérifié. L’exactitude du vérificateur d’épreuve Coq et de son mécanisme d’extraction de code, est supposée [37].

Implémentation de CertiKOS[modifier | modifier le code]

Au travers d'un Hyperviseur Certifié[modifier | modifier le code]

Avec le développement important des solutions de stockage et d'hébergement de type Cloud (Amazon EC2, Salesforce CRM, Rackspace), il devenait de plus en plus important de sécuriser ces données afin que les clients puissent avoir confiance en ces solutions. Cependant, il était complexe de certifier qu'un hyperviseur était 100% sécurisé, de par sa complexité et sa taille. Il était donc impossible de certifier et garantir que son fonctionnement serait correct.

L'une des premières faille de sécurité dans un environnement cloud est le logiciel de management en lui-même. En effet, ce logiciel permet de faire de l'allocation et de la révocation de ressources sur les serveurs mis à disposition pour héberger les données, et celui-ci peut donc éventuellement avoir accès aux informations que se trouvent sur les serveurs.

Le logiciel de gestion du fournisseur utilise les interfaces de délégation du noyau approuvé pour allouer et révoquer des ressources conformément à la politique du fournisseur. À son tour, le noyau approuvé met à jour ses enregistrements de propriété afin de restreindre de manière appropriée l'accès aux ressources de chaque domaine non approuvé à l'aide de techniques de protection et de virtualisation standard.

Allocation, Gestion et Révocation des ressources selon l'Hyperviseur CertiKOS

CertiKOS alloue les ressources de la CPU de manière spatiale, à la granularité de base. Lors de la première ébauche de CertiKOS, un Coeur du CPU était affecté à un invité. Par la suite, l'hyperviseur CertiKOS a été ajusté afin de rendre l'allocation CPU 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.


Au moment de l'exécution, CertiKOS utilise ses enregistrements de propriété pour vérifier l'autorisation sur toutes les demandes d'accès explicites et pour configurer des mécanismes de protection basés sur le matériel, tels que le matériel MMU et IOMMU. De cette manière, CertiKOS applique l'isolation des ressources entre les applications et évite les fuites d'informations.


Au travers d'un Noyau Certifié: mCertiKOS,mC2[modifier | modifier le code]

Une fois l'hyperviseur développé, les chercheurs se sont retrouvés confrontés à quelques difficultés. En effet, leur hyperviseur n'était pas forcément adapté à un noyau standard Linux ou autre. Cela rendait donc l'utilisation de l'hyperviseur obsolète. Ils ont alors décidé de développer entièrement un Noyau (Kernel), de façon allegé par rapport à un noyau Linux, mais permettant de valider le bon fonctionnement de leur hyperviseur. De plus, pour développer ce noyau, ils on également utilisé les méthodes de certification, de telle sorte que le noyau soit également vérifié et que l'hyperviseur donne le meilleur rendement.

Grâce à sa sémantique de compositions de couches,CertiKOS a débouché sur plusieurs noyaux certifiés, dont les plus aboutis sont mCertikos et mC2. Mc2 est capable de prendre en charge des machines multi-cœurs et la simultanéité, ainsi que l’entrelacement d’exécutions de modules noyau et utilisateur, sur différentes couches d'abstraction [38],[39]. Le noyau mC2 est une évolution de mCertikos développé à l’origine, dans le cadre d’un vaste projet de recherche, financé par la DARPA, pour des véhicules terrestres sans pilote [40]. Ce dernier est pensé de manière séquentielle, en 4 modules totalisant 28 couches d’abstractions certifiées pour sa version basique, et de 5 modules totalisant 37 couches d’abstractions certifiées pour sa version avec hyperviseur [41]. Chaque couche est compilée et certifiée par CompCertX. Ce noyau représente 3000 lignes de code et permet de démarrer un système Linux.

Découpage des modules des noyaux mCertiKOS

En partant de mCertikos, et en y ajoutant différentes fonctionnalités (modules), telles que la gestion de la mémoire dynamique, la prise en charge des conteneurs pour le contrôle de la consommation de ressources, la prise en charge de la virtualisation du matériel Intel, la mémoire partagée IPC, verrous IPC, ticket et MCS synchrones (un spinlock par exclusion mutuelle) (etc..)[42], Certikos a fait naitre mC2.

Le noyau mC2 est quant à lui, une version plus évoluée, qui comprend 6 500 lignes d’assemblage C et x86. Il prouve que l'exactitude fonctionnelle d'un noyau de système d'exploitation simultané complet et polyvalent, avec un verrouillage à grain fin (MCS), est possible [43].

Le noyau mC2 comprend un socle fondamental de spécifications réduit, afin de simplifier le processus de révision et de limiter les erreurs. Ce socle représente près de 1400 lignes, dont 943 lignes pour les couches les plus basses, constituants la théorie axiomatique de la machine physique, et 450 lignes pour les interfaces d'appel système abstraites. En dehors de ce socle, des spécifications supplémentaires existent : 5246 lignes, pour les différentes fonctions du noyau et près de 40 000 lignes, pour définir différents théorèmes, lemmes, et invariants. [44]

CertiKOS a permit de prouver la propriété de raffinement contextuel de son noyau mC2, par rapport à une spécification profonde de haut niveau. Ce raffinement est définit de la façon suivante: pour tout programme(P), l’interaction du noyau (K) et de P, dans la sémantique de la machine x86, implique le même comportement que P dans la sémantique de la machine mC2: ∀P, [ [P⋉K] ]x86 ⊆ [ [P] ]mC2 [45]. La propriété d’équivalence de comportement pour P est donc dérivable. Toutes les interruptions et les appels système suivent strictement les spécifications de hauts niveaux. Ils sont toujours exécutés en toute sécurité (et se termine éventuellement) comme l'indique cette propriété de correction fonctionnelle. Il n'y a pas de dépassement de tampon, pas d'attaque par injection de code, de dépassement d'entier ou d'accès de pointeur nul, etc [46].

Le noyau mC2 n'est encore aussi complet qu'un système Linux. Il manque encore actuellement d'un système de stockage certifié. De plus, il s'appui sur un chargeur de démarrage qui initialise les CPU et les périphériques qui n'est pas encore vérifié [47].

Références[modifier | modifier le code]

  1. ↑ LinuxFoundation 2017, p. 1
  2. ↑ Auffray 2018, p. 1
  3. ↑ TMR 2018, p. 1
  4. ↑ Shao 2016, p. 1
  5. ↑ Toyota 2013, p. 1
  6. ↑ Kalagiakos 2012, p. 6
  7. ↑ LinuxFoundation 2017, p. 1
  8. ↑ Dijkstra 1979, p. 1
  9. ↑ Klein 2009, p. 1
  10. ↑ Gu 2015, p. 596-2
  11. ↑ Shao 2016, p. 666
  12. ↑ Shao 2016, p. 3
  13. ↑ Shao 2016, p. 655-3
  14. ↑ De Millo 1979, p. 279-9
  15. ↑ Shao 2016, p. 654
  16. ↑ Klein 2009, p. 1
  17. ↑ Gu 2015, p. 596-2
  18. ↑ Shao 2016, p. 666
  19. ↑ Shao 2016, p. 607
  20. ↑ Appel 2016, p. 2
  21. ↑ Gu 2015, p. 595-1
  22. ↑ Pierce 2016, p. 1
  23. ↑ Gu 2015, p. 596-2
  24. ↑ Shao 2016, p. 654-2
  25. ↑ Shao 2016, p. 658
  26. ↑ Gu 2015, p. 595
  27. ↑ Gu 2015, p. 595
  28. ↑ Shao 2016, p. 655
  29. ↑ Gu 2015, p. 596-2
  30. ↑ Shao 2016, p. 655-3
  31. ↑ Gu 2015, p. 596-2
  32. ↑ Gu 2015, p. 604-10
  33. ↑ Shao 2016, p. 656-4
  34. ↑ The CompCert C verified compiler 2018, p. 1
  35. ↑ Gu 2015, p. 596-2
  36. ↑ Gu 2015, p. 604-10
  37. ↑ Shao 2016, p. 657-5
  38. ↑ Gu 2015, p. 604-10
  39. ↑ Shao 2016, p. 654
  40. ↑ Shao 2016, p. 656-657
  41. ↑ Gu 2015, p. 596
  42. ↑ Shao 2016, p. 663
  43. ↑ Shao 2016, p. 654
  44. ↑ Shao 2016, p. 664
  45. ↑ Shao 2016, p. 655-655
  46. ↑ Shao 2016, p. 657
  47. ↑ Shao 2016, p. 657

Bibliographie[modifier | modifier le code]

  • (en) A. Vaynberg et Z. Shao, « Compositional Verification of a Baby Virtual Memory Manager », Springer, Berlin, Heidelberg, vol. 7679,‎ , ??-?? (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,‎ (ISBN 978-1-5090-1764-5, DOI 10.1109/TASE.2016.28)
  • (en) R.A De Millo, R.J Lipton et A.J Perlis, « Social processes and proofs of theorems and programs », The ACM Digital Library,‎ (DOI 10.1145/359104.359106)Document utilisé pour la rédaction de l’article
  • (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,‎ (ISBN 978-1-4503-3300-9, DOI 10.1145/2676726.2676975)Document utilisé pour la rédaction de l’article
  • (en) B. C. Pierce, « The science of deep specification (keynote) », The ACM Digital Library,‎ (ISBN 978-1-4503-4437-1, DOI 10.1145/2984043.2998388)Document utilisé pour la rédaction de l’article
  • (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,‎ (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,‎ (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,‎ (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,‎ (ISBN 978-1-931971-33-1)Document utilisé pour la rédaction de l’article
  • (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,‎ (ISBN 978-1-60558-752-3, DOI 10.1145/1629575.1629596)Document utilisé pour la rédaction de l’article
  • (en) A. Ferraiuolo, A. Baumann, C. Hawblitzel et B. Parno, « Komodo: Using verification to disentangle secure-enclave hardware from software », The ACM Digital Library,‎ (ISBN 978-1-4503-5085-3, DOI 10.1145/3132747.3132782)
  • (en) A. W. Appel, « Modular Verification for Computer Security », IEEE Xplore,‎ , ??-?? (ISBN 978-1-5090-2607-4, DOI 10.1109/CSF.2016.8)Document utilisé pour la rédaction de l’article
  • (en) G. Malecha, D. Ricketts, M. M. Alvarez et S. Lerner, « Towards foundational verification of cyber-physical systems », IEEE Xplore,‎ (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,‎ , ??-?? (ISBN 978-1-4673-1740-5, DOI 10.1109/ICAICT.2012.6398491)Document utilisé pour la rédaction de l’article
  • (en) E. Dijkstra, « Structured programming », The ACM Digital Library,‎ , ??-?? (ISBN 0-917072-14-6)Document utilisé pour la rédaction de l’article
  • (en) B. Reddy Kandukuri, R. Paturi V. et A. Rakshit, « Cloud Security Issues », IEEE Xplore,‎ , 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,‎ , ??-?? (DOI ??, HAL hal-01819955)
  • (en) « The CompCert C verified compiler », INRIA Paris, September 17, 2018,‎ Document utilisé pour la rédaction de l’article

Transparency Market Research, « Global Embedded Systems Market Rises at 6.4% CAGR; Automotive Industry Powers Growth », sur Transparency Market Research, (consulté en ). Christophe Auffray, « Chiffres clés : les ventes de mobiles et de smartphones », sur zdnet, (consulté en ). Christophe Auffray, Jonathan Corbet et Kroah-Hartman Greg, « 2017 Linux Kernel Development Report », sur linuxfoundation, (consulté en ).

Liens Externes[modifier | modifier le code]

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

Ce document provient de « https://fr.wikipedia.org/w/index.php?title=Utilisateur:TV974/Brouillon&oldid=162726321 ».