Property |
Value |
dbo:abstract
|
- 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’exploitation certifiés. Son approche se fait autour de la définition et la Certification de couches d'abstraction, elles-mêmes basées sur la sémantique de spécification riche (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 l'exécution entrelacée de modules noyau / utilisateur sur différentes couches d'abstraction (la simultanéité) . (fr)
- 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’exploitation certifiés. Son approche se fait autour de la définition et la Certification de couches d'abstraction, elles-mêmes basées sur la sémantique de spécification riche (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 l'exécution entrelacée de modules noyau / utilisateur sur différentes couches d'abstraction (la simultanéité) . (fr)
|
dbo:thumbnail
| |
dbo:wikiPageExternalLink
| |
dbo:wikiPageID
| |
dbo:wikiPageLength
|
- 38636 (xsd:nonNegativeInteger)
|
dbo:wikiPageRevisionID
| |
dbo:wikiPageWikiLink
| |
prop-fr:année
|
- 1979 (xsd:integer)
- 2009 (xsd:integer)
- 2011 (xsd:integer)
- 2012 (xsd:integer)
- 2013 (xsd:integer)
- 2015 (xsd:integer)
- 2016 (xsd:integer)
- 2017 (xsd:integer)
- 2018 (xsd:integer)
|
prop-fr:auteur
|
- Christophe Auffray (fr)
- Transparency Market Research (fr)
- Christophe Auffray (fr)
- Transparency Market Research (fr)
|
prop-fr:consultéLe
|
- Décembre 2018 (fr)
- Novembre 2018 (fr)
- Décembre 2018 (fr)
- Novembre 2018 (fr)
|
prop-fr:date
|
- 2017 (xsd:integer)
- 2018-11-26 (xsd:date)
- Novembre 2018 (fr)
|
prop-fr:doi
|
- 10.100700 (xsd:double)
- 10.109800 (xsd:double)
- 10.110900 (xsd:double)
- 10.114500 (xsd:double)
- ?? (fr)
|
prop-fr:hal
|
- hal-01819955 (fr)
- hal-01819955 (fr)
|
prop-fr:id
|
- AT&T (fr)
- Shao (fr)
- Appel2016 (fr)
- Appel2017 (fr)
- Auffray2018 (fr)
- Certik (fr)
- De Millo1979 (fr)
- Dijkstra1979 (fr)
- FR-CERT2018-1 (fr)
- FR-CERT2018-2 (fr)
- FR-CERT2018-3 (fr)
- Ferraiuolo2017 (fr)
- Gu2015 (fr)
- Jomaa2016 (fr)
- Jomaa2018 (fr)
- Kalagiakos2012 (fr)
- Klein2009 (fr)
- Liang2013 (fr)
- LinuxFoundation2017 (fr)
- Malecha2016 (fr)
- Pierce2016 (fr)
- Reddy2009 (fr)
- Ronghui Gu (fr)
- Shao2016 (fr)
- Shao2017-1 (fr)
- Shao2017-2 (fr)
- TMR2018 (fr)
- The CompCert C verified compiler (fr)
- Toyota2013 (fr)
- US-CERT2018-1 (fr)
- US-CERT2018-2 (fr)
- US-CERT2018-3 (fr)
- US-CERT2018-4 (fr)
- US-CERT2018-5 (fr)
- Vaynberg2011 (fr)
- Vaynberg2012 (fr)
- cnrs (fr)
- github (fr)
- AT&T (fr)
- Shao (fr)
- Appel2016 (fr)
- Appel2017 (fr)
- Auffray2018 (fr)
- Certik (fr)
- De Millo1979 (fr)
- Dijkstra1979 (fr)
- FR-CERT2018-1 (fr)
- FR-CERT2018-2 (fr)
- FR-CERT2018-3 (fr)
- Ferraiuolo2017 (fr)
- Gu2015 (fr)
- Jomaa2016 (fr)
- Jomaa2018 (fr)
- Kalagiakos2012 (fr)
- Klein2009 (fr)
- Liang2013 (fr)
- LinuxFoundation2017 (fr)
- Malecha2016 (fr)
- Pierce2016 (fr)
- Reddy2009 (fr)
- Ronghui Gu (fr)
- Shao2016 (fr)
- Shao2017-1 (fr)
- Shao2017-2 (fr)
- TMR2018 (fr)
- The CompCert C verified compiler (fr)
- Toyota2013 (fr)
- US-CERT2018-1 (fr)
- US-CERT2018-2 (fr)
- US-CERT2018-3 (fr)
- US-CERT2018-4 (fr)
- US-CERT2018-5 (fr)
- Vaynberg2011 (fr)
- Vaynberg2012 (fr)
- cnrs (fr)
- github (fr)
|
prop-fr:isbn
|
- 0 (xsd:integer)
- 978 (xsd:integer)
|
prop-fr:isnn
| |
prop-fr:lang
|
- en (fr)
- fr (fr)
- en (fr)
- fr (fr)
|
prop-fr:lireEnLigne
| |
prop-fr:mois
|
- Avril (fr)
- Décembre (fr)
- Janvier (fr)
- Octobre (fr)
- décembre (fr)
- septembre (fr)
- May (fr)
- octobre (fr)
- October (fr)
- September (fr)
- January (fr)
- August (fr)
- july (fr)
- november (fr)
- Avril (fr)
- Décembre (fr)
- Janvier (fr)
- Octobre (fr)
- décembre (fr)
- septembre (fr)
- May (fr)
- octobre (fr)
- October (fr)
- September (fr)
- January (fr)
- August (fr)
- july (fr)
- november (fr)
|
prop-fr:nom
|
- Ford (fr)
- Greg (fr)
- Grimaud (fr)
- Perlis (fr)
- Hoffmann (fr)
- Shao (fr)
- Chen (fr)
- Wu (fr)
- Costanzo (fr)
- Feng (fr)
- Kim (fr)
- Liang (fr)
- Zhang (fr)
- Lerner (fr)
- Appel (fr)
- Burke (fr)
- Alvarez (fr)
- Klein (fr)
- Nowak (fr)
- Sewell (fr)
- Gu (fr)
- Dijkstra (fr)
- Vaynberg (fr)
- Baumann (fr)
- Pierce (fr)
- Koenig (fr)
- Novak (fr)
- Corbet (fr)
- TMR (fr)
- Auffray (fr)
- Bora (fr)
- Ricketts (fr)
- Andronick (fr)
- Beringer (fr)
- CERT (fr)
- COLLOMBET-GOURDON (fr)
- Certik.org (fr)
- Chlipala (fr)
- Cock (fr)
- DEPARIS (fr)
- De Millo (fr)
- Derrin (fr)
- EL HAFIDI (fr)
- Elkaduwe (fr)
- Elphinstone (fr)
- Engelhardt (fr)
- Ferraiuolo (fr)
- FÉVRIER (fr)
- Hawblitzel (fr)
- Heiser (fr)
- Hym (fr)
- Jomaa (fr)
- Kalagiakos (fr)
- Kolanski (fr)
- LinuxFoundation (fr)
- Lipton (fr)
- Mahboubi (fr)
- Malecha (fr)
- Norrish (fr)
- Parno (fr)
- Paturi V. (fr)
- Rakshit (fr)
- Ramananandro (fr)
- Reddy Kandukuri (fr)
- Sjöberg (fr)
- TREMBLAY (fr)
- Tuch (fr)
- Weirich (fr)
- Weng (fr)
- Winwood (fr)
- Zdancewic (fr)
- Ford (fr)
- Greg (fr)
- Grimaud (fr)
- Perlis (fr)
- Hoffmann (fr)
- Shao (fr)
- Chen (fr)
- Wu (fr)
- Costanzo (fr)
- Feng (fr)
- Kim (fr)
- Liang (fr)
- Zhang (fr)
- Lerner (fr)
- Appel (fr)
- Burke (fr)
- Alvarez (fr)
- Klein (fr)
- Nowak (fr)
- Sewell (fr)
- Gu (fr)
- Dijkstra (fr)
- Vaynberg (fr)
- Baumann (fr)
- Pierce (fr)
- Koenig (fr)
- Novak (fr)
- Corbet (fr)
- TMR (fr)
- Auffray (fr)
- Bora (fr)
- Ricketts (fr)
- Andronick (fr)
- Beringer (fr)
- CERT (fr)
- COLLOMBET-GOURDON (fr)
- Certik.org (fr)
- Chlipala (fr)
- Cock (fr)
- DEPARIS (fr)
- De Millo (fr)
- Derrin (fr)
- EL HAFIDI (fr)
- Elkaduwe (fr)
- Elphinstone (fr)
- Engelhardt (fr)
- Ferraiuolo (fr)
- FÉVRIER (fr)
- Hawblitzel (fr)
- Heiser (fr)
- Hym (fr)
- Jomaa (fr)
- Kalagiakos (fr)
- Kolanski (fr)
- LinuxFoundation (fr)
- Lipton (fr)
- Mahboubi (fr)
- Malecha (fr)
- Norrish (fr)
- Parno (fr)
- Paturi V. (fr)
- Rakshit (fr)
- Ramananandro (fr)
- Reddy Kandukuri (fr)
- Sjöberg (fr)
- TREMBLAY (fr)
- Tuch (fr)
- Weirich (fr)
- Weng (fr)
- Winwood (fr)
- Zdancewic (fr)
|
prop-fr:pages
|
- 517 (xsd:integer)
- ??-?? (fr)
|
prop-fr:prénom
|
- Jonathan (fr)
- T (fr)
- A. (fr)
- A. W. (fr)
- B. (fr)
- E. (fr)
- G. (fr)
- H. (fr)
- J. (fr)
- K. (fr)
- L. (fr)
- M. (fr)
- P. (fr)
- R. (fr)
- Christophe (fr)
- C. (fr)
- Chloé (fr)
- D. (fr)
- Dennis (fr)
- FR (fr)
- Gilles (fr)
- Tom (fr)
- N. (fr)
- S. (fr)
- US (fr)
- V. (fr)
- T. (fr)
- Xavier (fr)
- Z. (fr)
- X. (fr)
- B. C. (fr)
- Zhong (fr)
- Assia (fr)
- A.J (fr)
- Amjad (fr)
- Kroah-Hartman (fr)
- Laure-Lou (fr)
- M. M. (fr)
- R.A (fr)
- R.J (fr)
- S-C. (fr)
- Jonathan (fr)
- T (fr)
- A. (fr)
- A. W. (fr)
- B. (fr)
- E. (fr)
- G. (fr)
- H. (fr)
- J. (fr)
- K. (fr)
- L. (fr)
- M. (fr)
- P. (fr)
- R. (fr)
- Christophe (fr)
- C. (fr)
- Chloé (fr)
- D. (fr)
- Dennis (fr)
- FR (fr)
- Gilles (fr)
- Tom (fr)
- N. (fr)
- S. (fr)
- US (fr)
- V. (fr)
- T. (fr)
- Xavier (fr)
- Z. (fr)
- X. (fr)
- B. C. (fr)
- Zhong (fr)
- Assia (fr)
- A.J (fr)
- Amjad (fr)
- Kroah-Hartman (fr)
- Laure-Lou (fr)
- M. M. (fr)
- R.A (fr)
- R.J (fr)
- S-C. (fr)
|
prop-fr:périodique
|
- Springer (fr)
- Springer, Berlin, Heidelberg (fr)
- IEEE Xplore (fr)
- Compas 2018 (fr)
- INRIA Paris, September 17, 2018 (fr)
- The ACM Digital Library (fr)
- the Association for Computing Machinery (fr)
- the Royal Society (fr)
- Springer (fr)
- Springer, Berlin, Heidelberg (fr)
- IEEE Xplore (fr)
- Compas 2018 (fr)
- INRIA Paris, September 17, 2018 (fr)
- The ACM Digital Library (fr)
- the Association for Computing Machinery (fr)
- the Royal Society (fr)
|
prop-fr:site
| |
prop-fr:titre
|
- 2017 (xsd:integer)
- Global Embedded Systems Market Rises at 6.4% CAGR; Automotive Industry Powers Growth (fr)
- Multiples vulnérabilités de fuite d’informations dans des processeurs (fr)
- All Circuits are Busy Now: The 1990 AT&T Long Distance Network Collapse (fr)
- Le théorème des quatre couleurs et les preuves informatisées (fr)
- Deep Specifications and Certified Abstraction Layers (fr)
- Apple-Releases-Security-Updates-iCloud-iOS (fr)
- Certik (fr)
- Cisco-Releases-Security-Updates (fr)
- Cloud Security Issues (fr)
- Cloud security tactics: Virtualization and the VMM (fr)
- DeepSpec Summer School, Part 38, Shao (fr)
- DeepSpec Summer School, Part 40, Shao (fr)
- Keynote:Building Fully Trustworthy Smart Contracts and Blockchain Ecosystems (fr)
- Microsoft-Releases-November-2018-Security-Updates (fr)
- Modular Verification for Computer Security (fr)
- My Current Work on CertiKOS (fr)
- Position paper: the science of deep specification (fr)
- Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors (fr)
- Structured programming (fr)
- The CompCert C verified compiler (fr)
- The science of deep specification (fr)
- VMware-Releases-Security-Updates (fr)
- Vulnérabilité dans Wallix AdminBastion (fr)
- Characterizing Progress Properties of Concurrent Objects via Contextual Refinements (fr)
- Social processes and proofs of theorems and programs (fr)
- seL4: Formal Verification of an OS Kernel (fr)
- Compositional Verification of a Baby Virtual Memory Manager (fr)
- Multiples vulnérabilités dans le noyau Linux d’Ubuntu (fr)
- CertiKOS: an extensible architecture for building certified concurrent OS kernels (fr)
- La conception d’un noyau orientée par sa preuve d’isolation mémoire (fr)
- CertiKOS: a certified kernel for secure cloud computing (fr)
- Komodo: Using verification to disentangle secure-enclave hardware from software (fr)
- Formal Proof of Dynamic Memory Isolation Based on MMU (fr)
- Towards foundational verification of cyber-physical systems (fr)
- Un ordinateur pour vérifier les preuves mathématiques (fr)
- Chiffres clés : les ventes de mobiles et de smartphones (fr)
- Toyota's killer firmware: Bad design and its consequences (fr)
|
prop-fr:url
| |
prop-fr:volume
|
- 7679 (xsd:integer)
- Juillet 2018 (fr)
|
prop-fr:wikiPageUsesTemplate
| |
dct:subject
| |
rdfs:comment
|
- 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’exploitation certifiés. Son approche se fait autour de la définition et la Certification de couches d'abstraction, elles-mêmes basées sur la sémantique de spécification riche (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 (fr)
- 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’exploitation certifiés. Son approche se fait autour de la définition et la Certification de couches d'abstraction, elles-mêmes basées sur la sémantique de spécification riche (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 (fr)
|
rdfs:label
|
- CertiKOS (fr)
- CertiKOS (fr)
|
owl:sameAs
| |
prov:wasDerivedFrom
| |
foaf:depiction
| |
foaf:isPrimaryTopicOf
| |
is oa:hasTarget
of | |
is foaf:primaryTopic
of | |