About DBpedia Fr

About: http://fr.dbpedia.org/resource/CertiKOS

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

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

thumbnail
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
  • 12297843 (xsd:integer)
dbo:wikiPageLength
  • 38636 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 189344097 (xsd:integer)
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
  • 1471 (xsd:integer)
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
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