{"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\/pt\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","title":{"rendered":"O microkernel seL4 foi verificado matematicamente para a arquitetura RISC-V","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"<p>Organiza\u00e7\u00e3o RISC-V Foundation <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-is-verified-on-risc-v\/\">anunciou<\/a><\/noindex> a verifica\u00e7\u00e3o do microkernel <noindex><a rel=\"nofollow\" href=\"https:\/\/github.com\/seL4\/seL4\">seL4<\/a><\/noindex>  em sistemas com arquitetura de conjunto de instru\u00e7\u00f5es RISC-V. A verifica\u00e7\u00e3o consiste em <noindex><a rel=\"nofollow\" href=\"https:\/\/www.opennet.ru\/opennews\/art.shtml?num=23011\">uma prova matem\u00e1tica<\/a><\/noindex> da confiabilidade da opera\u00e7\u00e3o do seL4, que comprova a total conformidade com as especifica\u00e7\u00f5es definidas em uma linguagem formal. A prova de confiabilidade <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-operating-system-protects-critical-systems-on-risc-v-architecture-from-cyber-attacks\/\">permite utilizar<\/a><\/noindex> o seL4 em sistemas cr\u00edticos baseados em processadores RISC-V RV64, que exigem um alto n\u00edvel de confiabilidade e garantem a aus\u00eancia de falhas. Os desenvolvedores de software que opera sobre o n\u00facleo seL4 podem ter total confian\u00e7a de que, em caso de falha em uma parte do sistema, essa falha n\u00e3o se espalhar\u00e1 para o restante do sistema e, em particular, para suas partes cr\u00edticas. <\/p>\n<p>O microkernel seL4 foi inicialmente verificado para processadores ARM de 32 bits e, posteriormente, para processadores x86 de 64 bits. \u00c9 not\u00e1vel que a combina\u00e7\u00e3o da arquitetura de hardware aberto RISC-V com o microkernel aberto seL4 permitir\u00e1 alcan\u00e7ar um novo n\u00edvel de seguran\u00e7a, uma vez que os componentes de hardware tamb\u00e9m podem ser totalmente verificados no futuro, o que n\u00e3o \u00e9 vi\u00e1vel para arquiteturas de hardware propriet\u00e1rias. <\/p>\n<p>Na verifica\u00e7\u00e3o do seL4, assume-se que o hardware funciona conforme declarado e que a especifica\u00e7\u00e3o descreve totalmente o comportamento do sistema. Contudo, o hardware n\u00e3o est\u00e1 livre de erros, o que \u00e9 bem demonstrado por problemas recorrentes que surgem no mecanismo de execu\u00e7\u00e3o especulativa de instru\u00e7\u00f5es. As plataformas de hardware abertas simplificam a integra\u00e7\u00e3o de mudan\u00e7as relacionadas \u00e0 seguran\u00e7a \u2014 por exemplo, para bloquear todos os poss\u00edveis canais de vazamento atrav\u00e9s de canais secund\u00e1rios, onde \u00e9 muito mais eficiente resolver o problema em n\u00edvel de hardware do que tentar encontrar solu\u00e7\u00f5es alternativas em n\u00edvel de software.<\/p>\n<p>Lembramos que a arquitetura seL4 <noindex><a rel=\"nofollow\" href=\"http:\/\/sel4.systems\/FAQ\/\">\u00e9 not\u00e1vel<\/a><\/noindex> a aloca\u00e7\u00e3o de partes para gerenciamento de recursos do n\u00facleo no espa\u00e7o do usu\u00e1rio e a aplica\u00e7\u00e3o das mesmas ferramentas de controle de acesso para esses recursos, como para recursos do usu\u00e1rio. O micron\u00facleo n\u00e3o fornece abstra\u00e7\u00f5es de alto n\u00edvel prontas para gerenciamento de arquivos, processos, conex\u00f5es de rede, etc., em vez disso, oferece apenas mecanismos m\u00ednimos para controlar o acesso ao espa\u00e7o de endere\u00e7os f\u00edsico, interrup\u00e7\u00f5es e recursos do processador. Abstra\u00e7\u00f5es de alto n\u00edvel e drivers para intera\u00e7\u00e3o com hardware s\u00e3o implementados separadamente sobre o micron\u00facleo na forma de tarefas executadas em n\u00edvel de usu\u00e1rio. O acesso a esses recursos do micron\u00facleo por parte dessas tarefas \u00e9 organizado atrav\u00e9s da defini\u00e7\u00e3o de regras.<\/p>\n<p>O RISC-V fornece um sistema de instru\u00e7\u00f5es de m\u00e1quina aberto e flex\u00edvel, permitindo a cria\u00e7\u00e3o de microprocessadores para diversas \u00e1reas de aplica\u00e7\u00e3o, sem exigir pagamentos e sem impor condi\u00e7\u00f5es de uso. O RISC-V possibilita a cria\u00e7\u00e3o de SoCs e processadores totalmente abertos. Atualmente, v\u00e1rias empresas e comunidades est\u00e3o desenvolvendo com base na especifica\u00e7\u00e3o RISC-V sob diversas licen\u00e7as livres (BSD, MIT, Apache 2.0). <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/risc-v-cores\/\">est\u00e1 em desenvolvimento<\/a><\/noindex> v\u00e1rias dezenas de variantes de n\u00facleos de microprocessadores, SoCs e chips j\u00e1 em produ\u00e7\u00e3o. O suporte ao RISC-V est\u00e1 presente desde as vers\u00f5es Glibc 2.27, binutils 2.30, gcc 7 e do n\u00facleo Linux 4.15.<\/p>\n<p><noindex><a rel=\"nofollow\" name=\"link\"><\/a><\/noindex><\/p>\n<p>Fonte: <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.3 - 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\/pt\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v\" \/>\n\t\t<meta name=\"generator\" content=\"All in One SEO (AIOSEO) 5.0.3\" \/>\n\t\t<meta property=\"og:locale\" content=\"pt_PT\" \/>\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\/pt\/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\udd47Micron\u00facleo seL4 verificado matematicamente para a arquitetura RISC-V | ProHoster","description":"A organiza\u00e7\u00e3o RISC-V Foundation anunciou a verifica\u00e7\u00e3o do funcionamento do micron\u00facleo","canonical_url":"https:\/\/prohoster.info\/pt\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"pt_PT","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\/pt\/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\/pt\/wp-json\/wp\/v2\/posts\/84726","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/comments?post=84726"}],"version-history":[{"count":0,"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/posts\/84726\/revisions"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/media?parent=84726"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/categories?post=84726"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/pt\/wp-json\/wp\/v2\/tags?post=84726"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}