| http://dbpedia.org/ontology/abstract
|
CertiKOS est un projet développé par Zhong … 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é) . couches d'abstraction (la simultanéité) .
|
| http://dbpedia.org/ontology/thumbnail
|
http://commons.wikimedia.org/wiki/Special:FilePath/Raffinement_contextuel.jpg?width=300 +
|
| http://dbpedia.org/ontology/wikiPageExternalLink
|
https://www.us-cert.gov/ +
, https://www.us-cert.gov/ncas/current-activity/2018/11/13/Microsoft-Releases-November-2018-Security-Updates +
, https://www.us-cert.gov/ncas/current-activity/2018/11/22/VMware-Releases-Security-Updates +
, https://www.linuxfoundation.org/2017-linux-kernel-report-landing-page/ +
, https://www.us-cert.gov/ncas/current-activity/2018/10/31/Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors +
, https://www.us-cert.gov/ncas/current-activity/2018/11/07/Cisco-Releases-Security-Updates +
, https://www.edn.com/design/automotive/4423428/Toyota-s-killer-firmware--Bad-design-and-its-consequences +
, https://www.cert.ssi.gouv.fr +
, https://controverses.github.io/4CTpreuvesinformatiques/%23main +
, https://www.cert.ssi.gouv.fr/avis/CERTFR-2018-AVI-581/ +
, https://www.cert.ssi.gouv.fr/alerte/CERTFR-2018-ALE-001/ +
, https://certik.org/ +
, https://www.cert.ssi.gouv.fr/alerte/CERTFR-2018-ALE-012/ +
, http://images.math.cnrs.fr/Un-ordinateur-pour-verifier-les.html +
, https://www.youtube.com/watch%3Fv=ibdjeEHSF54&t=756s +
, https://www.youtube.com/watch%3Fv=RHXpz2ZJ-w0 +
, https://pdfs.semanticscholar.org/0dd7/9b76356624f5f3d7df27721fb4c44c95f0f0.pdf +
, http://users.csc.calpoly.edu/~jdalbey/SWE/Papers/att_collapse +
, https://www.zdnet.fr/actualites/chiffres-cles-les-ventes-de-mobiles-et-de-smartphones-39789928.htm +
, https://www.us-cert.gov/ncas/current-activity/2018/11/07/Apple-Releases-Security-Updates-iCloud-iOS +
, https://www.transparencymarketresearch.com/pressrelease/embedded-system.htm +
, https://www.youtube.com/watch%3Fv=2df39-QA4x0 +
, https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf +
|
| http://dbpedia.org/ontology/wikiPageID
|
12297843
|
| http://dbpedia.org/ontology/wikiPageLength
|
38636
|
| http://dbpedia.org/ontology/wikiPageRevisionID
|
189344097
|
| http://dbpedia.org/ontology/wikiPageWikiLink
|
http://fr.dbpedia.org/resource/Bug_%28informatique%29 +
, http://fr.dbpedia.org/resource/Syst%C3%A8me_d%27exploitation +
, http://fr.dbpedia.org/resource/Trivial_%28math%C3%A9matiques%29 +
, http://fr.dbpedia.org/resource/Vuln%C3%A9rabilit%C3%A9_%28informatique%29 +
, http://fr.dbpedia.org/resource/Defense_Advanced_Research_Projects_Agency +
, http://fr.dbpedia.org/resource/M%C3%A9thode_formelle_%28informatique%29 +
, http://fr.dbpedia.org/resource/Linux +
, http://fr.dbpedia.org/resource/Hyperviseur +
, http://fr.dbpedia.org/resource/Fichier:Raffinement_contextuel.jpg +
, http://fr.dbpedia.org/resource/Injection_de_code +
, http://fr.dbpedia.org/resource/Unit%C3%A9_de_gestion_de_m%C3%A9moire +
, http://fr.dbpedia.org/resource/Microprocesseur_multi-c%C5%93ur +
, http://fr.dbpedia.org/resource/Processeur +
, http://fr.dbpedia.org/resource/Smartphone +
, http://fr.dbpedia.org/resource/Assistant_de_preuve +
, http://fr.dbpedia.org/resource/Drone +
, http://fr.dbpedia.org/resource/Programme_informatique +
, http://fr.dbpedia.org/resource/Espace_utilisateur +
, http://fr.dbpedia.org/resource/Cloud_computing +
, http://fr.dbpedia.org/resource/Transparency_Market_Research +
, http://fr.dbpedia.org/resource/Cat%C3%A9gorie:Informatique +
, http://fr.dbpedia.org/resource/Pointeur_%28programmation%29 +
, http://fr.dbpedia.org/resource/Connecticut +
, http://fr.dbpedia.org/resource/Coq_%28logiciel%29 +
, http://fr.dbpedia.org/resource/Universit%C3%A9_Yale +
, http://fr.dbpedia.org/resource/Certification +
, http://fr.dbpedia.org/resource/Cat%C3%A9gorie:M%C3%A9thodologie +
, http://fr.dbpedia.org/resource/Cat%C3%A9gorie:M%C3%A9thode_formelle +
, http://fr.dbpedia.org/resource/S%C3%A9curit%C3%A9_des_syst%C3%A8mes_d%27information +
, http://fr.dbpedia.org/resource/Superordinateur +
, http://fr.dbpedia.org/resource/Abstraction_%28informatique%29 +
, http://fr.dbpedia.org/resource/Fichier:Modules_Noyau_2.jpg +
, http://fr.dbpedia.org/resource/ZDNet +
, http://fr.dbpedia.org/resource/S%C3%A9mantique_des_langages_de_programmation +
, http://fr.dbpedia.org/resource/Fondation_Linux +
, http://fr.dbpedia.org/resource/Analyse_statique_de_programmes +
, http://fr.dbpedia.org/resource/Linuxfoundation +
, http://fr.dbpedia.org/resource/Noyau_de_syst%C3%A8me_d%27exploitation +
, http://fr.dbpedia.org/resource/Fichier:Allocation_ressources_CertiKOS.jpg +
, http://fr.dbpedia.org/resource/Noyau_Linux +
, http://fr.dbpedia.org/resource/Implication_%28logique%29 +
, http://fr.dbpedia.org/resource/Cat%C3%A9gorie:Logique_formelle +
, http://fr.dbpedia.org/resource/Code_source +
, http://fr.dbpedia.org/resource/X86 +
, http://fr.dbpedia.org/resource/Th%C3%A9orie_axiomatique +
, http://fr.dbpedia.org/resource/Fichier:Comportement_contextuel.jpg +
, http://fr.dbpedia.org/resource/Spinlock +
, http://fr.dbpedia.org/resource/Raffinement +
, http://fr.dbpedia.org/resource/Assembleur +
, http://fr.dbpedia.org/resource/Syst%C3%A8me_embarqu%C3%A9 +
, http://fr.dbpedia.org/resource/Lemme_%28math%C3%A9matiques%29 +
, http://fr.dbpedia.org/resource/Edsger_Dijkstra +
, http://fr.dbpedia.org/resource/Compilateur +
, http://fr.dbpedia.org/resource/Preuve +
, http://fr.dbpedia.org/resource/M%C3%A9moire_vive +
, http://fr.dbpedia.org/resource/Domotique +
, http://fr.dbpedia.org/resource/Communication_inter-processus +
, http://fr.dbpedia.org/resource/M%C3%A9moire_tampon +
|
| http://fr.dbpedia.org/property/année
|
2018
, 2016
, 2017
, 2011
, 2009
, 2015
, 2012
, 2013
, 1979
|
| http://fr.dbpedia.org/property/auteur
|
Christophe Auffray
, Transparency Market Research
|
| http://fr.dbpedia.org/property/consultéLe
|
Décembre 2018
, Novembre 2018
|
| http://fr.dbpedia.org/property/date
|
Novembre 2018
, "2018-11-26"^^xsd:date
, 2017
|
| http://fr.dbpedia.org/property/doi
|
10.1145
, 10.1098
, ??
, 10.1109
, 10.1007
|
| http://fr.dbpedia.org/property/hal
|
hal-01819955
|
| http://fr.dbpedia.org/property/id
|
US-CERT2018-4
, Certik
, Liang2013
, FR-CERT2018-1
, US-CERT2018-5
, Reddy2009
, Appel2017
, TMR2018
, Vaynberg2012
, US-CERT2018-2
, Jomaa2016
, Shao
, LinuxFoundation2017
, Klein2009
, AT&T
, Gu2015
, US-CERT2018-3
, Malecha2016
, github
, Appel2016
, Vaynberg2011
, US-CERT2018-1
, Pierce2016
, Shao2017-1
, Toyota2013
, Shao2017-2
, cnrs
, Auffray2018
, Kalagiakos2012
, FR-CERT2018-2
, Ferraiuolo2017
, FR-CERT2018-3
, Jomaa2018
, Shao2016
, De Millo1979
, Ronghui Gu
, The CompCert C verified compiler
, Dijkstra1979
|
| http://fr.dbpedia.org/property/isbn
|
978
, 0
|
| http://fr.dbpedia.org/property/isnn
|
1471
|
| http://fr.dbpedia.org/property/lang
|
fr
, en
|
| http://fr.dbpedia.org/property/lireEnLigne
|
https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf +
|
| http://fr.dbpedia.org/property/mois
|
Avril
, décembre
, October
, January
, Octobre
, july
, Janvier
, octobre
, septembre
, August
, Décembre
, november
, September
, May
|
| http://fr.dbpedia.org/property/nom
|
FÉVRIER
, EL HAFIDI
, Dijkstra
, Greg
, Chlipala
, Auffray
, Norrish
, Chen
, Klein
, CERT
, Lipton
, Ramananandro
, Ricketts
, Burke
, Engelhardt
, Beringer
, Hym
, Parno
, Wu
, Liang
, Corbet
, Kolanski
, LinuxFoundation
, Winwood
, Ferraiuolo
, Weng
, Feng
, Costanzo
, Baumann
, Jomaa
, Lerner
, Bora
, Cock
, Derrin
, Kim
, TREMBLAY
, Ford
, Hawblitzel
, Grimaud
, Hoffmann
, Shao
, Malecha
, Sewell
, DEPARIS
, De Millo
, Perlis
, Rakshit
, Zdancewic
, Zhang
, COLLOMBET-GOURDON
, Paturi V.
, Alvarez
, Reddy Kandukuri
, Kalagiakos
, Elphinstone
, Koenig
, Mahboubi
, Gu
, Sjöberg
, Appel
, Pierce
, Nowak
, TMR
, Vaynberg
, Elkaduwe
, Heiser
, Novak
, Tuch
, Certik.org
, Andronick
, Weirich
|
| http://fr.dbpedia.org/property/pages
|
??-??
, 517
|
| http://fr.dbpedia.org/property/prénom
|
T.
, R.
, X.
, Z.
, Kroah-Hartman
, Jonathan
, Laure-Lou
, Tom
, S-C.
, R.A
, Dennis
, C.
, T
, D.
, FR
, H.
, K.
, Chloé
, B. C.
, Amjad
, Xavier
, G.
, P.
, Christophe
, M. M.
, US
, V.
, M.
, E.
, A.
, A.J
, B.
, Zhong
, R.J
, L.
, Assia
, Gilles
, J.
, S.
, N.
, A. W.
|
| http://fr.dbpedia.org/property/périodique
|
the Royal Society
, the Association for Computing Machinery
, Springer
, Springer, Berlin, Heidelberg
, The ACM Digital Library
, Compas 2018
, INRIA Paris, September 17, 2018
, IEEE Xplore
|
| http://fr.dbpedia.org/property/site
|
http://fr.dbpedia.org/resource/Linuxfoundation +
, http://fr.dbpedia.org/resource/ZDNet +
, http://fr.dbpedia.org/resource/Transparency_Market_Research +
|
| http://fr.dbpedia.org/property/titre
|
The science of deep specification
, DeepSpec Summer School, Part 40, Shao
, Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors
, La conception d’un noyau orientée par sa preuve d’isolation mémoire
, The CompCert C verified compiler
, Position paper: the science of deep specification
, Structured programming
, Towards foundational verification of cyber-physical systems
, My Current Work on CertiKOS
, Cloud Security Issues
, Apple-Releases-Security-Updates-iCloud-iOS
, seL4: Formal Verification of an OS Kernel
, Modular Verification for Computer Security
, Cisco-Releases-Security-Updates
, Chiffres clés : les ventes de mobiles et de smartphones
, Cloud security tactics: Virtualization and the VMM
, Multiples vulnérabilités dans le noyau Linux d’Ubuntu
, Formal Proof of Dynamic Memory Isolation Based on MMU
, Characterizing Progress Properties of Concurrent Objects via Contextual Refinements
, Un ordinateur pour vérifier les preuves mathématiques
, Komodo: Using verification to disentangle secure-enclave hardware from software
, Vulnérabilité dans Wallix AdminBastion
, Compositional Verification of a Baby Virtual Memory Manager
, VMware-Releases-Security-Updates
, Multiples vulnérabilités de fuite d’informations dans des processeurs
, Le théorème des quatre couleurs et les preuves informatisées
, Keynote：Building Fully Trustworthy Smart Contracts and Blockchain Ecosystems
, Microsoft-Releases-November-2018-Security-Updates
, CertiKOS: a certified kernel for secure cloud computing
, Certik
, Global Embedded Systems Market Rises at 6.4% CAGR; Automotive Industry Powers Growth
, Deep Specifications and Certified Abstraction Layers
, Toyota's killer firmware: Bad design and its consequences
, Social processes and proofs of theorems and programs
, All Circuits are Busy Now: The 1990 AT&T Long Distance Network Collapse
, 2017
, CertiKOS: an extensible architecture for building certified concurrent OS kernels
, DeepSpec Summer School, Part 38, Shao
|
| http://fr.dbpedia.org/property/url
|
https://www.zdnet.fr/actualites/chiffres-cles-les-ventes-de-mobiles-et-de-smartphones-39789928.htm +
, https://www.us-cert.gov/ncas/current-activity/2018/11/07/Apple-Releases-Security-Updates-iCloud-iOS +
, http://users.csc.calpoly.edu/~jdalbey/SWE/Papers/att_collapse +
, https://www.us-cert.gov/ncas/current-activity/2018/10/31/Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors +
, https://www.us-cert.gov/ncas/current-activity/2018/11/07/Cisco-Releases-Security-Updates +
, https://www.us-cert.gov/ncas/current-activity/2018/11/13/Microsoft-Releases-November-2018-Security-Updates +
, https://www.us-cert.gov/ncas/current-activity/2018/11/22/VMware-Releases-Security-Updates +
, https://www.transparencymarketresearch.com/pressrelease/embedded-system.htm +
, https://pdfs.semanticscholar.org/0dd7/9b76356624f5f3d7df27721fb4c44c95f0f0.pdf +
, https://www.edn.com/design/automotive/4423428/Toyota-s-killer-firmware--Bad-design-and-its-consequences +
, https://www.cert.ssi.gouv.fr/alerte/CERTFR-2018-ALE-001/ +
, https://www.cert.ssi.gouv.fr/avis/CERTFR-2018-AVI-581/ +
, https://controverses.github.io/4CTpreuvesinformatiques/%23main +
, https://www.youtube.com/watch%3Fv=RHXpz2ZJ-w0 +
, http://images.math.cnrs.fr/Un-ordinateur-pour-verifier-les.html +
, https://certik.org/ +
, https://www.linuxfoundation.org/2017-linux-kernel-report-landing-page/ +
, https://www.cert.ssi.gouv.fr/alerte/CERTFR-2018-ALE-012/ +
, https://www.youtube.com/watch%3Fv=2df39-QA4x0 +
, 756.0
|
| http://fr.dbpedia.org/property/volume
|
7679
, Juillet 2018
|
| http://fr.dbpedia.org/property/wikiPageUsesTemplate
|
http://fr.dbpedia.org/resource/Mod%C3%A8le:R%C3%A9f%C3%A9rences +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:Portail +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:Plume +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:Lien_web +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:Palette +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:3e +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:%2C +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:Article +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:Unit%C3%A9 +
, http://fr.dbpedia.org/resource/Mod%C3%A8le:Tmp +
|
| http://purl.org/dc/terms/subject
|
http://fr.dbpedia.org/resource/Cat%C3%A9gorie:M%C3%A9thode_formelle +
, http://fr.dbpedia.org/resource/Cat%C3%A9gorie:Logique_formelle +
, http://fr.dbpedia.org/resource/Cat%C3%A9gorie:M%C3%A9thodologie +
, http://fr.dbpedia.org/resource/Cat%C3%A9gorie:Informatique +
|
| http://www.w3.org/ns/prov#wasDerivedFrom
|
http://fr.wikipedia.org/wiki/CertiKOS?oldid=189344097&ns=0 +
|
| http://xmlns.com/foaf/0.1/depiction
|
http://commons.wikimedia.org/wiki/Special:FilePath/Comportement_contextuel.jpg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Raffinement_contextuel.jpg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Modules_Noyau_2.jpg +
, http://commons.wikimedia.org/wiki/Special:FilePath/Allocation_ressources_CertiKOS.jpg +
|
| http://xmlns.com/foaf/0.1/isPrimaryTopicOf
|
http://fr.wikipedia.org/wiki/CertiKOS +
|
| owl:sameAs |
http://www.wikidata.org/entity/Q60965189 +
, http://g.co/kg/g/11gyc22vk1 +
, http://fr.dbpedia.org/resource/CertiKOS +
|
| rdfs:comment |
CertiKOS est un projet développé par Zhong … 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 utilisation de CompCertX. CertiKOS permet
|
| rdfs:label |
CertiKOS
|
