About DBpedia Fr

About: http://fr.dbpedia.org/resource/Noyau_de_système_d'exploitation_formellement_prouvé

An Entity of Type : Thing, from Named Graph : http://fr.dbpedia.org, within Data Space : fr.dbpedia.org

Un noyau de système d'exploitation formellement prouvé (ou Formal Verification of an OS Kernel, le 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. 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 la haute performance.

thumbnail
Property Value
dbo:abstract
  • Un noyau de système d'exploitation formellement prouvé (ou Formal Verification of an OS Kernel, le 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. En effet, les programmes informatiques étant convertibles mathématiquement, l’envie de prouver qu’ils sont corrects est automatiquement apparue. Et cela est fait de manière formelle afin que cela puisse être vérifié/ checké par une machine. Plusieurs méthodes existent afin de prouver formellement que ces noyaux sont sans erreur, telles que la Vérification de modèles ou la Démonstration automatique de théorèmes. Mais ces méthodes seules 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 formels comme Haskell ou Coq. Via ces méthodes et ces outils, 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 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é. 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 des nombreuses lacunes : on prouve qu’un système d'exploitation est fonctionnellement correct, pas qu’il soit parfait notamment au niveau de la sécurité. (fr)
  • Un noyau de système d'exploitation formellement prouvé (ou Formal Verification of an OS Kernel, le 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. En effet, les programmes informatiques étant convertibles mathématiquement, l’envie de prouver qu’ils sont corrects est automatiquement apparue. Et cela est fait de manière formelle afin que cela puisse être vérifié/ checké par une machine. Plusieurs méthodes existent afin de prouver formellement que ces noyaux sont sans erreur, telles que la Vérification de modèles ou la Démonstration automatique de théorèmes. Mais ces méthodes seules 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 formels comme Haskell ou Coq. Via ces méthodes et ces outils, 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 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é. 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 des nombreuses lacunes : on prouve qu’un système d'exploitation est fonctionnellement correct, pas qu’il soit parfait notamment au niveau de la sécurité. (fr)
dbo:thumbnail
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 10556175 (xsd:integer)
dbo:wikiPageLength
  • 28190 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 181295373 (xsd:integer)
dbo:wikiPageWikiLink
prop-fr:année
  • 1984 (xsd:integer)
  • 1990 (xsd:integer)
  • 1992 (xsd:integer)
  • 1994 (xsd:integer)
  • 1999 (xsd:integer)
  • 2001 (xsd:integer)
  • 2003 (xsd:integer)
  • 2005 (xsd:integer)
  • 2007 (xsd:integer)
  • 2009 (xsd:integer)
  • 2010 (xsd:integer)
  • 2011 (xsd:integer)
  • 2012 (xsd:integer)
  • 2013 (xsd:integer)
  • 2014 (xsd:integer)
  • 2016 (xsd:integer)
prop-fr:commentaire
  • http://www.mecs-press.net/ijcnis/ijcnis-v2-n2/IJCNIS-V2-N2-2.pdf
  • conférence (fr)
  • Secure Syst. Group, IBM Res. Div. Zurich (fr)
  • Real-Time Systems Symposium, 1992 (fr)
  • Security and Privacy , 2013 IEEE Symposium on (fr)
  • Security and Privacy, 1984 IEEE Symposium on (fr)
  • Emerging Intelligent Data and Web Technologies , 2012 Third International Conference on (fr)
  • Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on (fr)
  • Research in Security and Privacy, 1990. Proceedings., 1990 IEEE Computer Society Symposium on (fr)
  • Real-Time Systems, 1994. Proceedings., Sixth Euromicro Workshop on (fr)
  • Real-Time Systems, 2005. . Proceedings. 17th Euromicro Conference on (fr)
prop-fr:doi
  • 10.101600 (xsd:double)
  • 10.110900 (xsd:double)
  • 10.114500 (xsd:double)
prop-fr:fr
  • ACL2 (fr)
  • ACL2 (fr)
prop-fr:id
  • Klein2009 (fr)
  • Bernard2011 (fr)
  • Bernard2012 (fr)
  • CompFormalVerif (fr)
  • Compo2005 (fr)
  • FondPCC2003 (fr)
  • Formal1994 (fr)
  • Gernot2012 (fr)
  • Gerwin2009 (fr)
  • Hallgren2005 (fr)
  • Harvey2005 (fr)
  • KemelVerif1984 (fr)
  • Liu1999 (fr)
  • Sel42013 (fr)
  • SmallR1992 (fr)
  • SpecifKernel990 (fr)
  • Specification2012 (fr)
  • VanderLeest2016 (fr)
  • codeFormalVerif2010 (fr)
  • Klein2009 (fr)
  • Bernard2011 (fr)
  • Bernard2012 (fr)
  • CompFormalVerif (fr)
  • Compo2005 (fr)
  • FondPCC2003 (fr)
  • Formal1994 (fr)
  • Gernot2012 (fr)
  • Gerwin2009 (fr)
  • Hallgren2005 (fr)
  • Harvey2005 (fr)
  • KemelVerif1984 (fr)
  • Liu1999 (fr)
  • Sel42013 (fr)
  • SmallR1992 (fr)
  • SpecifKernel990 (fr)
  • Specification2012 (fr)
  • VanderLeest2016 (fr)
  • codeFormalVerif2010 (fr)
prop-fr:isbn
  • 0 (xsd:integer)
  • 1 (xsd:integer)
  • 978 (xsd:integer)
prop-fr:issn
  • 1043 (xsd:integer)
  • 1052 (xsd:integer)
  • 1068 (xsd:integer)
  • 1081 (xsd:integer)
  • 1540 (xsd:integer)
  • 2155 (xsd:integer)
  • 2398 (xsd:integer)
prop-fr:lang
  • en (fr)
  • en (fr)
prop-fr:mois
  • --10-14
  • décembre (fr)
  • mai (fr)
  • septembre (fr)
  • juillet (fr)
  • --09-29
  • avril (fr)
  • juin (fr)
  • octobre (fr)
  • février (fr)
  • April-May (fr)
prop-fr:nom
  • Dong (fr)
  • Pop (fr)
  • Anderson (fr)
  • Bruns (fr)
  • Johnston (fr)
  • Murray (fr)
  • Hong (fr)
  • Liu (fr)
  • Lundqvist (fr)
  • Zhang (fr)
  • Appel (fr)
  • Gao (fr)
  • Leslie (fr)
  • Klein (fr)
  • Sewell (fr)
  • Grebing (fr)
  • Gorski (fr)
  • Tol (fr)
  • Ganea (fr)
  • Bourke (fr)
  • Beckert (fr)
  • Andronick (fr)
  • Cock (fr)
  • Derrin (fr)
  • Elkaduwe (fr)
  • Elphinstone (fr)
  • Engelhardt (fr)
  • Heiser (fr)
  • Kolanski (fr)
  • Norrish (fr)
  • Tuch (fr)
  • Winwood (fr)
  • Dobre (fr)
  • Blackham (fr)
  • Cristea (fr)
  • Chattopadhyay (fr)
  • Hallgren (fr)
  • Palmquist (fr)
  • Di Vito (fr)
  • Brassil (fr)
  • Elphinstone1 (fr)
  • Gammie (fr)
  • H. VanderLeest (fr)
  • Mark P (fr)
  • Matichuk (fr)
  • Naeser (fr)
  • Orgunb (fr)
  • Roscoe2 (fr)
  • Seefried (fr)
  • ShiShi (fr)
  • Tolmach (fr)
  • Vickers Benzel (fr)
  • Wardzinski (fr)
  • Wiedijk (fr)
  • Dong (fr)
  • Pop (fr)
  • Anderson (fr)
  • Bruns (fr)
  • Johnston (fr)
  • Murray (fr)
  • Hong (fr)
  • Liu (fr)
  • Lundqvist (fr)
  • Zhang (fr)
  • Appel (fr)
  • Gao (fr)
  • Leslie (fr)
  • Klein (fr)
  • Sewell (fr)
  • Grebing (fr)
  • Gorski (fr)
  • Tol (fr)
  • Ganea (fr)
  • Bourke (fr)
  • Beckert (fr)
  • Andronick (fr)
  • Cock (fr)
  • Derrin (fr)
  • Elkaduwe (fr)
  • Elphinstone (fr)
  • Engelhardt (fr)
  • Heiser (fr)
  • Kolanski (fr)
  • Norrish (fr)
  • Tuch (fr)
  • Winwood (fr)
  • Dobre (fr)
  • Blackham (fr)
  • Cristea (fr)
  • Chattopadhyay (fr)
  • Hallgren (fr)
  • Palmquist (fr)
  • Di Vito (fr)
  • Brassil (fr)
  • Elphinstone1 (fr)
  • Gammie (fr)
  • H. VanderLeest (fr)
  • Mark P (fr)
  • Matichuk (fr)
  • Naeser (fr)
  • Orgunb (fr)
  • Roscoe2 (fr)
  • Seefried (fr)
  • ShiShi (fr)
  • Tolmach (fr)
  • Vickers Benzel (fr)
  • Wardzinski (fr)
  • Wiedijk (fr)
prop-fr:pages
  • 1 (xsd:integer)
  • 2 (xsd:integer)
  • 4 (xsd:integer)
  • 25 (xsd:integer)
  • 61 (xsd:integer)
  • 67 (xsd:integer)
  • 68 (xsd:integer)
  • 70 (xsd:integer)
  • 116 (xsd:integer)
  • 125 (xsd:integer)
  • 205 (xsd:integer)
  • 207 (xsd:integer)
  • 227 (xsd:integer)
  • 320 (xsd:integer)
  • 415 (xsd:integer)
  • 1052 (xsd:integer)
prop-fr:prénom
  • F (fr)
  • Yao (fr)
  • A. (fr)
  • A. W. (fr)
  • Andrew (fr)
  • G. (fr)
  • H. (fr)
  • J. (fr)
  • K. (fr)
  • M. (fr)
  • Michael (fr)
  • P. (fr)
  • R. (fr)
  • Y. (fr)
  • C. (fr)
  • Bernard (fr)
  • D. (fr)
  • Daniel (fr)
  • David (fr)
  • Kevin (fr)
  • Sarah (fr)
  • Simon (fr)
  • Jones (fr)
  • Philip (fr)
  • S. (fr)
  • Thomas (fr)
  • V. (fr)
  • Steven (fr)
  • T. (fr)
  • F. (fr)
  • Harvey (fr)
  • June (fr)
  • Toby (fr)
  • O. (fr)
  • R. M. (fr)
  • Timothy (fr)
  • X. (fr)
  • B. L. (fr)
  • E. R. (fr)
  • M. L. (fr)
  • Kai (fr)
  • P. H. (fr)
  • Rebekah (fr)
  • Gernot (fr)
  • Dhammika (fr)
  • Freek (fr)
  • Gerwin (fr)
  • Rafal (fr)
  • Chuchang (fr)
  • Mehmet.A (fr)
  • Sudipta (fr)
  • F (fr)
  • Yao (fr)
  • A. (fr)
  • A. W. (fr)
  • Andrew (fr)
  • G. (fr)
  • H. (fr)
  • J. (fr)
  • K. (fr)
  • M. (fr)
  • Michael (fr)
  • P. (fr)
  • R. (fr)
  • Y. (fr)
  • C. (fr)
  • Bernard (fr)
  • D. (fr)
  • Daniel (fr)
  • David (fr)
  • Kevin (fr)
  • Sarah (fr)
  • Simon (fr)
  • Jones (fr)
  • Philip (fr)
  • S. (fr)
  • Thomas (fr)
  • V. (fr)
  • Steven (fr)
  • T. (fr)
  • F. (fr)
  • Harvey (fr)
  • June (fr)
  • Toby (fr)
  • O. (fr)
  • R. M. (fr)
  • Timothy (fr)
  • X. (fr)
  • B. L. (fr)
  • E. R. (fr)
  • M. L. (fr)
  • Kai (fr)
  • P. H. (fr)
  • Rebekah (fr)
  • Gernot (fr)
  • Dhammika (fr)
  • Freek (fr)
  • Gerwin (fr)
  • Rafal (fr)
  • Chuchang (fr)
  • Mehmet.A (fr)
  • Sudipta (fr)
prop-fr:périodique
  • IEEE (fr)
  • ACM (fr)
  • IEEE Computer Society (fr)
  • Logic in Computer Science (fr)
  • ACM Trans. Comput. Syst. (fr)
  • ACM digital library (fr)
  • EIDWT (fr)
  • EasyChair (fr)
  • Euromicro (fr)
  • I.J.Computer Network and Information Security (fr)
  • IEEE Computer Society Symposium (fr)
  • IEEE Symposium (fr)
  • Real-Time Systems Symposium (fr)
  • Usenix.org (fr)
  • usenix (fr)
  • usenix.org (fr)
  • IEEE (fr)
  • ACM (fr)
  • IEEE Computer Society (fr)
  • Logic in Computer Science (fr)
  • ACM Trans. Comput. Syst. (fr)
  • ACM digital library (fr)
  • EIDWT (fr)
  • EasyChair (fr)
  • Euromicro (fr)
  • I.J.Computer Network and Information Security (fr)
  • IEEE Computer Society Symposium (fr)
  • IEEE Symposium (fr)
  • Real-Time Systems Symposium (fr)
  • Usenix.org (fr)
  • usenix (fr)
  • usenix.org (fr)
prop-fr:texte
  • ACL2 (fr)
  • ACL2 (fr)
prop-fr:titre
  • Comprehensive Formal Verification of an OS Microkernel (fr)
  • seL4: From General Purpose to a Proof of Information Flow Enforcement (fr)
  • A small real-time kernel proven correct (fr)
  • Analysis of a Kemel Verification (fr)
  • Code Formal Verification of Operation System (fr)
  • Comparing mathematical provers (fr)
  • Correct OS kernel? Proof? done! (fr)
  • Foundational proof-carrying code (fr)
  • It's Time for Trustworthy Systems (fr)
  • OS Verification -- Now! (fr)
  • Specification and verification of the ASOS kernel (fr)
  • Towards a Practical, Verified Kernel (fr)
  • A principled approach to operating system construction in Haskell (fr)
  • seL4: formal verification of an OS kernel (fr)
  • Verification of reactive systems using temporal logic with clocks (fr)
  • Timing Analysis of a Protected Operating System Kernel (fr)
  • Specification and Validation of a Real-Time Simple Parallel Kernel for Dependable Distributed Systems (fr)
  • The open source, formally-proven seL4 microkernel : considerations for use in avionics (fr)
  • Component-based approach to run-time kernel specification and verification (fr)
  • Formal specification and verification of a real-time kernel (fr)
  • Mind the Gap: Formal Verification and the Common Criteria (fr)
  • Comprehensive Formal Verification of an OS Microkernel (fr)
  • seL4: From General Purpose to a Proof of Information Flow Enforcement (fr)
  • A small real-time kernel proven correct (fr)
  • Analysis of a Kemel Verification (fr)
  • Code Formal Verification of Operation System (fr)
  • Comparing mathematical provers (fr)
  • Correct OS kernel? Proof? done! (fr)
  • Foundational proof-carrying code (fr)
  • It's Time for Trustworthy Systems (fr)
  • OS Verification -- Now! (fr)
  • Specification and verification of the ASOS kernel (fr)
  • Towards a Practical, Verified Kernel (fr)
  • A principled approach to operating system construction in Haskell (fr)
  • seL4: formal verification of an OS kernel (fr)
  • Verification of reactive systems using temporal logic with clocks (fr)
  • Timing Analysis of a Protected Operating System Kernel (fr)
  • Specification and Validation of a Real-Time Simple Parallel Kernel for Dependable Distributed Systems (fr)
  • The open source, formally-proven seL4 microkernel : considerations for use in avionics (fr)
  • Component-based approach to run-time kernel specification and verification (fr)
  • Formal specification and verification of a real-time kernel (fr)
  • Mind the Gap: Formal Verification and the Common Criteria (fr)
prop-fr:trad
  • ACL2 (fr)
  • ACL2 (fr)
prop-fr:url
prop-fr:volume
  • 3 (xsd:integer)
  • 34 (xsd:integer)
  • Volume 10 (fr)
  • Volume 40 (fr)
prop-fr:wikiPageUsesTemplate
dct:subject
rdfs:comment
  • Un noyau de système d'exploitation formellement prouvé (ou Formal Verification of an OS Kernel, le 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. 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 la haute performance. (fr)
  • Un noyau de système d'exploitation formellement prouvé (ou Formal Verification of an OS Kernel, le 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. 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 la haute performance. (fr)
rdfs:label
  • Noyau de système d'exploitation formellement prouvé (fr)
  • Noyau de système d'exploitation formellement prouvé (fr)
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:isPrimaryTopicOf
is dbo:wikiPageWikiLink of
is oa:hasTarget of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License