CINXE.COM

<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available" lang="fr" dir="ltr"> <head> <meta charset="UTF-8"> <title>CertiKOS — Wikipédia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available";var cookie=document.cookie.match(/(?:^|; )frwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":[",\t."," \t,"],"wgDigitTransformTable":["",""], "wgDefaultDateFormat":"dmy","wgMonthNames":["","janvier","février","mars","avril","mai","juin","juillet","août","septembre","octobre","novembre","décembre"],"wgRequestId":"ba9f0e99-4f2d-4fe9-a9d0-f569680ddac9","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"CertiKOS","wgTitle":"CertiKOS","wgCurRevisionId":212292887,"wgRevisionId":212292887,"wgArticleId":12297843,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Article contenant un appel à traduction en anglais","Portail:Sciences de l'information et des bibliothèques/Articles liés","Portail:Sciences humaines et sociales/Articles liés","Portail:Informatique/Articles liés","Portail:Technologies/Articles liés","Portail:Informatique théorique/Articles liés","Projet:Mathématiques/Articles","Portail:Sécurité informatique/Articles liés","Portail:Sécurité de l'information/Articles liés","Informatique", "Méthodologie","Méthode formelle","Logique formelle"],"wgPageViewLanguage":"fr","wgPageContentLanguage":"fr","wgPageContentModel":"wikitext","wgRelevantPageName":"CertiKOS","wgRelevantArticleId":12297843,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":true,"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"fr","pageLanguageDir":"ltr","pageVariantFallbacks":"fr"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":true,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":40000,"wgRelatedArticlesCompat":[],"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q60965189", "wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false,"wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.cite.styles":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","mediawiki.page.media","site","mediawiki.page.ready","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ArchiveLinks" ,"ext.gadget.Wdsearch","ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader","ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.growthExperiments.SuggestedEditSession","wikibase.sidebar.tracking"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=fr&modules=ext.cite.styles%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediaBadges%7Cext.wikimediamessages.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=fr&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=fr&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.5"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="CertiKOS — Wikipédia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//fr.m.wikipedia.org/wiki/CertiKOS"> <link rel="alternate" type="application/x-wiki" title="Modifier" href="/w/index.php?title=CertiKOS&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipédia (fr)"> <link rel="EditURI" type="application/rsd+xml" href="//fr.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://fr.wikipedia.org/wiki/CertiKOS"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.fr"> <link rel="alternate" type="application/atom+xml" title="Flux Atom de Wikipédia" href="/w/index.php?title=Sp%C3%A9cial:Modifications_r%C3%A9centes&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-CertiKOS rootpage-CertiKOS skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Aller au contenu</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Menu principal" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Menu principal</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Menu principal</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">masquer</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Wikip%C3%A9dia:Accueil_principal" title="Accueil général [z]" accesskey="z"><span>Accueil</span></a></li><li id="n-thema" class="mw-list-item"><a href="/wiki/Portail:Accueil"><span>Portails thématiques</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Page_au_hasard" title="Affiche un article au hasard [x]" accesskey="x"><span>Article au hasard</span></a></li><li id="n-contact" class="mw-list-item"><a href="/wiki/Wikip%C3%A9dia:Contact"><span>Contact</span></a></li> </ul> </div> </div> <div id="p-Contribuer" class="vector-menu mw-portlet mw-portlet-Contribuer" > <div class="vector-menu-heading"> Contribuer </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-aboutwp" class="mw-list-item"><a href="/wiki/Aide:D%C3%A9buter"><span>Débuter sur Wikipédia</span></a></li><li id="n-help" class="mw-list-item"><a href="/wiki/Aide:Accueil" title="Accès à l’aide"><span>Aide</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikip%C3%A9dia:Accueil_de_la_communaut%C3%A9" title="À propos du projet, ce que vous pouvez faire, où trouver les informations"><span>Communauté</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Modifications_r%C3%A9centes" title="Liste des modifications récentes sur le wiki [r]" accesskey="r"><span>Modifications récentes</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Wikip%C3%A9dia:Accueil_principal" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipédia" src="/static/images/mobile/copyright/wikipedia-wordmark-fr.svg" style="width: 7.4375em; height: 1.125em;"> <img class="mw-logo-tagline" alt="l'encyclopédie libre" src="/static/images/mobile/copyright/wikipedia-tagline-fr.svg" width="120" height="13" style="width: 7.5em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Sp%C3%A9cial:Recherche" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Rechercher sur Wikipédia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Rechercher</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Rechercher sur Wikipédia" aria-label="Rechercher sur Wikipédia" autocapitalize="sentences" title="Rechercher sur Wikipédia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Spécial:Recherche"> </div> <button class="cdx-button cdx-search-input__end-button">Rechercher</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Outils personnels"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Apparence"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Modifier l'apparence de la taille, de la largeur et de la couleur de la police de la page" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Apparence" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Apparence</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="//donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_fr.wikipedia.org&uselang=fr" class=""><span>Faire un don</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Sp%C3%A9cial:Cr%C3%A9er_un_compte&returnto=CertiKOS" title="Nous vous encourageons à créer un compte utilisateur et vous connecter ; ce n’est cependant pas obligatoire." class=""><span>Créer un compte</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Sp%C3%A9cial:Connexion&returnto=CertiKOS" title="Nous vous encourageons à vous connecter ; ce n’est cependant pas obligatoire. [o]" accesskey="o" class=""><span>Se connecter</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Plus d’options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Outils personnels" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Outils personnels</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="Menu utilisateur" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="//donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_fr.wikipedia.org&uselang=fr"><span>Faire un don</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Cr%C3%A9er_un_compte&returnto=CertiKOS" title="Nous vous encourageons à créer un compte utilisateur et vous connecter ; ce n’est cependant pas obligatoire."><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Créer un compte</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Connexion&returnto=CertiKOS" title="Nous vous encourageons à vous connecter ; ce n’est cependant pas obligatoire. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Se connecter</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages pour les contributeurs déconnectés <a href="/wiki/Aide:Premiers_pas" aria-label="En savoir plus sur la contribution"><span>en savoir plus</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Mes_contributions" title="Une liste des modifications effectuées depuis cette adresse IP [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Mes_discussions" title="La page de discussion pour les contributions depuis cette adresse IP [n]" accesskey="n"><span>Discussion</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Sommaire" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Sommaire</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">masquer</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">Début</div> </a> </li> <li id="toc-Motivations_et_enjeux" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Motivations_et_enjeux"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>Motivations et enjeux</span> </div> </a> <ul id="toc-Motivations_et_enjeux-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-La_philosophie_de_Certikos" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#La_philosophie_de_Certikos"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>La philosophie de Certikos</span> </div> </a> <button aria-controls="toc-La_philosophie_de_Certikos-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Afficher / masquer la sous-section La philosophie de Certikos</span> </button> <ul id="toc-La_philosophie_de_Certikos-sublist" class="vector-toc-list"> <li id="toc-Certification_du_Noyau" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Certification_du_Noyau"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.1</span> <span>Certification du Noyau</span> </div> </a> <ul id="toc-Certification_du_Noyau-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Spécifications_profondes" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Spécifications_profondes"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.2</span> <span>Spécifications profondes</span> </div> </a> <ul id="toc-Spécifications_profondes-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Certification_du_code_informatique:_CompCertX" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Certification_du_code_informatique:_CompCertX"> <div class="vector-toc-text"> <span class="vector-toc-numb">2.3</span> <span>Certification du code informatique: CompCertX</span> </div> </a> <ul id="toc-Certification_du_code_informatique:_CompCertX-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Implémentation_de_CertiKOS" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Implémentation_de_CertiKOS"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>Implémentation de CertiKOS</span> </div> </a> <button aria-controls="toc-Implémentation_de_CertiKOS-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Afficher / masquer la sous-section Implémentation de CertiKOS</span> </button> <ul id="toc-Implémentation_de_CertiKOS-sublist" class="vector-toc-list"> <li id="toc-Au_travers_d'un_Hyperviseur_Certifié" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Au_travers_d'un_Hyperviseur_Certifié"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1</span> <span>Au travers d'un Hyperviseur Certifié</span> </div> </a> <ul id="toc-Au_travers_d'un_Hyperviseur_Certifié-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Au_travers_d'un_Noyau_Certifié:_mCertiKOS,_mC2" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Au_travers_d'un_Noyau_Certifié:_mCertiKOS,_mC2"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.2</span> <span>Au travers d'un Noyau Certifié: mCertiKOS, mC2</span> </div> </a> <ul id="toc-Au_travers_d'un_Noyau_Certifié:_mCertiKOS,_mC2-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-Références" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Références"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>Références</span> </div> </a> <ul id="toc-Références-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Bibliographie" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Bibliographie"> <div class="vector-toc-text"> <span class="vector-toc-numb">5</span> <span>Bibliographie</span> </div> </a> <ul id="toc-Bibliographie-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Liens_externes" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Liens_externes"> <div class="vector-toc-text"> <span class="vector-toc-numb">6</span> <span>Liens externes</span> </div> </a> <ul id="toc-Liens_externes-sublist" class="vector-toc-list"> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Sommaire" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Basculer la table des matières" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Basculer la table des matières</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">CertiKOS</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="Cet article n’existe que dans cette langue. Ajouter l’article pour d’autres langues." > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-0" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">Ajouter des langues</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> <div class="after-portlet after-portlet-lang"><span class="uls-after-portlet-link"></span><span class="wb-langlinks-add wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q60965189#sitelinks-wikipedia" title="Ajouter des liens interlangues" class="wbc-editpage">Ajouter des liens</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Espaces de noms"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/CertiKOS" title="Voir le contenu de la page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Discussion:CertiKOS" rel="discussion" title="Discussion au sujet de cette page de contenu [t]" accesskey="t"><span>Discussion</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Modifier la variante de langue" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">français</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Affichages"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/CertiKOS"><span>Lire</span></a></li><li id="ca-ve-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=CertiKOS&veaction=edit" title="Modifier cette page [v]" accesskey="v"><span>Modifier</span></a></li><li id="ca-edit" class="collapsible vector-tab-noicon mw-list-item"><a href="/w/index.php?title=CertiKOS&action=edit" title="Modifier le wikicode de cette page [e]" accesskey="e"><span>Modifier le code</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=CertiKOS&action=history" title="Historique des versions de cette page [h]" accesskey="h"><span>Voir l’historique</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Outils de la page"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Outils" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Outils</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Outils</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">masquer</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="Plus d’options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/CertiKOS"><span>Lire</span></a></li><li id="ca-more-ve-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=CertiKOS&veaction=edit" title="Modifier cette page [v]" accesskey="v"><span>Modifier</span></a></li><li id="ca-more-edit" class="collapsible vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=CertiKOS&action=edit" title="Modifier le wikicode de cette page [e]" accesskey="e"><span>Modifier le code</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=CertiKOS&action=history"><span>Voir l’historique</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> Général </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Pages_li%C3%A9es/CertiKOS" title="Liste des pages liées qui pointent sur celle-ci [j]" accesskey="j"><span>Pages liées</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Suivi_des_liens/CertiKOS" rel="nofollow" title="Liste des modifications récentes des pages appelées par celle-ci [k]" accesskey="k"><span>Suivi des pages liées</span></a></li><li id="t-upload" class="mw-list-item"><a href="/wiki/Aide:Importer_un_fichier" title="Téléverser des fichiers [u]" accesskey="u"><span>Téléverser un fichier</span></a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Sp%C3%A9cial:Pages_sp%C3%A9ciales" title="Liste de toutes les pages spéciales [q]" accesskey="q"><span>Pages spéciales</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=CertiKOS&oldid=212292887" title="Adresse permanente de cette version de cette page"><span>Lien permanent</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=CertiKOS&action=info" title="Davantage d’informations sur cette page"><span>Informations sur la page</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Citer&page=CertiKOS&id=212292887&wpFormIdentifier=titleform" title="Informations sur la manière de citer cette page"><span>Citer cette page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:UrlShortener&url=https%3A%2F%2Ffr.wikipedia.org%2Fwiki%2FCertiKOS"><span>Obtenir l'URL raccourcie</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:QrCode&url=https%3A%2F%2Ffr.wikipedia.org%2Fwiki%2FCertiKOS"><span>Télécharger le code QR</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Imprimer / exporter </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-create_a_book" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:Livre&bookcmd=book_creator&referer=CertiKOS"><span>Créer un livre</span></a></li><li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Sp%C3%A9cial:DownloadAsPdf&page=CertiKOS&action=show-download-screen"><span>Télécharger comme PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=CertiKOS&printable=yes" title="Version imprimable de cette page [p]" accesskey="p"><span>Version imprimable</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> Dans d’autres projets </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q60965189" title="Lien vers l’élément dans le dépôt de données connecté [g]" accesskey="g"><span>Élément Wikidata</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Outils de la page"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Apparence"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Apparence</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">déplacer vers la barre latérale</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">masquer</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">Un article de Wikipédia, l'encyclopédie libre.</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="fr" dir="ltr"><p><b>CertiKOS</b> est un projet développé par Zhong Shao, professeur à l'<a href="/wiki/Universit%C3%A9_Yale" title="Université Yale">Université de Yale</a>, dans le <a href="/wiki/Connecticut" title="Connecticut">Connecticut</a>, avec la participation d'une équipe de 6 autres chercheurs. CertiKOS (<i>Certified Kit Operating System</i>) est un outil méthodologique de conception et de développement de <a href="/wiki/Syst%C3%A8me_d%27exploitation" title="Système d'exploitation">systèmes d’exploitation</a> certifiés. Son approche se fait autour de la définition et la <a href="/wiki/Certification" title="Certification">Certification</a> de couches d'<a href="/wiki/Abstraction_(informatique)" title="Abstraction (informatique)">abstraction</a>, elles-mêmes basées sur la <a href="/wiki/S%C3%A9mantique_des_langages_de_programmation" title="Sémantique des langages de programmation">sémantique</a> de spécification riche (spécifications profondes). Ces procédés répondent à ce qui peut être considéré comme une loi fondamentale, un <a href="/wiki/Raffinement" title="Raffinement">raffinement</a> contextuel fort. Cette méthodologie permet non seulement de certifier toute la sémantique (par l'<a href="/wiki/Assistant_de_preuve" title="Assistant de preuve">assistant de preuve</a> de <a href="/wiki/Coq_(logiciel)" title="Coq (logiciel)">Coq</a>) mais également de certifier la <a href="/wiki/Compilateur" title="Compilateur">compilation</a> grâce à l'utilisation de CompCertX. CertiKOS permet de développer un <a href="/wiki/Hyperviseur" title="Hyperviseur">hyperviseur</a> et plusieurs <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">noyaux</a> certifiés, dont mC2. Ce dernier prenant en charge des <a href="/wiki/Microprocesseur_multi-c%C5%93ur" title="Microprocesseur multi-cœur">processeurs multi-cœurs</a>, ainsi que l'exécution entrelacée de modules noyau / utilisateur sur différentes couches d'abstraction (la simultanéité) . </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="Motivations_et_enjeux">Motivations et enjeux</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=1" title="Modifier la section : Motivations et enjeux" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=1" title="Modifier le code source de la section : Motivations et enjeux"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Les <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">noyaux</a>, <a href="/wiki/Syst%C3%A8me_d%27exploitation" title="Système d'exploitation">systèmes d’exploitation</a>, hyperviseurs (etc.) sont des <a href="/wiki/Programme_informatique" title="Programme informatique">logiciels/programmes</a>, une succession de lignes de <a href="/wiki/Code_source" title="Code source">code</a>, qui une fois compilée et interprétée par la machine, rend un service à l’utilisateur. Ils se retrouvent aujourd'hui dans nos <a href="/wiki/Smartphone" title="Smartphone">smartphones</a>, voitures, <a href="/wiki/Drone" title="Drone">drones</a>, ordinateurs, avions, systèmes bancaires ou <a href="/wiki/Domotique" title="Domotique">domotiques</a>... Selon le rapport 2017 de <a href="/wiki/Fondation_Linux" title="Fondation Linux">The Linux Foundation</a>, le <a href="/wiki/Syst%C3%A8me_d%27exploitation" title="Système d'exploitation">Système d'exploitation</a> Linux exécute près de 90 % de la charge de travail du <a href="/wiki/Cloud_computing" title="Cloud computing">cloud</a> public, couvre 62 % de la part de marché de la technologie <a href="/wiki/Syst%C3%A8me_embarqu%C3%A9" title="Système embarqué">embarquée</a> et 99 % de celle des <a href="/wiki/Superordinateur" title="Superordinateur">superordinateurs</a>. Il est présent sur 82 % des smartphones<sup id="cite_ref-Linux_p3_1-0" class="reference"><a href="#cite_note-Linux_p3-1"><span class="cite_crochet">[</span>1<span class="cite_crochet">]</span></a></sup>. International Data Corporation (IDC) rapporte qu'il s'est vendu près de 355.2 millions de smartphones dans le monde, au <abbr class="abbr" title="Troisième">3<sup>e</sup></abbr> trimestre 2018<sup id="cite_ref-Auffray2018Auffray20181_2-0" class="reference"><a href="#cite_note-Auffray2018Auffray20181-2"><span class="cite_crochet">[</span>2<span class="cite_crochet">]</span></a></sup>, soit près de 45 smartphones par seconde. L'impact est donc important mais l'enjeu financier est également présent. À 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<sup id="cite_ref-TMR2018TMR20181_3-0" class="reference"><a href="#cite_note-TMR2018TMR20181-3"><span class="cite_crochet">[</span>3<span class="cite_crochet">]</span></a></sup>. 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 <a href="/wiki/S%C3%A9curit%C3%A9_des_syst%C3%A8mes_d%27information" title="Sécurité des systèmes d'information">sécurisés</a>. </p><p>Les systèmes d'exploitation constituent l'épine dorsale des systèmes logiciels et des éléments particulièrement critiques, pour la sécurité dans le monde<sup id="cite_ref-Shao2016Shao2016653_4-0" class="reference"><a href="#cite_note-Shao2016Shao2016653-4"><span class="cite_crochet">[</span>4<span class="cite_crochet">]</span></a></sup>. En effet, ces systèmes ne permettent pas toujours à la machine de rendre le service pour lequel ils sont conçus. Cela peut être dû à des défauts d’écriture dans le code, des défauts de conception<sup id="cite_ref-Toyota2013Toyota20131_5-0" class="reference"><a href="#cite_note-Toyota2013Toyota20131-5"><span class="cite_crochet">[</span>5<span class="cite_crochet">]</span></a></sup>, ou même à des interactions avec d’autres logiciels<sup id="cite_ref-Dennis_BurkeAll_Circuits_are_Busy_Now:_The_1990_AT&T_Long_Distance_Network_CollapseAT&T_6-0" class="reference"><a href="#cite_note-Dennis_BurkeAll_Circuits_are_Busy_Now:_The_1990_AT&T_Long_Distance_Network_CollapseAT&T-6"><span class="cite_crochet">[</span>6<span class="cite_crochet">]</span></a></sup>. Ces défauts peuvent donner lieu à des <a href="/wiki/Bug_(informatique)" title="Bug (informatique)">bugs</a>. L'exploitation de certains de ces défauts peut également permettre à des tiers d'en détourner l'usage pour récupérer des données et nuire au fonctionnement des systèmes. Ces défauts constituent alors des <a href="/wiki/Vuln%C3%A9rabilit%C3%A9_(informatique)" title="Vulnérabilité (informatique)">failles de sécurité</a><sup id="cite_ref-Kalagiakos2012Kalagiakos20126_7-0" class="reference"><a href="#cite_note-Kalagiakos2012Kalagiakos20126-7"><span class="cite_crochet">[</span>7<span class="cite_crochet">]</span></a></sup> (voir liens externes: "Bulletins d'informations, failles de sécurité"<sup id="cite_ref-US-CERT2018VMware-Releases-Security-UpdatesUS-CERT2018-1_8-0" class="reference"><a href="#cite_note-US-CERT2018VMware-Releases-Security-UpdatesUS-CERT2018-1-8"><span class="cite_crochet">[</span>8<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-US-CERT2018Microsoft-Releases-November-2018-Security-UpdatesUS-CERT2018-2_9-0" class="reference"><a href="#cite_note-US-CERT2018Microsoft-Releases-November-2018-Security-UpdatesUS-CERT2018-2-9"><span class="cite_crochet">[</span>9<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-US-CERT2018Cisco-Releases-Security-UpdatesUS-CERT2018-3_10-0" class="reference"><a href="#cite_note-US-CERT2018Cisco-Releases-Security-UpdatesUS-CERT2018-3-10"><span class="cite_crochet">[</span>10<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-US-CERT2018Apple-Releases-Security-Updates-iCloud-iOSUS-CERT2018-4_11-0" class="reference"><a href="#cite_note-US-CERT2018Apple-Releases-Security-Updates-iCloud-iOSUS-CERT2018-4-11"><span class="cite_crochet">[</span>11<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-US-CERT2018Apache-Releases-Security-Update-Apache-Tomcat-JK-ConnectorsUS-CERT2018-5_12-0" class="reference"><a href="#cite_note-US-CERT2018Apache-Releases-Security-Update-Apache-Tomcat-JK-ConnectorsUS-CERT2018-5-12"><span class="cite_crochet">[</span>12<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-FR-CERT2018Multiples_vulnérabilités_de_fuite_d’informations_dans_des_processeursUS-CERT2018-1_13-0" class="reference"><a href="#cite_note-FR-CERT2018Multiples_vulnérabilités_de_fuite_d’informations_dans_des_processeursUS-CERT2018-1-13"><span class="cite_crochet">[</span>13<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-FR-CERT2018Vulnérabilité_dans_Wallix_AdminBastionUS-CERT2018-2_14-0" class="reference"><a href="#cite_note-FR-CERT2018Vulnérabilité_dans_Wallix_AdminBastionUS-CERT2018-2-14"><span class="cite_crochet">[</span>14<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-FR-CERT2018Multiples_vulnérabilités_dans_le_noyau_Linux_d’UbuntuUS-CERT2018-3_15-0" class="reference"><a href="#cite_note-FR-CERT2018Multiples_vulnérabilités_dans_le_noyau_Linux_d’UbuntuUS-CERT2018-3-15"><span class="cite_crochet">[</span>15<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup>). Ces défauts sont mis en exergue par une vérification du code, leur correction se fait par l'intermédiaire de patchs correctifs. Cette solution <a href="/wiki/Trivial" class="mw-redirect" title="Trivial">triviale</a> implique de passer en revue chaque <a href="/wiki/Ligne_de_code" title="Ligne de code">ligne de code</a> 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 code. À titre d'exemple, le <a href="/wiki/Noyau_Linux" title="Noyau Linux">noyau Linux</a> Version 4.13 contient 24.766.703 de lignes de codes<sup id="cite_ref-Linux_p3_1-1" class="reference"><a href="#cite_note-Linux_p3-1"><span class="cite_crochet">[</span>1<span class="cite_crochet">]</span></a></sup>. Selon <a href="/wiki/Edsger_Dijkstra" title="Edsger Dijkstra">Edsger W. Dijkstra</a>, "Les tests de programme peuvent être utilisés pour montrer la présence de bugs, mais jamais pour montrer leur absence"<sup id="cite_ref-Dijkstra1979Dijkstra19796_16-0" class="reference"><a href="#cite_note-Dijkstra1979Dijkstra19796-16"><span class="cite_crochet">[</span>16<span class="cite_crochet">]</span></a></sup>. L’alternative réside en une vérification par <a href="/wiki/M%C3%A9thode_formelle_(informatique)" title="Méthode formelle (informatique)">méthode formelle</a> (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'erreurs de programmation.»<sup id="cite_ref-Klein_p2_17-0" class="reference"><a href="#cite_note-Klein_p2-17"><span class="cite_crochet">[</span>17<span class="cite_crochet">]</span></a></sup>. Ces derniers ont notamment été les premiers à produire une preuve de correction fonctionnelle pour un micro-noyau<sup id="cite_ref-Gu_p596-2_18-0" class="reference"><a href="#cite_note-Gu_p596-2-18"><span class="cite_crochet">[</span>18<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Shao_p666_19-0" class="reference"><a href="#cite_note-Shao_p666-19"><span class="cite_crochet">[</span>19<span class="cite_crochet">]</span></a></sup>. CertiKOS se positionne ouvertement dans cette optique, afin de certifier un système d'exploitation, plutôt que d’en faire une vérification triviale<sup id="cite_ref-Shao_p655-3_20-0" class="reference"><a href="#cite_note-Shao_p655-3-20"><span class="cite_crochet">[</span>20<span class="cite_crochet">]</span></a></sup>. 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'exploitation performants, fiables et sûrs<sup id="cite_ref-Shao_p655-3_20-1" class="reference"><a href="#cite_note-Shao_p655-3-20"><span class="cite_crochet">[</span>20<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-De_Millo1979De_Millo1979279_21-0" class="reference"><a href="#cite_note-De_Millo1979De_Millo1979279-21"><span class="cite_crochet">[</span>21<span class="cite_crochet">]</span></a></sup>. CertiKOS cherche également à produire un noyau certifié, capable de prendre en charge la simultanéité et des machines multi-cœurs<sup id="cite_ref-Shao_p654_22-0" class="reference"><a href="#cite_note-Shao_p654-22"><span class="cite_crochet">[</span>22<span class="cite_crochet">]</span></a></sup>. </p> <div class="mw-heading mw-heading2"><h2 id="La_philosophie_de_Certikos">La philosophie de Certikos</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=2" title="Modifier la section : La philosophie de Certikos" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=2" title="Modifier le code source de la section : La philosophie de Certikos"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Le <a href="/wiki/Syst%C3%A8me_d%27exploitation" title="Système d'exploitation">système d’exploitation</a>, ou OS (<i>Operating System</i>), est un ensemble de <a href="/wiki/Programme_informatique" title="Programme informatique">programmes</a> 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 <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">noyau</a> (<i>Kernel</i> en Anglais), qui gère les ressources matérielles. Ce dernier offre des mécanismes d'<a href="/wiki/Abstraction_(informatique)" title="Abstraction (informatique)">abstraction</a> entre les <a href="/wiki/Programme_informatique" title="Programme informatique">logiciels</a> et les matériels. </p><p>La <a href="/wiki/Certification" title="Certification">certification</a> 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 tâche qui lui est confiée. Cette méthode repose sur une <a href="/wiki/Analyse_statique_de_programmes" title="Analyse statique de programmes">analyse statique</a> 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 <a href="/wiki/S%C3%A9mantique_des_langages_de_programmation" title="Sémantique des langages de programmation">sémantique</a> du programme. </p> <div class="mw-heading mw-heading3"><h3 id="Certification_du_Noyau">Certification du Noyau</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=3" title="Modifier la section : Certification du Noyau" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=3" title="Modifier le code source de la section : Certification du Noyau"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <figure typeof="mw:File/Thumb"><a href="/wiki/Fichier:Raffinement_contextuel.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/9/9d/Raffinement_contextuel.jpg/440px-Raffinement_contextuel.jpg" decoding="async" width="440" height="198" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/9/9d/Raffinement_contextuel.jpg 1.5x" data-file-width="526" data-file-height="237" /></a><figcaption>Représentation du principe de raffinement contextuel de CertiKOS</figcaption></figure> <p>CertiKOS a pour objectif de certifier un système d'exploitation. Cette notion est basée sur la prouvabilité de la vérification par machine, de manière explicite et formelle. Cet effort de <a href="/wiki/Preuve" title="Preuve">preuve</a> est d'autant plus compliqué, au regard porté sur la qualité de la preuve et du risque de la controverse<sup id="cite_ref-GuithubLe_théorème_des_quatre_couleurs_et_les_preuves_informatiséesgithub_23-0" class="reference"><a href="#cite_note-GuithubLe_théorème_des_quatre_couleurs_et_les_preuves_informatiséesgithub-23"><span class="cite_crochet">[</span>23<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-CNRSUn_ordinateur_pour_vérifier_les_preuves_mathématiquescnrs_24-0" class="reference"><a href="#cite_note-CNRSUn_ordinateur_pour_vérifier_les_preuves_mathématiquescnrs-24"><span class="cite_crochet">[</span>24<span class="cite_crochet">]</span></a></sup>. L'équipe de seL4<sup id="cite_ref-Klein_p2_17-1" class="reference"><a href="#cite_note-Klein_p2-17"><span class="cite_crochet">[</span>17<span class="cite_crochet">]</span></a></sup> a été la première à construire une preuve de correction fonctionnelle, pour un <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">micro-noyau</a><sup id="cite_ref-Gu_p596-2_18-1" class="reference"><a href="#cite_note-Gu_p596-2-18"><span class="cite_crochet">[</span>18<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Shao_p666_19-1" class="reference"><a href="#cite_note-Shao_p666-19"><span class="cite_crochet">[</span>19<span class="cite_crochet">]</span></a></sup>. CertiKOS s'y emploie aussi, notamment à l'aide de l'<a href="/wiki/Assistant_de_preuve" title="Assistant de preuve">assistant de preuve</a> de <a href="/wiki/Coq_(logiciel)" title="Coq (logiciel)">Coq</a> et à la définition d'un raffinement contextuel fort<sup id="cite_ref-Shao2016Shao2016607_25-0" class="reference"><a href="#cite_note-Shao2016Shao2016607-25"><span class="cite_crochet">[</span>25<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Appel2016Appel20162_26-0" class="reference"><a href="#cite_note-Appel2016Appel20162-26"><span class="cite_crochet">[</span>26<span class="cite_crochet">]</span></a></sup>. </p><p>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 <a href="/wiki/Programme_informatique" title="Programme informatique">programme</a>. 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'abstraction logiques<sup id="cite_ref-Gu2015Gu2015595-1_27-0" class="reference"><a href="#cite_note-Gu2015Gu2015595-1-27"><span class="cite_crochet">[</span>27<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Pierce2016Pierce20161_28-0" class="reference"><a href="#cite_note-Pierce2016Pierce20161-28"><span class="cite_crochet">[</span>28<span class="cite_crochet">]</span></a></sup>. </p><p>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 (<a href="/wiki/Espace_utilisateur" title="Espace utilisateur">contexte utilisateur</a>)<sup id="cite_ref-Gu_p596-2_18-2" class="reference"><a href="#cite_note-Gu_p596-2-18"><span class="cite_crochet">[</span>18<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Shao2016Shao2016654-2_29-0" class="reference"><a href="#cite_note-Shao2016Shao2016654-2-29"><span class="cite_crochet">[</span>29<span class="cite_crochet">]</span></a></sup>. Ainsi, en considérant K pour le noyau, P pour le programme et S pour la spécification fonctionnelle du noyau, la combinaison des <a href="/wiki/Code_source" title="Code source">codes</a> de K et P affine S et P. CertiKOS cherche à décomposer la vérification de l'OS en plusieurs sous tâches, plus petites et elles-mêmes contrôlables, sur la base de leurs spécifications profondes. C’est donc la <a href="/wiki/Certification" title="Certification">Certification</a> de ces différentes couches d’abstraction, 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’abstraction) 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<sup id="cite_ref-Shao2016Shao2016658_30-0" class="reference"><a href="#cite_note-Shao2016Shao2016658-30"><span class="cite_crochet">[</span>30<span class="cite_crochet">]</span></a></sup>. </p> <div class="mw-heading mw-heading3"><h3 id="Spécifications_profondes"><span id="Sp.C3.A9cifications_profondes"></span>Spécifications profondes</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=4" title="Modifier la section : Spécifications profondes" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=4" title="Modifier le code source de la section : Spécifications profondes"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Les systèmes d'exploitation constituent une multitude de superposition de couches d'abstraction: <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">noyaux</a> (Kernel), pilotes (Drivers ), <a href="/wiki/Hyperviseur" title="Hyperviseur">Hyperviseurs</a> (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 <a href="/wiki/Programme_informatique" title="Programme informatique">programmes</a> 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<sup id="cite_ref-Gu_p595_31-0" class="reference"><a href="#cite_note-Gu_p595-31"><span class="cite_crochet">[</span>31<span class="cite_crochet">]</span></a></sup>. Cela rend difficile l'établissement de propriétés de corrections fortes et la mise à l'échelle de la vérification de programmes, sur plusieurs couches. L’importance de définir précisément les spécifications fonctionnelles des différentes couches d’abstraction, est intimement liée à la <a href="/wiki/Certification" title="Certification">Certification</a> de ces dernières. </p> <figure typeof="mw:File/Thumb"><a href="/wiki/Fichier:Comportement_contextuel.jpg" class="mw-file-description"><img alt="" src="//upload.wikimedia.org/wikipedia/commons/thumb/9/91/Comportement_contextuel.jpg/500px-Comportement_contextuel.jpg" decoding="async" width="500" height="515" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/9/91/Comportement_contextuel.jpg 1.5x" data-file-width="524" data-file-height="540" /></a><figcaption>Vulgarisation de l'indépendance d'implémentation de la Spécification Profonde</figcaption></figure> <p>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<sup id="cite_ref-Gu_p595_31-1" class="reference"><a href="#cite_note-Gu_p595-31"><span class="cite_crochet">[</span>31<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Shao_p655-3_20-2" class="reference"><a href="#cite_note-Shao_p655-3-20"><span class="cite_crochet">[</span>20<span class="cite_crochet">]</span></a></sup>. </p><p>Il possible de représenter le concept de spécification avec les exemples suivants : </p> <ul><li>une spécification simple: L’eau pure bout à <span title="212 °F ou 373,2 K">100 </span><abbr class="abbr" title="degré Celsius">°C</abbr>.</li> <li>approche en spécification profonde : L’eau pure bout à <span title="212 °F ou 373,2 K">100 </span><abbr class="abbr" title="degré Celsius">°C</abbr> à une pression atmosphérique de <span title="101 300 Pa ou 0,999 753 atm" style="cursor:help">1,013</span> bar.</li></ul> <p>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<sup id="cite_ref-Gu_p596-2_18-3" class="reference"><a href="#cite_note-Gu_p596-2-18"><span class="cite_crochet">[</span>18<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Shao_p655-3_20-3" class="reference"><a href="#cite_note-Shao_p655-3-20"><span class="cite_crochet">[</span>20<span class="cite_crochet">]</span></a></sup>. Cette propriété d'indépendance d'implémentation des spécifications profondes rend possible la vérification modulaire des propriétés de correction, à l'instar des spécifications de type ou de programmation par contrat<sup id="cite_ref-Gu_p596-2_18-4" class="reference"><a href="#cite_note-Gu_p596-2-18"><span class="cite_crochet">[</span>18<span class="cite_crochet">]</span></a></sup>. </p><p>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 frein (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. </p> <div class="mw-heading mw-heading3"><h3 id="Certification_du_code_informatique:_CompCertX">Certification du code informatique: CompCertX</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=5" title="Modifier la section : Certification du code informatique: CompCertX" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=5" title="Modifier le code source de la section : Certification du code informatique: CompCertX"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>CertiKOS s’emploie à concevoir des micronoyaux car leurs vérifications est par essence moins lourde. Les <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">noyaux</a> de systèmes d'exploitations ne sont, ni plus ni moins, que des <a href="/wiki/Programme_informatique" title="Programme informatique">programmes</a> informatiques écrits dans un langage de programmation C et/ou en langage de programmation assembleur<sup id="cite_ref-Klein_p2_17-2" class="reference"><a href="#cite_note-Klein_p2-17"><span class="cite_crochet">[</span>17<span class="cite_crochet">]</span></a></sup>. Tout langage de programmation constitue en soi une couche d’abstraction car il n’est pas directement interprétable par la machine. </p><p>Afin de certifier cette nouvelle couche d’abstraction, pour assurer le bon fonctionnement d'un [noyau, il faut donc certifier que les lignes de <a href="/wiki/Code_source" title="Code source">codes</a> vont pouvoir être compilées correctement, de manière à n'engendrer aucun bug. C’est dans ce but que CertiKOS fait appel à CompCertX «CompCert eXtended», développé par Gu et al<sup id="cite_ref-Gu_p604-10_32-0" class="reference"><a href="#cite_note-Gu_p604-10-32"><span class="cite_crochet">[</span>32<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Shao2016Shao2016656_33-0" class="reference"><a href="#cite_note-Shao2016Shao2016656-33"><span class="cite_crochet">[</span>33<span class="cite_crochet">]</span></a></sup> et basé sur <a href="/wiki/CompCert" title="CompCert">CompCert</a><sup id="cite_ref-The_CompCert_C_verified_compiler2018The_CompCert_C_verified_compiler1_34-0" class="reference"><a href="#cite_note-The_CompCert_C_verified_compiler2018The_CompCert_C_verified_compiler1-34"><span class="cite_crochet">[</span>34<span class="cite_crochet">]</span></a></sup>. L'utilisation de CompCert ne permet pas de prouver l'exactitude de la <a href="/wiki/Compilateur" title="Compilateur">compilation</a> 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é<sup id="cite_ref-Gu_p596-2_18-5" class="reference"><a href="#cite_note-Gu_p596-2-18"><span class="cite_crochet">[</span>18<span class="cite_crochet">]</span></a></sup>. </p><p>CompCertX implémente ClightX (une variante du langage source de CompCert, Clight) et un langage <a href="/wiki/Assembleur" title="Assembleur">assembleur</a>, LAsm. La <a href="/wiki/S%C3%A9mantique_des_langages_de_programmation" title="Sémantique des langages de programmation">sémantique</a> 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<sup id="cite_ref-Gu_p604-10_32-1" class="reference"><a href="#cite_note-Gu_p604-10-32"><span class="cite_crochet">[</span>32<span class="cite_crochet">]</span></a></sup>. </p><p>La <a href="/wiki/Certification" title="Certification">Certification</a> des couches d'abstraction 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<sup id="cite_ref-Shao2016Shao2016657-5_35-0" class="reference"><a href="#cite_note-Shao2016Shao2016657-5-35"><span class="cite_crochet">[</span>35<span class="cite_crochet">]</span></a></sup>. </p> <div class="mw-heading mw-heading2"><h2 id="Implémentation_de_CertiKOS"><span id="Impl.C3.A9mentation_de_CertiKOS"></span>Implémentation de CertiKOS</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=6" title="Modifier la section : Implémentation de CertiKOS" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=6" title="Modifier le code source de la section : Implémentation de CertiKOS"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="mw-heading mw-heading3"><h3 id="Au_travers_d'un_Hyperviseur_Certifié"><span id="Au_travers_d.27un_Hyperviseur_Certifi.C3.A9"></span>Au travers d'un Hyperviseur Certifié</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=7" title="Modifier la section : Au travers d'un Hyperviseur Certifié" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=7" title="Modifier le code source de la section : Au travers d'un Hyperviseur Certifié"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Avec le développement important des solutions de stockage et d'hébergement de type <a href="/wiki/Cloud_computing" title="Cloud computing">Cloud</a> (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 <a href="/wiki/Hyperviseur" title="Hyperviseur">hyperviseur</a> était 100% sécurisé, de par sa complexité et sa taille. Il était donc impossible de certifier et garantir que son fonctionnement serait correct<sup id="cite_ref-Vaynberg20112011Vaynberg20114_36-0" class="reference"><a href="#cite_note-Vaynberg20112011Vaynberg20114-36"><span class="cite_crochet">[</span>36<span class="cite_crochet">]</span></a></sup>. </p><p>L'une des premières faille de sécurité dans un environnement cloud est le <a href="/wiki/Programme_informatique" title="Programme informatique">logiciel</a> de management en lui-même<sup id="cite_ref-Vaynberg20112011Vaynberg20112_37-0" class="reference"><a href="#cite_note-Vaynberg20112011Vaynberg20112-37"><span class="cite_crochet">[</span>37<span class="cite_crochet">]</span></a></sup>. 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. </p><p>Le logiciel de gestion du fournisseur utilise les interfaces de délégation du <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">noyau</a> 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. </p> <figure typeof="mw:File/Thumb"><a href="/wiki/Fichier:Allocation_ressources_CertiKOS.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/e/e8/Allocation_ressources_CertiKOS.jpg/518px-Allocation_ressources_CertiKOS.jpg" decoding="async" width="518" height="293" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/e/e8/Allocation_ressources_CertiKOS.jpg 1.5x" data-file-width="536" data-file-height="303" /></a><figcaption>Allocation des ressources avec un hyperviseur certifié</figcaption></figure> <p>Allocation, Gestion et Révocation des ressources selon l'Hyperviseur CertiKOS </p> <ul><li>Allocation <a href="/wiki/Processeur" title="Processeur">CPU</a> :</li></ul> <p>CertiKOS alloue les ressources de la CPU de manière spatiale, à la granularité de base. Lors de la première ébauche de CertiKOS, un Cœur 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. </p> <ul><li>Allocation RAM et Disques :</li></ul> <p>CertiKOS extrait à la fois la <a href="/wiki/M%C3%A9moire_vive" title="Mémoire vive">RAM</a> 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 <a href="/wiki/Syst%C3%A8me_de_fichiers" title="Système de fichiers">système de fichiers</a>, 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. </p> <ul><li>Allocation Interfaces :</li></ul> <p>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. </p><p>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 <a href="/wiki/Unit%C3%A9_de_gestion_m%C3%A9moire" class="mw-redirect" title="Unité de gestion mémoire">MMU</a> et IOMMU. De cette manière, CertiKOS applique l'isolation des ressources entre les applications et évite les fuites d'informations. </p> <div class="mw-heading mw-heading3"><h3 id="Au_travers_d'un_Noyau_Certifié:_mCertiKOS,_mC2"><span id="Au_travers_d.27un_Noyau_Certifi.C3.A9:_mCertiKOS.2C_mC2"></span>Au travers d'un Noyau Certifié: mCertiKOS, mC2</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=8" title="Modifier la section : Au travers d'un Noyau Certifié: mCertiKOS, mC2" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=8" title="Modifier le code source de la section : Au travers d'un Noyau Certifié: mCertiKOS, mC2"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Une fois l'<a href="/wiki/Hyperviseur" title="Hyperviseur">Hyperviseur</a> développé, les chercheurs se sont confrontés à quelques difficultés. En effet, leur hyperviseur n'était pas forcément adapté à un <a href="/wiki/Noyau_de_syst%C3%A8me_d%27exploitation" title="Noyau de système d'exploitation">noyau</a> standard <a href="/wiki/Linux" title="Linux">Linux</a> 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), allegé par rapport à un noyau Linux, mais permettant de valider le bon fonctionnement de leur hyperviseur. De plus, pour développer ce noyau, ils ont également utilisé les méthodes de <a href="/wiki/Certification" title="Certification">Certification</a>, de telle sorte que le noyau soit également vérifié et que l'hyperviseur donne un rendement optimal. </p><p>Grâce à sa <a href="/wiki/S%C3%A9mantique_des_langages_de_programmation" title="Sémantique des langages de programmation">sémantique</a> de composition 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écution de modules noyau et utilisateur, sur différentes couches d'abstraction<sup id="cite_ref-Gu_p604-10_32-2" class="reference"><a href="#cite_note-Gu_p604-10-32"><span class="cite_crochet">[</span>32<span class="cite_crochet">]</span></a></sup><sup class="reference cite_virgule">,</sup><sup id="cite_ref-Shao_p654_22-1" class="reference"><a href="#cite_note-Shao_p654-22"><span class="cite_crochet">[</span>22<span class="cite_crochet">]</span></a></sup>. Le noyau mC2 est une évolution de mCertikos développé à l’origine, dans le cadre d’un vaste projet de recherche, financé par la <a href="/wiki/Defense_Advanced_Research_Projects_Agency" title="Defense Advanced Research Projects Agency">DARPA</a>, pour des véhicules terrestres sans pilote<sup id="cite_ref-Shao2016Shao2016656-657_38-0" class="reference"><a href="#cite_note-Shao2016Shao2016656-657-38"><span class="cite_crochet">[</span>38<span class="cite_crochet">]</span></a></sup>. Ce dernier est pensé de manière séquentielle, en 4 modules totalisant 28 couches d’abstraction certifiées pour sa version basique, et de 5 modules totalisant 37 couches d’abstraction certifiées pour sa version avec hyperviseur<sup id="cite_ref-Gu2015Gu2015596_39-0" class="reference"><a href="#cite_note-Gu2015Gu2015596-39"><span class="cite_crochet">[</span>39<span class="cite_crochet">]</span></a></sup>. Chaque couche est compilée et certifiée par CompCertX. Ce noyau représente 3 000 lignes de <a href="/wiki/Code_source" title="Code source">code</a> et permet de démarrer un système Linux. </p> <figure typeof="mw:File/Thumb"><a href="/wiki/Fichier:Modules_Noyau_2.jpg" class="mw-file-description"><img alt="" src="//upload.wikimedia.org/wikipedia/commons/thumb/7/7f/Modules_Noyau_2.jpg/440px-Modules_Noyau_2.jpg" decoding="async" width="440" height="183" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/7/7f/Modules_Noyau_2.jpg/660px-Modules_Noyau_2.jpg 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/7/7f/Modules_Noyau_2.jpg/880px-Modules_Noyau_2.jpg 2x" data-file-width="1106" data-file-height="460" /></a><figcaption>Découpage des modules des noyaux mCertiKOS</figcaption></figure> <p>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 <a href="/wiki/Communication_inter-processus" title="Communication inter-processus">IPC</a>, verrous IPC, ticket et MCS synchrones (un <a href="/wiki/Spinlock" title="Spinlock">spinlock</a> par <a href="/wiki/Exclusion_mutuelle" title="Exclusion mutuelle">exclusion mutuelle</a>) (etc..)<sup id="cite_ref-Shao2016Shao2016663_40-0" class="reference"><a href="#cite_note-Shao2016Shao2016663-40"><span class="cite_crochet">[</span>40<span class="cite_crochet">]</span></a></sup>, Certikos a fait naitre mC2. </p><p>Le noyau mC2 est quant à lui, une version plus évoluée, qui comprend 6 500 lignes d’assemblage C et <a href="/wiki/X86" title="X86">x86</a>. 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<sup id="cite_ref-Shao_p654_22-2" class="reference"><a href="#cite_note-Shao_p654-22"><span class="cite_crochet">[</span>22<span class="cite_crochet">]</span></a></sup>. </p><p>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 1 400 lignes, dont 943 lignes pour les couches les plus basses, constituant la <a href="/wiki/Th%C3%A9orie_axiomatique" title="Théorie axiomatique">théorie axiomatique</a> 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 : 5 246 lignes, pour les différentes fonctions du noyau et près de 40 000 lignes, pour définir différents théorèmes, <a href="/wiki/Lemme_(math%C3%A9matiques)" title="Lemme (mathématiques)">lemmes</a>, et invariants<sup id="cite_ref-Shao2016Shao2016664_41-0" class="reference"><a href="#cite_note-Shao2016Shao2016664-41"><span class="cite_crochet">[</span>41<span class="cite_crochet">]</span></a></sup>. </p><p>CertiKOS a permis 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éfini de la façon suivante : pour tout <a href="/wiki/Programme_informatique" title="Programme informatique">programme</a> (P), l’interaction du noyau (K) et de P, dans la sémantique de la machine x86, <a href="/wiki/Implication_(logique)" title="Implication (logique)">implique</a> le même comportement que P dans la sémantique de la machine mC2: ∀P, [ [P⋉K] ]x86 ⊆ [ [P] ]mC2<sup id="cite_ref-Shao2016Shao2016655-655_42-0" class="reference"><a href="#cite_note-Shao2016Shao2016655-655-42"><span class="cite_crochet">[</span>42<span class="cite_crochet">]</span></a></sup>. 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 haut niveau. 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 <a href="/wiki/M%C3%A9moire_tampon" title="Mémoire tampon">mémoire tampon</a>, pas d'attaque par <a href="/wiki/Injection_de_code" title="Injection de code">injection de code</a>, de dépassement d'entier ou d'accès de <a href="/wiki/Pointeur_(programmation)" title="Pointeur (programmation)">pointeur</a> nul, etc<sup id="cite_ref-Shao_p657_43-0" class="reference"><a href="#cite_note-Shao_p657-43"><span class="cite_crochet">[</span>43<span class="cite_crochet">]</span></a></sup>. </p><p>Le noyau mC2 n'est pas encore aussi complet qu'un système Linux. Il manque actuellement d'un système de stockage certifié. De plus, il s'appuie sur un chargeur de démarrage qui initialise les CPU et les périphériques qui n'est pas encore vérifié<sup id="cite_ref-Shao_p657_43-1" class="reference"><a href="#cite_note-Shao_p657-43"><span class="cite_crochet">[</span>43<span class="cite_crochet">]</span></a></sup>. </p> <div class="mw-heading mw-heading2"><h2 id="Références"><span id="R.C3.A9f.C3.A9rences"></span>Références</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=9" title="Modifier la section : Références" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=9" title="Modifier le code source de la section : Références"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <div class="references-small decimal" style="column-width:24em; column-count:3;"><ol class="references"> <li id="cite_note-Linux_p3-1"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Linux_p3_1-0">a</a> et <a href="#cite_ref-Linux_p3_1-1">b</a></sup> </span><span class="reference-text"><a href="#LinuxFoundation2017">LinuxFoundation 2017</a>, <abbr class="abbr" title="page(s)">p.</abbr> 3</span> </li> <li id="cite_note-Auffray2018Auffray20181-2"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Auffray2018Auffray20181_2-0">↑</a> </span><span class="reference-text"><a href="#Auffray2018">Auffray 2018</a>, <abbr class="abbr" title="page(s)">p.</abbr> 1. </span> </li> <li id="cite_note-TMR2018TMR20181-3"><span class="mw-cite-backlink noprint"><a href="#cite_ref-TMR2018TMR20181_3-0">↑</a> </span><span class="reference-text"><a href="#TMR2018">TMR 2018</a>, <abbr class="abbr" title="page(s)">p.</abbr> 1. </span> </li> <li id="cite_note-Shao2016Shao2016653-4"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016653_4-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 653. </span> </li> <li id="cite_note-Toyota2013Toyota20131-5"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Toyota2013Toyota20131_5-0">↑</a> </span><span class="reference-text"><a href="#Toyota2013">Toyota 2013</a>, <abbr class="abbr" title="page(s)">p.</abbr> 1. </span> </li> <li id="cite_note-Dennis_BurkeAll_Circuits_are_Busy_Now:_The_1990_AT&T_Long_Distance_Network_CollapseAT&T-6"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Dennis_BurkeAll_Circuits_are_Busy_Now:_The_1990_AT&T_Long_Distance_Network_CollapseAT&T_6-0">↑</a> </span><span class="reference-text"><a href="#AT&T">Dennis Burke All Circuits are Busy Now: The 1990 AT&T Long Distance Network Collapse</a>. </span> </li> <li id="cite_note-Kalagiakos2012Kalagiakos20126-7"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Kalagiakos2012Kalagiakos20126_7-0">↑</a> </span><span class="reference-text"><a href="#Kalagiakos2012">Kalagiakos 2012</a>, <abbr class="abbr" title="page(s)">p.</abbr> 6. </span> </li> <li id="cite_note-US-CERT2018VMware-Releases-Security-UpdatesUS-CERT2018-1-8"><span class="mw-cite-backlink noprint"><a href="#cite_ref-US-CERT2018VMware-Releases-Security-UpdatesUS-CERT2018-1_8-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-1">US-CERT et 2018 VMware-Releases-Security-Updates</a>. </span> </li> <li id="cite_note-US-CERT2018Microsoft-Releases-November-2018-Security-UpdatesUS-CERT2018-2-9"><span class="mw-cite-backlink noprint"><a href="#cite_ref-US-CERT2018Microsoft-Releases-November-2018-Security-UpdatesUS-CERT2018-2_9-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-2">US-CERT et 2018 Microsoft-Releases-November-2018-Security-Updates</a>. </span> </li> <li id="cite_note-US-CERT2018Cisco-Releases-Security-UpdatesUS-CERT2018-3-10"><span class="mw-cite-backlink noprint"><a href="#cite_ref-US-CERT2018Cisco-Releases-Security-UpdatesUS-CERT2018-3_10-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-3">US-CERT et 2018 Cisco-Releases-Security-Updates</a>. </span> </li> <li id="cite_note-US-CERT2018Apple-Releases-Security-Updates-iCloud-iOSUS-CERT2018-4-11"><span class="mw-cite-backlink noprint"><a href="#cite_ref-US-CERT2018Apple-Releases-Security-Updates-iCloud-iOSUS-CERT2018-4_11-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-4">US-CERT et 2018 Apple-Releases-Security-Updates-iCloud-iOS</a>. </span> </li> <li id="cite_note-US-CERT2018Apache-Releases-Security-Update-Apache-Tomcat-JK-ConnectorsUS-CERT2018-5-12"><span class="mw-cite-backlink noprint"><a href="#cite_ref-US-CERT2018Apache-Releases-Security-Update-Apache-Tomcat-JK-ConnectorsUS-CERT2018-5_12-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-5">US-CERT et 2018 Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors</a>. </span> </li> <li id="cite_note-FR-CERT2018Multiples_vulnérabilités_de_fuite_d’informations_dans_des_processeursUS-CERT2018-1-13"><span class="mw-cite-backlink noprint"><a href="#cite_ref-FR-CERT2018Multiples_vulnérabilités_de_fuite_d’informations_dans_des_processeursUS-CERT2018-1_13-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-1">FR-CERT et 2018 Multiples vulnérabilités de fuite d’informations dans des processeurs</a>. </span> </li> <li id="cite_note-FR-CERT2018Vulnérabilité_dans_Wallix_AdminBastionUS-CERT2018-2-14"><span class="mw-cite-backlink noprint"><a href="#cite_ref-FR-CERT2018Vulnérabilité_dans_Wallix_AdminBastionUS-CERT2018-2_14-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-2">FR-CERT et 2018 Vulnérabilité dans Wallix AdminBastion</a>. </span> </li> <li id="cite_note-FR-CERT2018Multiples_vulnérabilités_dans_le_noyau_Linux_d’UbuntuUS-CERT2018-3-15"><span class="mw-cite-backlink noprint"><a href="#cite_ref-FR-CERT2018Multiples_vulnérabilités_dans_le_noyau_Linux_d’UbuntuUS-CERT2018-3_15-0">↑</a> </span><span class="reference-text"><a href="#US-CERT2018-3">FR-CERT et 2018 Multiples vulnérabilités dans le noyau Linux d’Ubuntu</a>. </span> </li> <li id="cite_note-Dijkstra1979Dijkstra19796-16"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Dijkstra1979Dijkstra19796_16-0">↑</a> </span><span class="reference-text"><a href="#Dijkstra1979">Dijkstra 1979</a>, <abbr class="abbr" title="page(s)">p.</abbr> 6. </span> </li> <li id="cite_note-Klein_p2-17"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Klein_p2_17-0">a</a> <a href="#cite_ref-Klein_p2_17-1">b</a> et <a href="#cite_ref-Klein_p2_17-2">c</a></sup> </span><span class="reference-text"><a href="#Klein2009">Klein 2009</a>, <abbr class="abbr" title="page(s)">p.</abbr> 207</span> </li> <li id="cite_note-Gu_p596-2-18"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Gu_p596-2_18-0">a</a> <a href="#cite_ref-Gu_p596-2_18-1">b</a> <a href="#cite_ref-Gu_p596-2_18-2">c</a> <a href="#cite_ref-Gu_p596-2_18-3">d</a> <a href="#cite_ref-Gu_p596-2_18-4">e</a> et <a href="#cite_ref-Gu_p596-2_18-5">f</a></sup> </span><span class="reference-text"><a href="#Gu2015">Gu 2015</a>, <abbr class="abbr" title="page(s)">p.</abbr> 596-2</span> </li> <li id="cite_note-Shao_p666-19"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Shao_p666_19-0">a</a> et <a href="#cite_ref-Shao_p666_19-1">b</a></sup> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 666</span> </li> <li id="cite_note-Shao_p655-3-20"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Shao_p655-3_20-0">a</a> <a href="#cite_ref-Shao_p655-3_20-1">b</a> <a href="#cite_ref-Shao_p655-3_20-2">c</a> et <a href="#cite_ref-Shao_p655-3_20-3">d</a></sup> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 655</span> </li> <li id="cite_note-De_Millo1979De_Millo1979279-21"><span class="mw-cite-backlink noprint"><a href="#cite_ref-De_Millo1979De_Millo1979279_21-0">↑</a> </span><span class="reference-text"><a href="#De_Millo1979">De Millo 1979</a>, <abbr class="abbr" title="page(s)">p.</abbr> 279. </span> </li> <li id="cite_note-Shao_p654-22"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Shao_p654_22-0">a</a> <a href="#cite_ref-Shao_p654_22-1">b</a> et <a href="#cite_ref-Shao_p654_22-2">c</a></sup> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 654</span> </li> <li id="cite_note-GuithubLe_théorème_des_quatre_couleurs_et_les_preuves_informatiséesgithub-23"><span class="mw-cite-backlink noprint"><a href="#cite_ref-GuithubLe_théorème_des_quatre_couleurs_et_les_preuves_informatiséesgithub_23-0">↑</a> </span><span class="reference-text"><a href="#github">Guithub Le théorème des quatre couleurs et les preuves informatisées</a>. </span> </li> <li id="cite_note-CNRSUn_ordinateur_pour_vérifier_les_preuves_mathématiquescnrs-24"><span class="mw-cite-backlink noprint"><a href="#cite_ref-CNRSUn_ordinateur_pour_vérifier_les_preuves_mathématiquescnrs_24-0">↑</a> </span><span class="reference-text"><a href="#cnrs">CNRS Un ordinateur pour vérifier les preuves mathématiques</a>. </span> </li> <li id="cite_note-Shao2016Shao2016607-25"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016607_25-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 607. </span> </li> <li id="cite_note-Appel2016Appel20162-26"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Appel2016Appel20162_26-0">↑</a> </span><span class="reference-text"><a href="#Appel2016">Appel 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 2. </span> </li> <li id="cite_note-Gu2015Gu2015595-1-27"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Gu2015Gu2015595-1_27-0">↑</a> </span><span class="reference-text"><a href="#Gu2015">Gu 2015</a>, <abbr class="abbr" title="page(s)">p.</abbr> 595-1. </span> </li> <li id="cite_note-Pierce2016Pierce20161-28"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Pierce2016Pierce20161_28-0">↑</a> </span><span class="reference-text"><a href="#Pierce2016">Pierce 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 1. </span> </li> <li id="cite_note-Shao2016Shao2016654-2-29"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016654-2_29-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 654-2. </span> </li> <li id="cite_note-Shao2016Shao2016658-30"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016658_30-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 658. </span> </li> <li id="cite_note-Gu_p595-31"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Gu_p595_31-0">a</a> et <a href="#cite_ref-Gu_p595_31-1">b</a></sup> </span><span class="reference-text"><a href="#Gu2015">Gu 2015</a>, <abbr class="abbr" title="page(s)">p.</abbr> 595</span> </li> <li id="cite_note-Gu_p604-10-32"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Gu_p604-10_32-0">a</a> <a href="#cite_ref-Gu_p604-10_32-1">b</a> et <a href="#cite_ref-Gu_p604-10_32-2">c</a></sup> </span><span class="reference-text"><a href="#Gu2015">Gu 2015</a>, <abbr class="abbr" title="page(s)">p.</abbr> 604</span> </li> <li id="cite_note-Shao2016Shao2016656-33"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016656_33-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 656. </span> </li> <li id="cite_note-The_CompCert_C_verified_compiler2018The_CompCert_C_verified_compiler1-34"><span class="mw-cite-backlink noprint"><a href="#cite_ref-The_CompCert_C_verified_compiler2018The_CompCert_C_verified_compiler1_34-0">↑</a> </span><span class="reference-text"><a href="#The_CompCert_C_verified_compiler">The CompCert C verified compiler 2018</a>, <abbr class="abbr" title="page(s)">p.</abbr> 1. </span> </li> <li id="cite_note-Shao2016Shao2016657-5-35"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016657-5_35-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 657-5. </span> </li> <li id="cite_note-Vaynberg20112011Vaynberg20114-36"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Vaynberg20112011Vaynberg20114_36-0">↑</a> </span><span class="reference-text"><a href="#Vaynberg2011">Vaynberg2011 2011</a>, <abbr class="abbr" title="page(s)">p.</abbr> 4. </span> </li> <li id="cite_note-Vaynberg20112011Vaynberg20112-37"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Vaynberg20112011Vaynberg20112_37-0">↑</a> </span><span class="reference-text"><a href="#Vaynberg2011">Vaynberg2011 2011</a>, <abbr class="abbr" title="page(s)">p.</abbr> 2. </span> </li> <li id="cite_note-Shao2016Shao2016656-657-38"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016656-657_38-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 656-657. </span> </li> <li id="cite_note-Gu2015Gu2015596-39"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Gu2015Gu2015596_39-0">↑</a> </span><span class="reference-text"><a href="#Gu2015">Gu 2015</a>, <abbr class="abbr" title="page(s)">p.</abbr> 596. </span> </li> <li id="cite_note-Shao2016Shao2016663-40"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016663_40-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 663. </span> </li> <li id="cite_note-Shao2016Shao2016664-41"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016664_41-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 664. </span> </li> <li id="cite_note-Shao2016Shao2016655-655-42"><span class="mw-cite-backlink noprint"><a href="#cite_ref-Shao2016Shao2016655-655_42-0">↑</a> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 655-655. </span> </li> <li id="cite_note-Shao_p657-43"><span class="mw-cite-backlink noprint">↑ <sup><a href="#cite_ref-Shao_p657_43-0">a</a> et <a href="#cite_ref-Shao_p657_43-1">b</a></sup> </span><span class="reference-text"><a href="#Shao2016">Shao 2016</a>, <abbr class="abbr" title="page(s)">p.</abbr> 657</span> </li> </ol> </div> <div class="mw-heading mw-heading2"><h2 id="Bibliographie">Bibliographie</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=10" title="Modifier la section : Bibliographie" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=10" title="Modifier le code source de la section : Bibliographie"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><span class="ouvrage" id="Vaynberg2012"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> A. <span class="nom_auteur">Vaynberg</span> et Z. <span class="nom_auteur">Shao</span>, « <cite style="font-style:normal" lang="en">Compositional Verification of a Baby Virtual Memory Manager</cite> », <i><span class="lang-en" lang="en">Springer, Berlin, Heidelberg</span></i>, <abbr class="abbr" title="volume">vol.</abbr> 7679,‎ <time>2012</time>, ??-?? <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-3-642-35308-6" title="Spécial:Ouvrages de référence/978-3-642-35308-6"><span class="nowrap">978-3-642-35308-6</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1007/978-3-642-35308-6_13">10.1007/978-3-642-35308-6_13</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Compositional+Verification+of+a+Baby+Virtual+Memory+Manager&rft.jtitle=Springer%2C+Berlin%2C+Heidelberg&rft.aulast=Vaynberg&rft.aufirst=A.&rft.au=Shao%2C+Z.&rft.date=2012&rft.volume=7679&rft.pages=%3F%3F-%3F%3F&rft.isbn=978-3-642-35308-6&rft_id=info%3Adoi%2F10.1007%2F978-3-642-35308-6_13&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="Jomaa2016"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> N. <span class="nom_auteur">Jomaa</span>, D. <span class="nom_auteur">Nowak</span>, G. <span class="nom_auteur">Grimaud</span> et S. <span class="nom_auteur">Hym</span>, « <cite style="font-style:normal" lang="en">Formal Proof of Dynamic Memory Isolation Based on MMU</cite> », <i><span class="lang-en" lang="en">IEEE Xplore</span></i>,‎ <time class="nowrap" datetime="2016-08" data-sort-value="2016-08">août 2016</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-5090-1764-5" title="Spécial:Ouvrages de référence/978-1-5090-1764-5"><span class="nowrap">978-1-5090-1764-5</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1109/TASE.2016.28">10.1109/TASE.2016.28</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Formal+Proof+of+Dynamic+Memory+Isolation+Based+on+MMU&rft.jtitle=IEEE+Xplore&rft.aulast=Jomaa&rft.aufirst=N.&rft.au=Nowak%2C+D.&rft.au=Grimaud%2C+G.&rft.au=Hym%2C+S.&rft.date=2016-08&rft.isbn=978-1-5090-1764-5&rft_id=info%3Adoi%2F10.1109%2FTASE.2016.28&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="De_Millo1979"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> R.A <span class="nom_auteur">De Millo</span>, R.J <span class="nom_auteur">Lipton</span> et A.J <span class="nom_auteur">Perlis</span>, « <cite style="font-style:normal" lang="en">Social processes and proofs of theorems and programs</cite> », <i><span class="lang-en" lang="en">The ACM Digital Library</span></i>,‎ <time class="nowrap" datetime="1979-05" data-sort-value="1979-05">mai 1979</time> <small style="line-height:1em;">(<a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/359104.359106">10.1145/359104.359106</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Social+processes+and+proofs+of+theorems+and+programs&rft.jtitle=The+ACM+Digital+Library&rft.aulast=De+Millo&rft.aufirst=R.A&rft.au=Lipton%2C+R.J&rft.au=Perlis%2C+A.J&rft.date=1979-05&rft_id=info%3Adoi%2F10.1145%2F359104.359106&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Gu2015"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> R. <span class="nom_auteur">Gu</span>, J. <span class="nom_auteur">Koenig</span>, T. <span class="nom_auteur">Ramananandro</span>, Z. <span class="nom_auteur">Shao</span>, X. <span class="nom_auteur">Wu</span>, S-C. <span class="nom_auteur">Weng</span> et H. <span class="nom_auteur">Zhang</span>, « <cite style="font-style:normal" lang="en">Deep Specifications and Certified Abstraction Layers</cite> », <i><span class="lang-en" lang="en">The ACM Digital Library</span></i>,‎ <time class="nowrap" datetime="2015-01" data-sort-value="2015-01">janvier 2015</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-4503-3300-9" title="Spécial:Ouvrages de référence/978-1-4503-3300-9"><span class="nowrap">978-1-4503-3300-9</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/2676726.2676975">10.1145/2676726.2676975</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Deep+Specifications+and+Certified+Abstraction+Layers&rft.jtitle=The+ACM+Digital+Library&rft.aulast=Gu&rft.aufirst=R.&rft.au=Koenig%2C+J.&rft.au=Ramananandro%2C+T.&rft.au=Shao%2C+Z.&rft.au=Wu%2C+X.&rft.au=Weng%2C+S-C.&rft.au=Zhang%2C+H.&rft.date=2015-01&rft.isbn=978-1-4503-3300-9&rft_id=info%3Adoi%2F10.1145%2F2676726.2676975&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Pierce2016"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> B. C. <span class="nom_auteur">Pierce</span>, « <cite style="font-style:normal" lang="en">The science of deep specification (keynote)</cite> », <i><span class="lang-en" lang="en">The ACM Digital Library</span></i>,‎ <time class="nowrap" datetime="2016-10" data-sort-value="2016-10">octobre 2016</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-4503-4437-1" title="Spécial:Ouvrages de référence/978-1-4503-4437-1"><span class="nowrap">978-1-4503-4437-1</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/2984043.2998388">10.1145/2984043.2998388</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=The+science+of+deep+specification+%28keynote%29&rft.jtitle=The+ACM+Digital+Library&rft.aulast=Pierce&rft.aufirst=B.+C.&rft.date=2016-10&rft.isbn=978-1-4503-4437-1&rft_id=info%3Adoi%2F10.1145%2F2984043.2998388&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Appel2017"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> A. W. <span class="nom_auteur">Appel</span>, L. <span class="nom_auteur">Beringer</span>, A. <span class="nom_auteur">Chlipala</span>, B. C. <span class="nom_auteur">Pierce</span>, Z. <span class="nom_auteur">Shao</span>, S. <span class="nom_auteur">Weirich</span> et S. <span class="nom_auteur">Zdancewic</span>, « <cite style="font-style:normal" lang="en">Position paper: the science of deep specification</cite> », <i><span class="lang-en" lang="en">the Royal Society</span></i>,‎ <time class="nowrap" datetime="2017-09" data-sort-value="2017-09">septembre 2017</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Serial_Number" title="International Standard Serial Number">ISSN</a> <span class="plainlinks noarchive"><a rel="nofollow" class="external text" href="https://portal.issn.org/resource/issn/1471-2962">1471-2962</a></span>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1098/rsta.2016.0331">10.1098/rsta.2016.0331</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Position+paper%3A+the+science+of+deep+specification&rft.jtitle=the+Royal+Society&rft.aulast=Appel&rft.aufirst=A.+W.&rft.au=Beringer%2C+L.&rft.au=Chlipala%2C+A.&rft.au=Pierce%2C+B.+C.&rft.au=Shao%2C+Z.&rft.au=Weirich%2C+S.&rft.au=Zdancewic%2C+S.&rft.date=2017-09&rft.issn=1471-2962&rft_id=info%3Adoi%2F10.1098%2Frsta.2016.0331&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="Liang2013"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> H. <span class="nom_auteur">Liang</span>, J. <span class="nom_auteur">Hoffmann</span>, X. <span class="nom_auteur">Feng</span> et Z. <span class="nom_auteur">Shao</span>, « <cite style="font-style:normal" lang="en">Characterizing Progress Properties of Concurrent Objects via Contextual Refinements</cite> », <i><span class="lang-en" lang="en">Springer</span></i>,‎ <time>2013</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-3-642-40184-8" title="Spécial:Ouvrages de référence/978-3-642-40184-8"><span class="nowrap">978-3-642-40184-8</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1007/978-3-642-40184-8_17">10.1007/978-3-642-40184-8_17</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Characterizing+Progress+Properties+of+Concurrent+Objects+via+Contextual+Refinements&rft.jtitle=Springer&rft.aulast=Liang&rft.aufirst=H.&rft.au=Hoffmann%2C+J.&rft.au=Feng%2C+X.&rft.au=Shao%2C+Z.&rft.date=2013&rft.isbn=978-3-642-40184-8&rft_id=info%3Adoi%2F10.1007%2F978-3-642-40184-8_17&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="Vaynberg2011"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> L. <span class="nom_auteur">Gu</span>, A. <span class="nom_auteur">Vaynberg</span>, B. <span class="nom_auteur">Ford</span>, Z. <span class="nom_auteur">Shao</span> et D. <span class="nom_auteur">Costanzo</span>, « <cite style="font-style:normal" lang="en">CertiKOS: a certified kernel for secure cloud computing</cite> », <i><span class="lang-en" lang="en">The ACM Digital Library</span></i>,‎ <time class="nowrap" datetime="2011-07" data-sort-value="2011-07">juillet 2011</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-4503-1179-3" title="Spécial:Ouvrages de référence/978-1-4503-1179-3"><span class="nowrap">978-1-4503-1179-3</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/2103799.2103803">10.1145/2103799.2103803</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=CertiKOS%3A+a+certified+kernel+for+secure+cloud+computing&rft.jtitle=The+ACM+Digital+Library&rft.aulast=Gu&rft.aufirst=L.&rft.au=Vaynberg%2C+A.&rft.au=Ford%2C+B.&rft.au=Shao%2C+Z.&rft.au=Costanzo%2C+D.&rft.date=2011-07&rft.isbn=978-1-4503-1179-3&rft_id=info%3Adoi%2F10.1145%2F2103799.2103803&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="Shao2016"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> R. <span class="nom_auteur">Gu</span>, Z. <span class="nom_auteur">Shao</span>, H. <span class="nom_auteur">Chen</span>, X. <span class="nom_auteur">Wu</span>, J. <span class="nom_auteur">Kim</span>, V. <span class="nom_auteur">Sjöberg</span> et D. <span class="nom_auteur">Costanzo</span>, « <cite style="font-style:normal" lang="en">CertiKOS: an extensible architecture for building certified concurrent OS kernels</cite> », <i><span class="lang-en" lang="en">The ACM Digital Library</span></i>,‎ <time class="nowrap" datetime="2016-11" data-sort-value="2016-11">novembre 2016</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-931971-33-1" title="Spécial:Ouvrages de référence/978-1-931971-33-1"><span class="nowrap">978-1-931971-33-1</span></a>, <a rel="nofollow" class="external text" href="https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf">lire en ligne</a>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=CertiKOS%3A+an+extensible+architecture+for+building+certified+concurrent+OS+kernels&rft.jtitle=The+ACM+Digital+Library&rft.aulast=Gu&rft.aufirst=R.&rft.au=Shao%2C+Z.&rft.au=Chen%2C+H.&rft.au=Wu%2C+X.&rft.au=Kim%2C+J.&rft.au=Sj%C3%B6berg%2C+V.&rft.au=Costanzo%2C+D.&rft.date=2016-11&rft.isbn=978-1-931971-33-1&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Klein2009"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> G. <span class="nom_auteur">Klein</span>, K. <span class="nom_auteur">Elphinstone</span>, G. <span class="nom_auteur">Heiser</span>, J. <span class="nom_auteur">Andronick</span>, D. <span class="nom_auteur">Cock</span>, P. <span class="nom_auteur">Derrin</span>, D. <span class="nom_auteur">Elkaduwe</span>, K. <span class="nom_auteur">Engelhardt</span>, R. <span class="nom_auteur">Kolanski</span>, M. <span class="nom_auteur">Norrish</span>, T <span class="nom_auteur">Sewell</span>, H. <span class="nom_auteur">Tuch</span> et S. <span class="nom_auteur">Winwood</span>, « <cite style="font-style:normal" lang="en">seL4: Formal Verification of an OS Kernel</cite> », <i><span class="lang-en" lang="en">the Association for Computing Machinery</span></i>,‎ <time class="nowrap" datetime="2009-10" data-sort-value="2009-10">octobre 2009</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-60558-752-3" title="Spécial:Ouvrages de référence/978-1-60558-752-3"><span class="nowrap">978-1-60558-752-3</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/1629575.1629596">10.1145/1629575.1629596</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=seL4%3A+Formal+Verification+of+an+OS+Kernel&rft.jtitle=the+Association+for+Computing+Machinery&rft.aulast=Klein&rft.aufirst=G.&rft.au=Elphinstone%2C+K.&rft.au=Heiser%2C+G.&rft.au=Andronick%2C+J.&rft.au=Cock%2C+D.&rft.au=Derrin%2C+P.&rft.au=Elkaduwe%2C+D.&rft.au=Engelhardt%2C+K.&rft.au=Kolanski%2C+R.&rft.au=Norrish%2C+M.&rft.au=Sewell%2C+T&rft.au=Tuch%2C+H.&rft.au=Winwood%2C+S.&rft.date=2009-10&rft.isbn=978-1-60558-752-3&rft_id=info%3Adoi%2F10.1145%2F1629575.1629596&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Ferraiuolo2017"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> A. <span class="nom_auteur">Ferraiuolo</span>, A. <span class="nom_auteur">Baumann</span>, C. <span class="nom_auteur">Hawblitzel</span> et B. <span class="nom_auteur">Parno</span>, « <cite style="font-style:normal" lang="en">Komodo: Using verification to disentangle secure-enclave hardware from software</cite> », <i><span class="lang-en" lang="en">The ACM Digital Library</span></i>,‎ <time class="nowrap" datetime="2017-10" data-sort-value="2017-10">octobre 2017</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-4503-5085-3" title="Spécial:Ouvrages de référence/978-1-4503-5085-3"><span class="nowrap">978-1-4503-5085-3</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1145/3132747.3132782">10.1145/3132747.3132782</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Komodo%3A+Using+verification+to+disentangle+secure-enclave+hardware+from+software&rft.jtitle=The+ACM+Digital+Library&rft.aulast=Ferraiuolo&rft.aufirst=A.&rft.au=Baumann%2C+A.&rft.au=Hawblitzel%2C+C.&rft.au=Parno%2C+B.&rft.date=2017-10&rft.isbn=978-1-4503-5085-3&rft_id=info%3Adoi%2F10.1145%2F3132747.3132782&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="Appel2016"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> A. W. <span class="nom_auteur">Appel</span>, « <cite style="font-style:normal" lang="en">Modular Verification for Computer Security</cite> », <i><span class="lang-en" lang="en">IEEE Xplore</span></i>,‎ <time class="nowrap" datetime="2016-08" data-sort-value="2016-08">août 2016</time>, ??-?? <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-5090-2607-4" title="Spécial:Ouvrages de référence/978-1-5090-2607-4"><span class="nowrap">978-1-5090-2607-4</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1109/CSF.2016.8">10.1109/CSF.2016.8</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Modular+Verification+for+Computer+Security&rft.jtitle=IEEE+Xplore&rft.aulast=Appel&rft.aufirst=A.+W.&rft.date=2016-08&rft.pages=%3F%3F-%3F%3F&rft.isbn=978-1-5090-2607-4&rft_id=info%3Adoi%2F10.1109%2FCSF.2016.8&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Malecha2016"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> G. <span class="nom_auteur">Malecha</span>, D. <span class="nom_auteur">Ricketts</span>, M. M. <span class="nom_auteur">Alvarez</span> et S. <span class="nom_auteur">Lerner</span>, « <cite style="font-style:normal" lang="en">Towards foundational verification of cyber-physical systems</cite> », <i><span class="lang-en" lang="en">IEEE Xplore</span></i>,‎ <time class="nowrap" datetime="2016-04" data-sort-value="2016-04">avril 2016</time> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-5090-4304-0" title="Spécial:Ouvrages de référence/978-1-5090-4304-0"><span class="nowrap">978-1-5090-4304-0</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1109/SOSCYPS.2016.7580000">10.1109/SOSCYPS.2016.7580000</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Towards+foundational+verification+of+cyber-physical+systems&rft.jtitle=IEEE+Xplore&rft.aulast=Malecha&rft.aufirst=G.&rft.au=Ricketts%2C+D.&rft.au=Alvarez%2C+M.+M.&rft.au=Lerner%2C+S.&rft.date=2016-04&rft.isbn=978-1-5090-4304-0&rft_id=info%3Adoi%2F10.1109%2FSOSCYPS.2016.7580000&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="Kalagiakos2012"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> P. <span class="nom_auteur">Kalagiakos</span> et M. <span class="nom_auteur">Bora</span>, « <cite style="font-style:normal" lang="en">Cloud security tactics: Virtualization and the VMM</cite> », <i><span class="lang-en" lang="en">IEEE Xplore</span></i>,‎ <time class="nowrap" datetime="2012-12" data-sort-value="2012-12">décembre 2012</time>, ??-?? <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-1-4673-1740-5" title="Spécial:Ouvrages de référence/978-1-4673-1740-5"><span class="nowrap">978-1-4673-1740-5</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1109/ICAICT.2012.6398491">10.1109/ICAICT.2012.6398491</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Cloud+security+tactics%3A+Virtualization+and+the+VMM&rft.jtitle=IEEE+Xplore&rft.aulast=Kalagiakos&rft.aufirst=P.&rft.au=Bora%2C+M.&rft.date=2012-12&rft.pages=%3F%3F-%3F%3F&rft.isbn=978-1-4673-1740-5&rft_id=info%3Adoi%2F10.1109%2FICAICT.2012.6398491&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Dijkstra1979"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> E. <span class="nom_auteur">Dijkstra</span>, « <cite style="font-style:normal" lang="en">Structured programming</cite> », <i><span class="lang-en" lang="en">The ACM Digital Library</span></i>,‎ <time class="nowrap" datetime="1979-01" data-sort-value="1979-01">janvier 1979</time>, ??-?? <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/0-917072-14-6" title="Spécial:Ouvrages de référence/0-917072-14-6"><span class="nowrap">0-917072-14-6</span></a>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Structured+programming&rft.jtitle=The+ACM+Digital+Library&rft.aulast=Dijkstra&rft.aufirst=E.&rft.date=1979-01&rft.pages=%3F%3F-%3F%3F&rft.isbn=0-917072-14-6&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="Reddy2009"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> B. <span class="nom_auteur">Reddy Kandukuri</span>, R. <span class="nom_auteur">Paturi V.</span> et A. <span class="nom_auteur">Rakshit</span>, « <cite style="font-style:normal" lang="en">Cloud Security Issues</cite> », <i><span class="lang-en" lang="en">IEEE Xplore</span></i>,‎ <time class="nowrap" datetime="2009-09" data-sort-value="2009-09">septembre 2009</time>, <abbr class="abbr" title="pages">p.</abbr> <span class="nowrap">517- 520</span> <small style="line-height:1em;">(<a href="/wiki/International_Standard_Book_Number" title="International Standard Book Number">ISBN</a> <a href="/wiki/Sp%C3%A9cial:Ouvrages_de_r%C3%A9f%C3%A9rence/978-0-7695-3811-2" title="Spécial:Ouvrages de référence/978-0-7695-3811-2"><span class="nowrap">978-0-7695-3811-2</span></a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">DOI</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://dx.doi.org/10.1109/SCC.2009.84">10.1109/SCC.2009.84</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=Cloud+Security+Issues&rft.jtitle=IEEE+Xplore&rft.aulast=Reddy+Kandukuri&rft.aufirst=B.&rft.au=Paturi+V.%2C+R.&rft.au=Rakshit%2C+A.&rft.date=2009-09&rft.pages=517-+520&rft.isbn=978-0-7695-3811-2&rft_id=info%3Adoi%2F10.1109%2FSCC.2009.84&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="Jomaa2018">N. <span class="nom_auteur">Jomaa</span>, S. <span class="nom_auteur">Hym</span> et D. <span class="nom_auteur">Novak</span>, « <cite style="font-style:normal">La conception d’un noyau orientée par sa preuve d’isolation mémoire</cite> », <i>Compas 2018</i>, <abbr class="abbr" title="volume">vol.</abbr> Juillet 2018,‎ <time>2018</time> <small style="line-height:1em;">(<a href="/wiki/HAL_(archive_ouverte)" title="HAL (archive ouverte)">HAL</a> <span class="plainlinks noarchive nowrap"><a rel="nofollow" class="external text" href="https://hal.science/hal-01819955">hal-01819955</a></span>)</small><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=La+conception+d%E2%80%99un+noyau+orient%C3%A9e+par+sa+preuve+d%E2%80%99isolation+m%C3%A9moire&rft.jtitle=Compas+2018&rft.aulast=Jomaa&rft.aufirst=N.&rft.au=Hym%2C+S.&rft.au=Novak%2C+D.&rft.date=2018&rft.volume=Juillet+2018&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span></li> <li><span class="ouvrage" id="The_CompCert_C_verified_compiler"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <cite style="font-style:normal" lang="en">The CompCert C verified compiler</cite> », <i><span class="lang-en" lang="en">INRIA Paris, September 17, 2018</span></i>,‎ <time class="nowrap" datetime="2018-09" data-sort-value="2018-09">septembre 2018</time><span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.atitle=The+CompCert+C+verified+compiler&rft.jtitle=INRIA+Paris%2C+September+17%2C+2018&rft.date=2018-09&rfr_id=info%3Asid%2Ffr.wikipedia.org%3ACertiKOS"></span></span><span title="Document utilisé pour la rédaction de l’article"><span typeof="mw:File"><span><img alt="Document utilisé pour la rédaction de l’article" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/20px-Icon_flat_design_plume.svg.png" decoding="async" width="20" height="10" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/30px-Icon_flat_design_plume.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/bc/Icon_flat_design_plume.svg/40px-Icon_flat_design_plume.svg.png 2x" data-file-width="330" data-file-height="158" /></span></span></span></li> <li><span class="ouvrage" id="TMR2018">Transparency Market Research, « <a rel="nofollow" class="external text" href="https://www.transparencymarketresearch.com/pressrelease/embedded-system.htm"><cite style="font-style:normal;">Global Embedded Systems Market Rises at 6.4% CAGR; Automotive Industry Powers Growth</cite></a> », sur <span class="italique"><a href="/w/index.php?title=Transparency_Market_Research&action=edit&redlink=1" class="new" title="Transparency Market Research (page inexistante)">Transparency Market Research</a></span>, <time>2018</time> <small style="line-height:1em;">(consulté en <time class="nowrap" datetime="2018-12" data-sort-value="2018-12">décembre 2018</time>)</small></span>.</li> <li><span class="ouvrage" id="Auffray2018">Christophe Auffray, « <a rel="nofollow" class="external text" href="https://www.zdnet.fr/actualites/chiffres-cles-les-ventes-de-mobiles-et-de-smartphones-39789928.htm"><cite style="font-style:normal;">Chiffres clés : les ventes de mobiles et de smartphones</cite></a> », sur <span class="italique"><a href="/wiki/ZDNet" title="ZDNet">zDNet</a></span>, <time>2018</time> <small style="line-height:1em;">(consulté en <time class="nowrap" datetime="2018-12" data-sort-value="2018-12">décembre 2018</time>)</small></span>.</li> <li><span class="ouvrage" id="LinuxFoundation2017">Christophe Auffray, Jonathan <span class="nom_auteur">Corbet</span> et Kroah-Hartman <span class="nom_auteur">Greg</span>, « <a rel="nofollow" class="external text" href="https://www.linuxfoundation.org/2017-linux-kernel-report-landing-page/"><cite style="font-style:normal;">2017 Linux Kernel Development Report</cite></a> », sur <span class="italique"><a href="/w/index.php?title=Linuxfoundation&action=edit&redlink=1" class="new" title="Linuxfoundation (page inexistante)">linuxfoundation</a></span>, <time>2017</time> <small style="line-height:1em;">(consulté en <time class="nowrap" datetime="2018-11" data-sort-value="2018-11">novembre 2018</time>)</small></span>.</li></ul> <div class="mw-heading mw-heading2"><h2 id="Liens_externes">Liens externes</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=CertiKOS&veaction=edit&section=11" title="Modifier la section : Liens externes" class="mw-editsection-visualeditor"><span>modifier</span></a><span class="mw-editsection-divider"> | </span><a href="/w/index.php?title=CertiKOS&action=edit&section=11" title="Modifier le code source de la section : Liens externes"><span>modifier le code</span></a><span class="mw-editsection-bracket">]</span></span></div> <p><b>Bulletin d'information : failles informatiques</b> <a rel="nofollow" class="external free" href="https://www.us-cert.gov/">https://www.us-cert.gov/</a> <a rel="nofollow" class="external free" href="https://www.cert.ssi.gouv.fr">https://www.cert.ssi.gouv.fr</a> </p> <ul><li><span class="ouvrage" id="US-CERT2018-1"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> US <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.us-cert.gov/ncas/current-activity/2018/11/22/VMware-Releases-Security-Updates"><cite style="font-style:normal;" lang="en">VMware-Releases-Security-Updates</cite></a> », <time class="nowrap" datetime="2018-11" data-sort-value="2018-11">novembre 2018</time></span></li> <li><span class="ouvrage" id="US-CERT2018-2"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> US <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.us-cert.gov/ncas/current-activity/2018/11/13/Microsoft-Releases-November-2018-Security-Updates"><cite style="font-style:normal;" lang="en">Microsoft-Releases-November-2018-Security-Updates</cite></a> », <time class="nowrap" datetime="2018-11" data-sort-value="2018-11">novembre 2018</time></span></li> <li><span class="ouvrage" id="US-CERT2018-3"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> US <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.us-cert.gov/ncas/current-activity/2018/11/07/Cisco-Releases-Security-Updates"><cite style="font-style:normal;" lang="en">Cisco-Releases-Security-Updates</cite></a> », <time class="nowrap" datetime="2018-11" data-sort-value="2018-11">novembre 2018</time></span></li> <li><span class="ouvrage" id="US-CERT2018-4"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> US <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.us-cert.gov/ncas/current-activity/2018/11/07/Apple-Releases-Security-Updates-iCloud-iOS"><cite style="font-style:normal;" lang="en">Apple-Releases-Security-Updates-iCloud-iOS</cite></a> », <time class="nowrap" datetime="2018-11" data-sort-value="2018-11">novembre 2018</time></span></li> <li><span class="ouvrage" id="US-CERT2018-5"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> US <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.us-cert.gov/ncas/current-activity/2018/10/31/Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors"><cite style="font-style:normal;" lang="en">Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors</cite></a> », <time class="nowrap" datetime="2018-11" data-sort-value="2018-11">novembre 2018</time></span></li> <li><span class="ouvrage" id="FR-CERT2018-1">FR <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.cert.ssi.gouv.fr/alerte/CERTFR-2018-ALE-001/"><cite style="font-style:normal;">Multiples vulnérabilités de fuite d’informations dans des processeurs</cite></a> », <time class="nowrap" datetime="2018-01" data-sort-value="2018-01">janvier 2018</time></span></li> <li><span class="ouvrage" id="FR-CERT2018-2">FR <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.cert.ssi.gouv.fr/alerte/CERTFR-2018-ALE-012/"><cite style="font-style:normal;">Vulnérabilité dans Wallix AdminBastion</cite></a> », <time class="nowrap" datetime="2018-10" data-sort-value="2018-10">octobre 2018</time></span></li> <li><span class="ouvrage" id="FR-CERT2018-3">FR <span class="nom_auteur">CERT</span>, « <a rel="nofollow" class="external text" href="https://www.cert.ssi.gouv.fr/avis/CERTFR-2018-AVI-581/"><cite style="font-style:normal;">Multiples vulnérabilités dans le noyau Linux d’Ubuntu</cite></a> », <time class="nowrap" datetime="2018-12" data-sort-value="2018-12">décembre 2018</time></span></li> <li><span class="ouvrage" id="Ronghui_Gu"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> R. <span class="nom_auteur">Gu</span>, « <a rel="nofollow" class="external text" href="https://pdfs.semanticscholar.org/0dd7/9b76356624f5f3d7df27721fb4c44c95f0f0.pdf"><cite style="font-style:normal;" lang="en">My Current Work on CertiKOS</cite></a> »</span></li> <li><span class="ouvrage" id="Toyota2013"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> « <a rel="nofollow" class="external text" href="https://www.edn.com/design/automotive/4423428/Toyota-s-killer-firmware--Bad-design-and-its-consequences"><cite style="font-style:normal;" lang="en">Toyota's killer firmware: Bad design and its consequences</cite></a> », <time class="nowrap" datetime="2013-10" data-sort-value="2013-10">octobre 2013</time></span></li> <li><span class="ouvrage" id="Certik"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> <span class="nom_auteur">Certik.org</span>, « <a rel="nofollow" class="external text" href="https://certik.org/"><cite style="font-style:normal;" lang="en">Certik</cite></a> »</span></li> <li><span class="ouvrage" id="Shao"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Zhong <span class="nom_auteur">Shao</span>, « <a rel="nofollow" class="external text" href="https://www.youtube.com/watch?v=ibdjeEHSF54&t=756s"><cite style="font-style:normal;" lang="en">Keynote：Building Fully Trustworthy Smart Contracts and Blockchain Ecosystems</cite></a> »</span></li> <li><span class="ouvrage" id="Shao2017-1"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Zhong <span class="nom_auteur">Shao</span>, « <a rel="nofollow" class="external text" href="https://www.youtube.com/watch?v=RHXpz2ZJ-w0"><cite style="font-style:normal;" lang="en">DeepSpec Summer School, Part 38, Shao (July 27, 2017)</cite></a> »</span></li> <li><span class="ouvrage" id="Shao2017-2"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Zhong <span class="nom_auteur">Shao</span>, « <a rel="nofollow" class="external text" href="https://www.youtube.com/watch?v=2df39-QA4x0"><cite style="font-style:normal;" lang="en">DeepSpec Summer School, Part 40, Shao (July 28, 2017)</cite></a> »</span></li> <li><span class="ouvrage" id="github">Gilles <span class="nom_auteur">COLLOMBET-GOURDON</span>, Chloé <span class="nom_auteur">DEPARIS</span>, Amjad <span class="nom_auteur">EL HAFIDI</span>, Tom <span class="nom_auteur">FÉVRIER</span> et Laure-Lou <span class="nom_auteur">TREMBLAY</span>, « <a rel="nofollow" class="external text" href="https://controverses.github.io/4CTpreuvesinformatiques/#main"><cite style="font-style:normal;">Le théorème des quatre couleurs et les preuves informatisées</cite></a> »</span></li> <li><span class="ouvrage" id="cnrs">Assia <span class="nom_auteur">Mahboubi</span>, « <a rel="nofollow" class="external text" href="http://images.math.cnrs.fr/Un-ordinateur-pour-verifier-les.html"><cite style="font-style:normal;">Un ordinateur pour vérifier les preuves mathématiques</cite></a> »</span></li> <li><span class="ouvrage" id="AT&T"><abbr class="abbr indicateur-langue" title="Langue : anglais">(en)</abbr> Dennis <span class="nom_auteur">Burke</span>, « <a rel="nofollow" class="external text" href="http://users.csc.calpoly.edu/~jdalbey/SWE/Papers/att_collapse"><cite style="font-style:normal;" lang="en">All Circuits are Busy Now: The 1990 AT&T Long Distance Network Collapse</cite></a> »</span></li></ul> <div class="navbox-container" style="clear:both;"> <table class="navbox collapsible noprint autocollapse" style=""> <tbody><tr><th class="navbox-title" colspan="2" style=""><div style="float:left; width:6em; text-align:left"><div class="noprint plainlinks nowrap tnavbar" style="padding:0; font-size:xx-small; color:var(--color-emphasized, #000000);"><a href="/wiki/Mod%C3%A8le:Palette_Syst%C3%A8mes_d%27exploitation" title="Modèle:Palette Systèmes d'exploitation"><abbr class="abbr" title="Voir ce modèle.">v</abbr></a> · <a class="external text" href="https://fr.wikipedia.org/w/index.php?title=Mod%C3%A8le:Palette_Syst%C3%A8mes_d%27exploitation&action=edit"><abbr class="abbr" title="Modifier ce modèle. Merci de prévisualiser avant de sauvegarder.">m</abbr></a></div></div><div style="font-size:110%"><a href="/wiki/Syst%C3%A8me_d%27exploitation" title="Système d'exploitation">Principaux systèmes d’exploitation</a></div></th> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Apple" title="Apple">Apple</a></th> <td class="navbox-list" style=""><table class="navbox-subgroup" style=""> <tbody><tr> <th class="navbox-group" style=""><a href="/wiki/Mac_OS_Classic" title="Mac OS Classic">Mac OS <i>Classic</i></a></th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Syst%C3%A8me_5" title="Système 5">Système 5</a></li> <li><a href="/wiki/Syst%C3%A8me_6" title="Système 6">Système 6</a></li> <li><a href="/wiki/Syst%C3%A8me_7" title="Système 7">Système 7</a></li> <li><a href="/wiki/Mac_OS_8" title="Mac OS 8">Mac OS 8</a></li> <li><a href="/wiki/Mac_OS_9" title="Mac OS 9">Mac OS 9</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Dérivés de NeXTSTEP</th> <td class="navbox-list navbox-even" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/NeXTSTEP" title="NeXTSTEP">NeXTSTEP</a></li> <li><a href="/wiki/Rhapsody_(syst%C3%A8me_d%27exploitation)" title="Rhapsody (système d'exploitation)">Rhapsody</a></li> <li><a href="/wiki/Darwin_(informatique)" title="Darwin (informatique)">Darwin</a></li> <li><a href="/wiki/MacOS" title="MacOS">macOS</a></li> <li><a href="/wiki/IOS" title="IOS">iOS</a></li></ul> </div></td> </tr> </tbody></table></td> </tr> <tr> <th class="navbox-group" style="">Dérivés de <a href="/wiki/BeOS" title="BeOS">BeOS</a></th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/BlueEyedOS" title="BlueEyedOS">BlueEyedOS</a></li> <li><a href="/wiki/Haiku_(syst%C3%A8me_d%27exploitation)" title="Haiku (système d'exploitation)">Haiku</a></li> <li><a href="/wiki/ZETA" title="ZETA">ZETA</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Disk_operating_system" title="Disk operating system">DOS</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/DR-DOS" title="DR-DOS">DR-DOS</a></li> <li><a href="/wiki/FreeDOS" title="FreeDOS">FreeDOS</a></li> <li><a href="/wiki/MS-DOS" title="MS-DOS">MS-DOS</a></li> <li><a href="/wiki/DOS" title="DOS">PC-DOS</a></li> <li><a href="/wiki/Open_DOS" title="Open DOS">Open DOS</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/IBM" title="IBM">IBM</a></th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/AIX" title="AIX">AIX</a></li> <li><a href="/wiki/Multiple_Virtual_Storage" title="Multiple Virtual Storage">MVS</a></li> <li><a href="/wiki/OS/2" title="OS/2">OS/2</a></li> <li><a href="/wiki/OS/360" title="OS/360">OS/360</a></li> <li><a href="/wiki/OS/390" title="OS/390">OS/390</a></li> <li><a href="/wiki/Z/OS" title="Z/OS">z/OS</a></li> <li><a href="/wiki/OS/400" title="OS/400">OS/400</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Microsoft_Windows" title="Microsoft Windows">Microsoft Windows</a></th> <td class="navbox-list" style=""><table class="navbox-subgroup" style=""> <tbody><tr> <th class="navbox-group" style="">Fondés sur MS-DOS</th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Windows_1.0" title="Windows 1.0">1.0</a></li> <li><a href="/wiki/Windows_2.x" title="Windows 2.x">2.x</a></li> <li><a href="/wiki/Windows_3.x" title="Windows 3.x">3.x</a></li> <li><a href="/wiki/Windows_95" title="Windows 95">95</a></li> <li><a href="/wiki/Windows_98" title="Windows 98">98</a></li> <li><a href="/wiki/Windows_Millennium_Edition" title="Windows Millennium Edition">ME</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Branche NT</th> <td class="navbox-list navbox-even" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Windows_NT_3.x" title="Windows NT 3.x">NT 3.x</a></li> <li><a href="/wiki/Windows_NT_4.0" title="Windows NT 4.0">NT 4.0</a></li> <li><a href="/wiki/Windows_2000" title="Windows 2000">2000</a></li> <li><a href="/wiki/Windows_XP" title="Windows XP">XP</a></li> <li><a href="/wiki/Windows_Server_2003" title="Windows Server 2003">2003</a></li> <li><a href="/wiki/Windows_Vista" title="Windows Vista">Vista</a></li> <li><a href="/wiki/Windows_Server_2008" title="Windows Server 2008">2008</a> <ul><li><a href="/wiki/Windows_Server_2008_R2" title="Windows Server 2008 R2">R2</a></li></ul></li> <li><a href="/wiki/Windows_7" title="Windows 7">7</a></li> <li><a href="/wiki/Windows_Server_2012" title="Windows Server 2012">2012</a> <ul><li><a href="/wiki/Windows_Server_2012_R2" title="Windows Server 2012 R2">R2</a></li></ul></li> <li><a href="/wiki/Windows_8" title="Windows 8">8 / 8.1</a></li> <li><a href="/wiki/Windows_Server_2016" title="Windows Server 2016">2016</a></li> <li><a href="/wiki/Windows_10" title="Windows 10">10</a></li> <li><a href="/wiki/Windows_Server_2019" title="Windows Server 2019">2019</a></li> <li><a href="/wiki/Windows_Server_2022" title="Windows Server 2022">2022</a></li> <li><a href="/wiki/Windows_11" title="Windows 11">11</a></li></ul> </div></td> </tr> </tbody></table></td> </tr> <tr> <th class="navbox-group" style=""><a href="/w/index.php?title=ReactOS_Foundation&action=edit&redlink=1" class="new" title="ReactOS Foundation (page inexistante)">ReactOS Foundation</a></th> <td class="navbox-list navbox-even" style=""><table class="navbox-subgroup" style=""> <tbody><tr> <th class="navbox-group" style="">Branche NT (GPL/LGPL/AGPL) non-Microsoft</th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/ReactOS" title="ReactOS">ReactOS</a></li></ul> </div></td> </tr> </tbody></table></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/POSIX" title="POSIX">POSIX</a> / <a href="/wiki/Unix" title="Unix">Unix</a></th> <td class="navbox-list" style=""><table class="navbox-subgroup" style=""> <tbody><tr> <th class="navbox-group" style=""><a href="/wiki/American_Telephone_%26_Telegraph" title="American Telephone & Telegraph">AT&T</a> / <a href="/wiki/Laboratoires_Bell" title="Laboratoires Bell">Laboratoires Bell</a></th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Unix_version_6" title="Unix version 6">Unix version 6</a></li> <li><a href="/wiki/Unix_version_7" title="Unix version 7">Unix version 7</a></li> <li><a href="/w/index.php?title=UNIX_System_III&action=edit&redlink=1" class="new" title="UNIX System III (page inexistante)"><span class="lang-en" lang="en">System</span> <abbr class="abbr" title="3"><span class="romain" style="text-transform:uppercase">III</span></abbr></a> <a href="https://en.wikipedia.org/wiki/UNIX_System_III" class="extiw" title="en:UNIX System III"><span class="indicateur-langue" title="Article en anglais : « UNIX System III »">(en)</span></a></li> <li><a href="/wiki/UNIX_System_V" title="UNIX System V"><span class="lang-en" lang="en">System</span> <abbr class="abbr" title="5"><span class="romain" style="text-transform:uppercase">V</span></abbr></a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Berkeley_Software_Distribution" title="Berkeley Software Distribution">BSD</a></th> <td class="navbox-list navbox-even" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/FreeBSD" title="FreeBSD">FreeBSD</a></li> <li><a href="/wiki/TrueOS" title="TrueOS">TrueOS</a></li> <li><a href="/wiki/GhostBSD" title="GhostBSD">GhostBSD</a></li> <li><a href="/wiki/DragonFly_BSD" title="DragonFly BSD">DragonFly BSD</a></li> <li><a href="/wiki/TrueNas" title="TrueNas">TrueNas</a></li> <li><a href="/wiki/OpenBSD" title="OpenBSD">OpenBSD</a></li> <li><a href="/wiki/NetBSD" title="NetBSD">NetBSD</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/GNU_Hurd" title="GNU Hurd">GNU Hurd</a></th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Debian_GNU/Hurd" title="Debian GNU/Hurd">Debian GNU/Hurd</a></li> <li><a href="/wiki/Arch_Hurd" title="Arch Hurd">Arch Hurd</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Linux" title="Linux">Linux</a> <small>(<a href="/wiki/Liste_des_distributions_GNU/Linux" title="Liste des distributions GNU/Linux">liste</a>)</small></th> <td class="navbox-list navbox-even" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Arch_Linux" title="Arch Linux">Arch Linux</a></li> <li><a href="/wiki/Calculate_Linux" title="Calculate Linux">Calculate Linux</a></li> <li><a href="/wiki/CentOS" title="CentOS">CentOS</a></li> <li><a href="/wiki/Debian" title="Debian">Debian</a></li> <li><a href="/wiki/Gentoo_Linux" title="Gentoo Linux">Gentoo</a></li> <li><a href="/wiki/GNU_Guix" title="GNU Guix">GNU Guix</a></li> <li><a href="/wiki/Fedora_Linux" title="Fedora Linux">Fedora</a></li> <li><a href="/wiki/Mageia" title="Mageia">Mageia</a></li> <li><a href="/wiki/Manjaro_Linux" title="Manjaro Linux">Manjaro</a></li> <li><a href="/wiki/Linux_Mint" title="Linux Mint">Mint</a></li> <li><a href="/wiki/OpenSUSE" title="OpenSUSE">openSUSE</a></li> <li><a href="/wiki/PCLinuxOS" title="PCLinuxOS">PCLinuxOS</a></li> <li><a href="/wiki/Puppy_Linux" title="Puppy Linux">Puppy</a></li> <li><a href="/wiki/Red_Hat_Enterprise_Linux" title="Red Hat Enterprise Linux">Red Hat</a></li> <li><a href="/wiki/Slackware" title="Slackware">Slackware</a></li> <li><a href="/wiki/Ubuntu_(syst%C3%A8me_d%27exploitation)" title="Ubuntu (système d'exploitation)">Ubuntu</a></li> <li><a href="/wiki/Raspberry_Pi_OS" title="Raspberry Pi OS">Raspberry Pi OS</a></li> <li><a href="/wiki/Chromium_OS" title="Chromium OS">Chromium OS</a>/<a href="/wiki/ChromeOS" title="ChromeOS">ChromeOS</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Autres dérivés</th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/AIX" title="AIX">AIX</a></li> <li>Apache <a href="/wiki/NuttX" title="NuttX">NuttX</a></li> <li><a href="/wiki/ChorusOS" title="ChorusOS">ChorusOS</a></li> <li><a href="/wiki/Fuzix_OS" title="Fuzix OS">Fuzix OS</a></li> <li><a href="/wiki/HP-UX" title="HP-UX">HP-UX</a></li> <li><a href="/wiki/IRIX" title="IRIX">IRIX</a></li> <li><a href="/wiki/LynxOS" title="LynxOS">LynxOS</a></li> <li><a href="/wiki/MacOS" title="MacOS">macOS</a></li> <li><a href="/wiki/Minix" title="Minix">Minix</a></li> <li><a href="/wiki/Solaris_(syst%C3%A8me_d%27exploitation)" title="Solaris (système d'exploitation)">Oracle Solaris</a></li> <li><a href="/wiki/QNX" title="QNX">QNX</a></li> <li><a href="/wiki/Redox_(syst%C3%A8me_d%27exploitation)" title="Redox (système d'exploitation)">Redox</a></li> <li><a href="/wiki/Tru64_UNIX" title="Tru64 UNIX">Tru64</a></li> <li><a href="/wiki/Cray_UNICOS" title="Cray UNICOS">UNICOS</a></li> <li><a href="/wiki/UnixWare" title="UnixWare">UnixWare</a></li></ul> </div></td> </tr> </tbody></table></td> </tr> <tr> <th class="navbox-group" style="">Dérivés d'<a href="/wiki/AmigaOS" title="AmigaOS">AmigaOS</a></th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/MorphOS" title="MorphOS">MorphOS</a></li> <li><a href="/wiki/AROS_research_operating_system" title="AROS research operating system">AROS</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Dérivés du <a href="/wiki/The_Operating_System" title="The Operating System">TOS</a></th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/EmuTOS" title="EmuTOS">EmuTOS</a></li> <li><a href="/wiki/MiNT#1994_:_FreeMiNT" title="MiNT">FreeMiNT</a></li> <li><a href="/wiki/Geneva_(informatique)" title="Geneva (informatique)">Geneva</a></li> <li><a href="/wiki/MagiC" title="MagiC">MagiC</a></li> <li><a href="/wiki/MiNT#1993_:_MiNT_is_Now_TOS_et_MultiTOS" title="MiNT">MultiTOS</a></li> <li><a href="/wiki/N.AES" title="N.AES">N.AES</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">D’importance historique</th> <td class="navbox-list navbox-even" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/Control_Program/Monitor" title="Control Program/Monitor">CP/M</a></li> <li><a href="/wiki/Compatible_Time_Sharing_System" title="Compatible Time Sharing System">CTSS</a></li> <li><a href="/wiki/General_Comprehensive_Operating_System" title="General Comprehensive Operating System">GCOS</a></li> <li><a href="/wiki/Genera" title="Genera">Genera</a></li> <li><a href="/wiki/Incompatible_Timesharing_System" title="Incompatible Timesharing System">ITS</a></li> <li><a href="/wiki/Multics" title="Multics">Multics</a></li> <li><a href="/wiki/Plan_9_from_Bell_Labs" title="Plan 9 from Bell Labs">Plan 9</a></li> <li><a href="/wiki/QDOS" title="QDOS">QDOS</a></li> <li><a href="/wiki/RSTS" title="RSTS">RSTS</a></li> <li><a href="/wiki/TENEX" title="TENEX">TENEX</a></li> <li><a href="/wiki/TOPS-20" title="TOPS-20">TOPS-20</a></li> <li><a href="/wiki/OpenVMS" title="OpenVMS">VMS</a></li> <li><a href="/wiki/Tarantella_(entreprise)" title="Tarantella (entreprise)">SCO</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Syst%C3%A8me_d%27exploitation_mobile" title="Système d'exploitation mobile">Mobile</a></th> <td class="navbox-list" style=""><table class="navbox-subgroup" style=""> <tbody><tr> <th class="navbox-group" style="">Noyau Linux</th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Android" title="Android">Android</a></li> <li><a href="/wiki/Bada" title="Bada">Bada</a></li> <li><a href="/wiki/Firefox_OS" title="Firefox OS">Firefox OS</a></li> <li><a href="/wiki/HarmonyOS" title="HarmonyOS">HarmonyOS</a></li> <li><a href="/wiki/KaiOS" title="KaiOS">KaiOS</a></li> <li><a href="/wiki/LG_webOS" title="LG webOS">LG webOS</a></li> <li><a href="/wiki/Sailfish_OS" title="Sailfish OS">Sailfish OS</a></li> <li><a href="/wiki/Tizen" title="Tizen">Tizen</a></li> <li><a href="/wiki/Ubuntu_Touch" title="Ubuntu Touch">Ubuntu Touch</a></li> <li><a href="/wiki/Ubuntu_Touch" title="Ubuntu Touch">UBports</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style="">Autres noyaux</th> <td class="navbox-list navbox-even" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/BlackBerry_OS" title="BlackBerry OS">BlackBerry OS</a></li> <li><a href="/wiki/HarmonyOS" title="HarmonyOS">HarmonyOS</a></li> <li><a href="/wiki/IOS" title="IOS">iOS</a></li> <li><a href="/wiki/Palm_OS" title="Palm OS">Palm OS</a></li> <li><a href="/wiki/Symbian_OS" title="Symbian OS">Symbian OS</a></li> <li><a href="/wiki/Windows_Phone" title="Windows Phone">Windows Phone</a></li></ul> </div></td> </tr> </tbody></table></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Syst%C3%A8me_d%27exploitation_embarqu%C3%A9" title="Système d'exploitation embarqué">Embarqués</a></th> <td class="navbox-list navbox-even" style=""><table class="navbox-subgroup" style=""> <tbody><tr> <th class="navbox-group" style=""><a href="/wiki/Syst%C3%A8me_d%27exploitation_pour_capteur_en_r%C3%A9seau" title="Système d'exploitation pour capteur en réseau">Pour capteur en réseau</a></th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Contiki" title="Contiki">Contiki</a></li> <li><a href="/wiki/TinyOS" title="TinyOS">TinyOS</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Syst%C3%A8me_d%27exploitation_pour_carte_%C3%A0_puce" title="Système d'exploitation pour carte à puce">Pour carte à puce</a></th> <td class="navbox-list navbox-even" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/Java_Card" title="Java Card">Java Card</a></li> <li><a href="/wiki/MULTOS" title="MULTOS">MULTOS</a></li></ul> </div></td> </tr> <tr> <th class="navbox-group" style=""><a href="/wiki/Syst%C3%A8me_temps_r%C3%A9el" title="Système temps réel">Temps réel</a></th> <td class="navbox-list" style=";"><div class="liste-horizontale"> <ul><li><a href="/wiki/ECos" title="ECos">eCos</a></li> <li><a href="/wiki/FreeRTOS" title="FreeRTOS">FreeRTOS</a></li> <li><a href="/wiki/Linux_embarqu%C3%A9" title="Linux embarqué">Linux embarqué</a></li> <li><a href="/wiki/LiteOS" title="LiteOS">LiteOS</a></li> <li><a href="/wiki/LynxOS" title="LynxOS">LynxOS</a></li> <li><a href="/wiki/MenuetOS" title="MenuetOS">MenuetOS</a></li> <li><a href="/wiki/NuttX" title="NuttX">NuttX</a></li> <li><a href="/wiki/OS-9" title="OS-9">OS-9</a></li> <li><a href="/wiki/PikeOS" title="PikeOS">PikeOS</a></li> <li><a href="/wiki/QNX" title="QNX">QNX</a></li> <li><a href="/wiki/RTEMS" title="RTEMS">RTEMS</a></li> <li><a href="/wiki/RTLinux" title="RTLinux">RTLinux</a></li> <li><a href="/wiki/RT-Thread" title="RT-Thread">RT-Thread</a></li> <li><a href="/wiki/RTX" title="RTX">RTX</a></li> <li><a href="/wiki/MicroC/OS-II" title="MicroC/OS-II">µC/OS-II</a></li> <li><a href="/wiki/VxWorks" title="VxWorks">VxWorks</a></li> <li><a href="/wiki/Zephyr_(syst%C3%A8me_d%27exploitation)" title="Zephyr (système d'exploitation)">Zephyr</a></li></ul> </div></td> </tr> </tbody></table></td> </tr> <tr> <th class="navbox-group" style="">Autres systèmes</th> <td class="navbox-list" style=""><div class="liste-horizontale"> <ul><li><a href="/wiki/EyeOS" title="EyeOS">eyeOS</a></li> <li><a href="/wiki/Cisco_IOS" title="Cisco IOS">Cisco IOS</a></li> <li><a href="/wiki/Inferno_(syst%C3%A8me_d%27exploitation)" title="Inferno (système d'exploitation)">Inferno</a></li> <li><a href="/wiki/MenuetOS" title="MenuetOS">MenuetOS</a></li> <li><a href="/wiki/Orbis_OS" title="Orbis OS">Orbis OS</a></li> <li><a class="mw-selflink selflink">CertiKOS</a></li></ul> </div></td> </tr> <tr> <td class="navbox-banner" style="" colspan="2"><i>Pour une liste complète, voir la <a href="/wiki/Liste_des_syst%C3%A8mes_d%27exploitation" title="Liste des systèmes d'exploitation">liste des systèmes d’exploitation</a> et la <a href="/wiki/Cat%C3%A9gorie:Syst%C3%A8me_d%27exploitation" title="Catégorie:Système d'exploitation">catégorie « Système d’exploitation »</a>.</i></td></tr></tbody></table> </div> <ul id="bandeau-portail" class="bandeau-portail"><li><span class="bandeau-portail-element"><span class="bandeau-portail-icone"><span class="noviewer" typeof="mw:File"><a href="/wiki/Portail:Sciences_de_l%27information_et_des_biblioth%C3%A8ques" title="Sciences de l’information et bibliothèques"><img alt="icône décorative" src="//upload.wikimedia.org/wikipedia/commons/thumb/4/4d/Circle-icons-bookshelf.svg/24px-Circle-icons-bookshelf.svg.png" decoding="async" width="24" height="24" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/4/4d/Circle-icons-bookshelf.svg/36px-Circle-icons-bookshelf.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/4/4d/Circle-icons-bookshelf.svg/48px-Circle-icons-bookshelf.svg.png 2x" data-file-width="512" data-file-height="512" /></a></span></span> <span class="bandeau-portail-texte"><a href="/wiki/Portail:Sciences_de_l%27information_et_des_biblioth%C3%A8ques" title="Portail:Sciences de l'information et des bibliothèques">Sciences de l’information et bibliothèques</a></span> </span></li> <li><span class="bandeau-portail-element"><span class="bandeau-portail-icone"><span class="noviewer" typeof="mw:File"><a href="/wiki/Portail:Informatique" title="Portail de l’informatique"><img alt="icône décorative" src="//upload.wikimedia.org/wikipedia/commons/thumb/0/02/Circle-icons-computer.svg/24px-Circle-icons-computer.svg.png" decoding="async" width="24" height="24" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/0/02/Circle-icons-computer.svg/36px-Circle-icons-computer.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/0/02/Circle-icons-computer.svg/48px-Circle-icons-computer.svg.png 2x" data-file-width="512" data-file-height="512" /></a></span></span> <span class="bandeau-portail-texte"><a href="/wiki/Portail:Informatique" title="Portail:Informatique">Portail de l’informatique</a></span> </span></li> <li><span class="bandeau-portail-element"><span class="bandeau-portail-icone"><span class="noviewer skin-invert-image" typeof="mw:File"><a href="/wiki/Portail:Informatique_th%C3%A9orique" title="Portail de l'informatique théorique"><img alt="icône décorative" src="//upload.wikimedia.org/wikipedia/commons/thumb/c/cf/Max-cut.svg/30px-Max-cut.svg.png" decoding="async" width="30" height="24" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/c/cf/Max-cut.svg/45px-Max-cut.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/c/cf/Max-cut.svg/60px-Max-cut.svg.png 2x" data-file-width="200" data-file-height="160" /></a></span></span> <span class="bandeau-portail-texte"><a href="/wiki/Portail:Informatique_th%C3%A9orique" title="Portail:Informatique théorique">Portail de l'informatique théorique</a></span> </span></li> <li><span class="bandeau-portail-element"><span class="bandeau-portail-icone"><span class="noviewer" typeof="mw:File"><a href="/wiki/Portail:S%C3%A9curit%C3%A9_informatique" title="Portail de la sécurité informatique"><img alt="icône décorative" src="//upload.wikimedia.org/wikipedia/commons/thumb/b/b3/Circle-icons-key.svg/24px-Circle-icons-key.svg.png" decoding="async" width="24" height="24" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/b/b3/Circle-icons-key.svg/36px-Circle-icons-key.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/b/b3/Circle-icons-key.svg/48px-Circle-icons-key.svg.png 2x" data-file-width="512" data-file-height="512" /></a></span></span> <span class="bandeau-portail-texte"><a href="/wiki/Portail:S%C3%A9curit%C3%A9_informatique" title="Portail:Sécurité informatique">Portail de la sécurité informatique</a></span> </span></li> </ul>    </div><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1&useformat=desktop" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Ce document provient de « <a dir="ltr" href="https://fr.wikipedia.org/w/index.php?title=CertiKOS&oldid=212292887">https://fr.wikipedia.org/w/index.php?title=CertiKOS&oldid=212292887</a> ».</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Cat%C3%A9gorie:Accueil" title="Catégorie:Accueil">Catégories</a> : <ul><li><a href="/wiki/Cat%C3%A9gorie:Informatique" title="Catégorie:Informatique">Informatique</a></li><li><a href="/wiki/Cat%C3%A9gorie:M%C3%A9thodologie" title="Catégorie:Méthodologie">Méthodologie</a></li><li><a href="/wiki/Cat%C3%A9gorie:M%C3%A9thode_formelle" title="Catégorie:Méthode formelle">Méthode formelle</a></li><li><a href="/wiki/Cat%C3%A9gorie:Logique_formelle" title="Catégorie:Logique formelle">Logique formelle</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Catégories cachées : <ul><li><a href="/wiki/Cat%C3%A9gorie:Article_contenant_un_appel_%C3%A0_traduction_en_anglais" title="Catégorie:Article contenant un appel à traduction en anglais">Article contenant un appel à traduction en anglais</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Sciences_de_l%27information_et_des_biblioth%C3%A8ques/Articles_li%C3%A9s" title="Catégorie:Portail:Sciences de l'information et des bibliothèques/Articles liés">Portail:Sciences de l'information et des bibliothèques/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Sciences_humaines_et_sociales/Articles_li%C3%A9s" title="Catégorie:Portail:Sciences humaines et sociales/Articles liés">Portail:Sciences humaines et sociales/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Informatique/Articles_li%C3%A9s" title="Catégorie:Portail:Informatique/Articles liés">Portail:Informatique/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Technologies/Articles_li%C3%A9s" title="Catégorie:Portail:Technologies/Articles liés">Portail:Technologies/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:Informatique_th%C3%A9orique/Articles_li%C3%A9s" title="Catégorie:Portail:Informatique théorique/Articles liés">Portail:Informatique théorique/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Projet:Math%C3%A9matiques/Articles" title="Catégorie:Projet:Mathématiques/Articles">Projet:Mathématiques/Articles</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:S%C3%A9curit%C3%A9_informatique/Articles_li%C3%A9s" title="Catégorie:Portail:Sécurité informatique/Articles liés">Portail:Sécurité informatique/Articles liés</a></li><li><a href="/wiki/Cat%C3%A9gorie:Portail:S%C3%A9curit%C3%A9_de_l%27information/Articles_li%C3%A9s" title="Catégorie:Portail:Sécurité de l'information/Articles liés">Portail:Sécurité de l'information/Articles liés</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> La dernière modification de cette page a été faite le 9 février 2024 à 15:10.</li> <li id="footer-info-copyright"><span style="white-space: normal"><a href="/wiki/Wikip%C3%A9dia:Citation_et_r%C3%A9utilisation_du_contenu_de_Wikip%C3%A9dia" title="Wikipédia:Citation et réutilisation du contenu de Wikipédia">Droit d'auteur</a> : les textes sont disponibles sous <a rel="nofollow" class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.fr">licence Creative Commons attribution, partage dans les mêmes conditions</a> ; d’autres conditions peuvent s’appliquer. Voyez les <a class="external text" href="https://foundation.wikimedia.org/wiki/Policy:Terms_of_Use/fr">conditions d’utilisation</a> pour plus de détails, ainsi que les <a href="/wiki/Wikip%C3%A9dia:Cr%C3%A9dits_graphiques" title="Wikipédia:Crédits graphiques">crédits graphiques</a>. En cas de réutilisation des textes de cette page, voyez <a href="/wiki/Sp%C3%A9cial:Citer/CertiKOS" title="Spécial:Citer/CertiKOS">comment citer les auteurs et mentionner la licence</a>.<br /> Wikipedia® est une marque déposée de la <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, organisation de bienfaisance régie par le paragraphe <a href="/wiki/501c" title="501c">501(c)(3)</a> du code fiscal des États-Unis.</span><br /></li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy/fr">Politique de confidentialité</a></li> <li id="footer-places-about"><a href="/wiki/Wikip%C3%A9dia:%C3%80_propos_de_Wikip%C3%A9dia">À propos de Wikipédia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikip%C3%A9dia:Avertissements_g%C3%A9n%C3%A9raux">Avertissements</a></li> <li id="footer-places-contact"><a href="//fr.wikipedia.org/wiki/Wikipédia:Contact">Contact</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code de conduite</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Développeurs</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/fr.wikipedia.org">Statistiques</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Déclaration sur les témoins (cookies)</a></li> <li id="footer-places-mobileview"><a href="//fr.m.wikipedia.org/w/index.php?title=CertiKOS&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Version mobile</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/w/resources/assets/poweredby_mediawiki.svg" alt="Powered by MediaWiki" width="88" height="31" loading="lazy"></a></li> </ul> </footer> </div> </div> </div> <div class="vector-settings" id="p-dock-bottom"> <ul></ul> </div><script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-7fc47fc68d-7jhxq","wgBackendResponseTime":696,"wgPageParseReport":{"limitreport":{"cputime":"0.445","walltime":"0.528","ppvisitednodes":{"value":9826,"limit":1000000},"postexpandincludesize":{"value":180261,"limit":2097152},"templateargumentsize":{"value":37260,"limit":2097152},"expansiondepth":{"value":24,"limit":100},"expensivefunctioncount":{"value":1,"limit":500},"unstrip-depth":{"value":0,"limit":20},"unstrip-size":{"value":30515,"limit":5000000},"entityaccesscount":{"value":1,"limit":400},"timingprofile":["100.00% 398.866 1 -total"," 18.45% 73.581 18 Modèle:Article"," 15.77% 62.897 1 Modèle:Portail"," 13.37% 53.341 34 Modèle:Sfn"," 13.36% 53.293 1 Modèle:Références"," 12.10% 48.267 1 Modèle:Palette"," 10.97% 43.754 20 Modèle:Lien_web"," 10.81% 43.107 1 Modèle:Palette_Systèmes_d'exploitation"," 10.36% 41.317 1 Modèle:Méta_palette_de_navigation"," 8.16% 32.534 1 Modèle:Catégorisation_badges"]},"scribunto":{"limitreport-timeusage":{"value":"0.133","limit":"10.000"},"limitreport-memusage":{"value":5129711,"limit":52428800}},"cachereport":{"origin":"mw-web.codfw.main-7fc47fc68d-7jhxq","timestamp":"20241128161737","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"CertiKOS","url":"https:\/\/fr.wikipedia.org\/wiki\/CertiKOS","sameAs":"http:\/\/www.wikidata.org\/entity\/Q60965189","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q60965189","author":{"@type":"Organization","name":"Contributeurs aux projets Wikimedia"},"publisher":{"@type":"Organization","name":"Fondation Wikimedia, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2019-01-08T09:22:26Z","dateModified":"2024-02-09T14:10:28Z"}</script> </body> </html>