{"id":84726,"date":"2020-06-10T13:42:19","date_gmt":"2020-06-10T11:42:19","guid":{"rendered":"https:\/\/prohoster.info\/blog\/novosti-interneta\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v"},"modified":"2020-06-10T13:42:19","modified_gmt":"2020-06-10T11:42:19","slug":"mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","status":"publish","type":"post","link":"https:\/\/prohoster.info\/fr\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","title":{"rendered":"Le micro-noyau seL4 a \u00e9t\u00e9 math\u00e9matiquement v\u00e9rifi\u00e9 pour l'architecture RISC-V.","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"<p>Organisation RISC-V Foundation <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-is-verified-on-risc-v\/\">a d\u00e9clar\u00e9<\/a><\/noindex> concernant la v\u00e9rification du fonctionnement du micro-noyau <noindex><a rel=\"nofollow\" href=\"https:\/\/github.com\/seL4\/seL4\">seL4<\/a><\/noindex>  sur des syst\u00e8mes avec une architecture de jeu d'instructions RISC-V. La v\u00e9rification se r\u00e9sume \u00e0 <noindex><a rel=\"nofollow\" href=\"https:\/\/www.opennet.ru\/opennews\/art.shtml?num=23011\">une preuve math\u00e9matique<\/a><\/noindex> de la fiabilit\u00e9 du seL4, qui t\u00e9moigne de la conformit\u00e9 totale avec les sp\u00e9cifications \u00e9tablies dans un langage formel. La preuve de fiabilit\u00e9 <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-operating-system-protects-critical-systems-on-risc-v-architecture-from-cyber-attacks\/\">permet d'utiliser<\/a><\/noindex> seL4 dans des syst\u00e8mes critiques bas\u00e9s sur les processeurs RISC-V RV64, qui n\u00e9cessitent un niveau de fiabilit\u00e9 accru et garantissent l'absence de pannes. Les d\u00e9veloppeurs de logiciels fonctionnant au-dessus du noyau seL4 peuvent \u00eatre pleinement assur\u00e9s que, en cas de d\u00e9faillance d'une partie du syst\u00e8me, cette d\u00e9faillance ne se propagera pas au reste du syst\u00e8me et, en particulier, \u00e0 ses parties critiques. <\/p>\n<p>\u00c0 l'origine, le micro-noyau seL4 a \u00e9t\u00e9 v\u00e9rifi\u00e9 pour des processeurs ARM 32 bits, puis pour des processeurs x86 64 bits. On note que la combinaison de l'architecture mat\u00e9rielle ouverte RISC-V avec le micro-noyau ouvert seL4 permettra d'atteindre un nouveau niveau de s\u00e9curit\u00e9, car les composants mat\u00e9riels pourraient \u00e9galement \u00eatre enti\u00e8rement v\u00e9rifi\u00e9s \u00e0 l'avenir, ce qui n'est pas r\u00e9alisable pour les architectures mat\u00e9rielles propri\u00e9taires. <\/p>\n<p>Lors de la v\u00e9rification de seL4, il est suppos\u00e9 que le mat\u00e9riel fonctionne comme annonc\u00e9 et que la sp\u00e9cification d\u00e9crit compl\u00e8tement le comportement du syst\u00e8me. Cependant, en r\u00e9alit\u00e9, le mat\u00e9riel n'est pas exempt d'erreurs, ce qui est bien illustr\u00e9 par les probl\u00e8mes r\u00e9currents li\u00e9s au m\u00e9canisme d'ex\u00e9cution sp\u00e9culative des instructions. Les plateformes mat\u00e9rielles ouvertes facilitent l'int\u00e9gration des modifications li\u00e9es \u00e0 la s\u00e9curit\u00e9 \u2014 par exemple, pour bloquer tous les canaux de fuite potentiels par des voies secondaires, o\u00f9 il est souvent plus efficace de r\u00e9soudre le probl\u00e8me mat\u00e9riellement plut\u00f4t que d'essayer de contourner la question par des solutions logicielles.<\/p>\n<p>Rappelons que l'architecture seL4 <noindex><a rel=\"nofollow\" href=\"http:\/\/sel4.systems\/FAQ\/\">est remarquable<\/a><\/noindex> la d\u00e9localisation des parties pour la gestion des ressources du noyau dans l'espace utilisateur et l'application des m\u00eames moyens de s\u00e9paration d'acc\u00e8s pour ces ressources que pour les ressources utilisateur. Le micro-noyau ne fournit pas d'abstractions de haut niveau pr\u00eates \u00e0 l'emploi pour la gestion des fichiers, des processus, des connexions r\u00e9seau, etc. Il ne propose que des m\u00e9canismes minimaux pour g\u00e9rer l'acc\u00e8s \u00e0 l'espace d'adresses physiques, aux interruptions et aux ressources du processeur. Les abstractions de haut niveau et les pilotes pour interagir avec le mat\u00e9riel sont mis en \u0153uvre s\u00e9par\u00e9ment au-dessus du micro-noyau sous la forme de t\u00e2ches ex\u00e9cut\u00e9es au niveau utilisateur. L'acc\u00e8s de ces t\u00e2ches aux ressources disponibles aupr\u00e8s du micro-noyau est organis\u00e9 par la d\u00e9finition de r\u00e8gles.<\/p>\n<p>RISC-V fournit un syst\u00e8me d'instructions machine ouvert et flexible, permettant de cr\u00e9er des microprocesseurs pour des applications vari\u00e9es, sans n\u00e9cessiter de redevances et sans imposer de conditions d'utilisation. RISC-V permet de cr\u00e9er des SoC et des processeurs enti\u00e8rement ouverts. Actuellement, des dizaines d'options de noyaux de microprocesseurs, SoC et de puces d\u00e9j\u00e0 produites sont bas\u00e9es sur la sp\u00e9cification RISC-V, par diff\u00e9rentes entreprises et communaut\u00e9s sous diverses licences gratuites (BSD, MIT, Apache 2.0). <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/risc-v-cores\/\">\u00e9volue<\/a><\/noindex> Le support de RISC-V est pr\u00e9sent depuis les versions de Glibc 2.27, binutils 2.30, gcc 7 et du noyau Linux 4.15.<\/p>\n<p><noindex><a rel=\"nofollow\" name=\"link\"><\/a><\/noindex><\/p>\n<p>Source : <a \ncontent=\"nofollow\" rel=\"nofollow\" href=\"https:\/\/www.opennet.ru\/opennews\/art.shtml?num=53129\">opennet.ru<\/a><\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"<p>\u041e\u0440\u0433\u0430\u043d\u0438\u0437\u0430\u0446\u0438\u044f RISC-V Foundation \u0441\u043e\u043e\u0431\u0449\u0438\u043b\u0430 \u043e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0440\u0430\u0431\u043e\u0442\u044b \u043c\u0438\u043a\u0440\u043e\u044f\u0434\u0440\u0430 seL4 \u043d\u0430 \u0441\u0438\u0441\u0442\u0435\u043c\u0430\u0445 \u0441 \u0430\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u043e\u0439 \u043d\u0430\u0431\u043e\u0440\u0430 \u043a\u043e\u043c\u0430\u043d\u0434 RISC-V. \u0412\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0441\u0432\u043e\u0434\u0438\u0442\u0441\u044f \u043a \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u043c\u0443 \u0434\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0443 \u043d\u0430\u0434\u0451\u0436\u043d\u043e\u0441\u0442\u0438 \u0440\u0430\u0431\u043e\u0442\u044b seL4, \u043a\u043e\u0442\u043e\u0440\u043e\u0435 \u0441\u0432\u0438\u0434\u0435\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u0443\u0435\u0442 \u043e \u043f\u043e\u043b\u043d\u043e\u043c \u0441\u043e\u043e\u0442\u0432\u0435\u0442\u0441\u0442\u0432\u0438\u0438 \u0437\u0430\u0434\u0430\u043d\u043d\u044b\u043c \u043d\u0430 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u043c \u044f\u0437\u044b\u043a\u0435 \u0441\u043f\u0435\u0446\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f\u043c. \u0414\u043e\u043a\u0430\u0437\u0430\u0442\u0435\u043b\u044c\u0441\u0442\u0432\u043e \u043d\u0430\u0434\u0451\u0436\u043d\u043e\u0441\u0442\u0438 \u043f\u043e\u0437\u0432\u043e\u043b\u044f\u0435\u0442 \u0438\u0441\u043f\u043e\u043b\u044c\u0437\u043e\u0432\u0430\u0442\u044c seL4 \u0432 \u043a\u0440\u0438\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0432\u0430\u0436\u043d\u044b\u0445 \u0441\u0438\u0441\u0442\u0435\u043c\u0430\u0445 \u043d\u0430 \u0431\u0430\u0437\u0435 \u043f\u0440\u043e\u0446\u0435\u0441\u0441\u043e\u0440\u043e\u0432 RISC-V RV64, \u0442\u0440\u0435\u0431\u0443\u044e\u0449\u0438\u0445 \u043f\u043e\u0432\u044b\u0448\u0435\u043d\u043d\u043e\u0433\u043e \u0443\u0440\u043e\u0432\u043d\u044f \u043d\u0430\u0434\u0451\u0436\u043d\u043e\u0441\u0442\u0438 \u0438 \u0433\u0430\u0440\u0430\u043d\u0442\u0438\u0440\u0443\u044e\u0449\u0438\u0445 \u043e\u0442\u0441\u0443\u0442\u0441\u0442\u0432\u0438\u0435 [&hellip;]<\/p>\n","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[702],"tags":[],"class_list":["post-84726","post","type-post","status-publish","format-standard","hentry","category-news"],"aioseo_notices":[],"aioseo_head":"\n\t\t<!-- All in One SEO 5.0.2 - aioseo.com -->\n\t<meta name=\"description\" content=\"\u041e\u0440\u0433\u0430\u043d\u0438\u0437\u0430\u0446\u0438\u044f RISC-V Foundation \u0441\u043e\u043e\u0431\u0449\u0438\u043b\u0430 \u043e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0440\u0430\u0431\u043e\u0442\u044b \u043c\u0438\u043a\u0440\u043e\u044f\u0434\u0440\u0430\" \/>\n\t<meta name=\"robots\" content=\"max-image-preview:large\" \/>\n\t<meta name=\"author\" content=\"Yuri Gagarin\"\/>\n\t<link rel=\"canonical\" href=\"https:\/\/prohoster.info\/fr\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v\" \/>\n\t<meta name=\"generator\" content=\"All in One SEO (AIOSEO) 5.0.2\" \/>\n\t\t<meta property=\"og:locale\" content=\"fr_FR\" \/>\n\t\t<meta property=\"og:site_name\" content=\"ProHoster | \u041a\u0443\u043f\u0438\u0442\u044c \u043d\u0430\u0434\u0435\u0436\u043d\u044b\u0439 \u0445\u043e\u0441\u0442\u0438\u043d\u0433 \u0434\u043b\u044f \u0441\u0430\u0439\u0442\u043e\u0432 \u0441 \u0437\u0430\u0449\u0438\u0442\u043e\u0439 \u043e\u0442 DDoS, VPS VDS \u0441\u0435\u0440\u0432\u0435\u0440\u044b\" \/>\n\t\t<meta property=\"og:type\" content=\"article\" \/>\n\t\t<meta property=\"og:title\" content=\"\ud83e\udd47\u041c\u0438\u043a\u0440\u043e\u044f\u0434\u0440\u043e seL4 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043e \u0434\u043b\u044f \u0430\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u044b RISC-V | ProHoster\" \/>\n\t\t<meta property=\"og:description\" content=\"\u041e\u0440\u0433\u0430\u043d\u0438\u0437\u0430\u0446\u0438\u044f RISC-V Foundation \u0441\u043e\u043e\u0431\u0449\u0438\u043b\u0430 \u043e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0440\u0430\u0431\u043e\u0442\u044b \u043c\u0438\u043a\u0440\u043e\u044f\u0434\u0440\u0430\" \/>\n\t\t<meta property=\"og:url\" content=\"https:\/\/prohoster.info\/fr\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v\" \/>\n\t\t<meta property=\"og:image\" content=\"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg\" \/>\n\t\t<meta property=\"og:image:secure_url\" content=\"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg\" \/>\n\t\t<meta property=\"og:image:width\" content=\"350\" \/>\n\t\t<meta property=\"og:image:height\" content=\"350\" \/>\n\t\t<meta property=\"article:published_time\" content=\"2020-06-10T11:42:19+00:00\" \/>\n\t\t<meta property=\"article:modified_time\" content=\"2020-06-10T11:42:19+00:00\" \/>\n\t\t<meta property=\"article:publisher\" content=\"https:\/\/www.facebook.com\/prohoster\" \/>\n\t\t<meta property=\"article:author\" content=\"https:\/\/www.facebook.com\/prohoster\" \/>\n\t\t<!-- All in One SEO -->\n\n","aioseo_head_json":{"title":"\ud83e\udd47Le micro-noyau seL4 est math\u00e9matiquement v\u00e9rifi\u00e9 pour l'architecture RISC-V | ProHoster","description":"L'organisation RISC-V Foundation a annonc\u00e9 la v\u00e9rification du fonctionnement du micro-noyau.","canonical_url":"https:\/\/prohoster.info\/fr\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"fr_FR","og:site_name":"ProHoster | \u041a\u0443\u043f\u0438\u0442\u044c \u043d\u0430\u0434\u0435\u0436\u043d\u044b\u0439 \u0445\u043e\u0441\u0442\u0438\u043d\u0433 \u0434\u043b\u044f \u0441\u0430\u0439\u0442\u043e\u0432 \u0441 \u0437\u0430\u0449\u0438\u0442\u043e\u0439 \u043e\u0442 DDoS, VPS VDS \u0441\u0435\u0440\u0432\u0435\u0440\u044b","og:type":"article","og:title":"\ud83e\udd47\u041c\u0438\u043a\u0440\u043e\u044f\u0434\u0440\u043e seL4 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u0438 \u0432\u0435\u0440\u0438\u0444\u0438\u0446\u0438\u0440\u043e\u0432\u0430\u043d\u043e \u0434\u043b\u044f \u0430\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u044b RISC-V | ProHoster","og:description":"\u041e\u0440\u0433\u0430\u043d\u0438\u0437\u0430\u0446\u0438\u044f RISC-V Foundation \u0441\u043e\u043e\u0431\u0449\u0438\u043b\u0430 \u043e \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0438 \u0440\u0430\u0431\u043e\u0442\u044b \u043c\u0438\u043a\u0440\u043e\u044f\u0434\u0440\u0430","og:url":"https:\/\/prohoster.info\/fr\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","og:image":"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg","og:image:secure_url":"https:\/\/prohoster.info\/wp-content\/uploads\/2021\/11\/logo-350.jpg","og:image:width":350,"og:image:height":350,"article:published_time":"2020-06-10T11:42:19+00:00","article:modified_time":"2020-06-10T11:42:19+00:00","article:publisher":"https:\/\/www.facebook.com\/prohoster","article:author":"https:\/\/www.facebook.com\/prohoster"},"aioseo_meta_data":{"post_id":"84726","title":null,"description":null,"keywords":null,"keyphrases":null,"primary_term":null,"canonical_url":null,"og_title":null,"og_description":null,"og_object_type":"default","og_image_type":"default","og_image_url":null,"og_image_width":null,"og_image_height":null,"og_image_custom_url":null,"og_image_custom_fields":null,"og_video":null,"og_custom_url":null,"og_article_section":null,"og_article_tags":null,"twitter_use_og":false,"twitter_card":"default","twitter_image_type":"default","twitter_image_url":null,"twitter_image_custom_url":null,"twitter_image_custom_fields":null,"twitter_title":null,"twitter_description":null,"schema":{"blockGraphs":[],"customGraphs":[],"default":{"data":{"Article":[],"Course":[],"Dataset":[],"FAQPage":[],"Movie":[],"Person":[],"Product":[],"ProductReview":[],"Car":[],"Recipe":[],"Service":[],"SoftwareApplication":[],"WebPage":[]},"graphName":"","isEnabled":true},"graphs":[]},"schema_type":null,"schema_type_options":null,"pillar_content":false,"robots_default":true,"robots_noindex":false,"robots_noarchive":false,"robots_nosnippet":false,"robots_nofollow":false,"robots_noimageindex":false,"robots_noodp":false,"robots_notranslate":false,"robots_max_snippet":null,"robots_max_videopreview":null,"robots_max_imagepreview":"large","priority":null,"frequency":null,"local_seo":null,"seo_analyzer_scan_date":null,"breadcrumb_settings":null,"limit_modified_date":false,"reviewed_by":null,"ai":null,"created":"2021-02-28 14:52:36","updated":"2022-10-01 14:07:46","focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"gt_translate_keys":[{"key":"link","format":"url"}],"_links":{"self":[{"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/posts\/84726","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/comments?post=84726"}],"version-history":[{"count":0,"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/posts\/84726\/revisions"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/media?parent=84726"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/categories?post=84726"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/fr\/wp-json\/wp\/v2\/tags?post=84726"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}