{"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\/cs\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","title":{"rendered":"Mikroj\u00e1dro seL4 je matematicky verifikov\u00e1no pro architekturu RISC-V","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"<p>Organizace RISC-V Foundation <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-is-verified-on-risc-v\/\">ozn\u00e1mila<\/a><\/noindex> o verifikaci mikrokernel\u016f <noindex><a rel=\"nofollow\" href=\"https:\/\/github.com\/seL4\/seL4\">seL4<\/a><\/noindex>  v syst\u00e9mech s architekturou instruk\u010dn\u00edho setu RISC-V. Verifikace se soust\u0159ed\u00ed na <noindex><a rel=\"nofollow\" href=\"https:\/\/www.opennet.ru\/opennews\/art.shtml?num=23011\">matematick\u00fd d\u016fkaz<\/a><\/noindex> spolehlivosti seL4, kter\u00fd potvrzuje \u00faplnou shodu se specifikacemi zadan\u00fdmi ve form\u00e1ln\u00edm jazyce. D\u016fkaz spolehlivosti <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-operating-system-protects-critical-systems-on-risc-v-architecture-from-cyber-attacks\/\">umo\u017e\u0148uje pou\u017eit\u00ed<\/a><\/noindex> seL4 v kritick\u00fdch syst\u00e9mech zalo\u017een\u00fdch na procesorech RISC-V RV64, kter\u00e9 vy\u017eaduj\u00ed vy\u0161\u0161\u00ed \u00farove\u0148 spolehlivosti a garantuj\u00ed absenci selh\u00e1n\u00ed. V\u00fdvoj\u00e1\u0159i softwaru b\u011b\u017e\u00edc\u00edho na j\u00e1d\u0159e seL4 si mohou b\u00fdt zcela jisti, \u017ee v p\u0159\u00edpad\u011b selh\u00e1n\u00ed jedn\u00e9 \u010d\u00e1sti syst\u00e9mu se toto selh\u00e1n\u00ed ne\u0161\u00ed\u0159\u00ed na zbytek syst\u00e9mu a zejm\u00e9na na jeho kritick\u00e9 \u010d\u00e1sti. <\/p>\n<p>P\u016fvodn\u011b byl mikrokernel seL4 verifikov\u00e1n pro 32bitov\u00e9 procesory ARM a pozd\u011bji pro 64bitov\u00e9 procesory x86. Je zd\u016frazn\u011bno, \u017ee kombinace otev\u0159en\u00e9 hardwarov\u00e9 architektury RISC-V s otev\u0159en\u00fdm mikrokernelem seL4 umo\u017en\u00ed dos\u00e1hnout nov\u00e9 \u00farovn\u011b zabezpe\u010den\u00ed, proto\u017ee hardwarov\u00e9 komponenty mohou b\u00fdt tak\u00e9 pln\u011b verifikov\u00e1ny, co\u017e nen\u00ed mo\u017en\u00e9 u propriet\u00e1rn\u00edch hardwarov\u00fdch architektur. <\/p>\n<p>P\u0159i ov\u011b\u0159ov\u00e1n\u00ed seL4 se p\u0159edpokl\u00e1d\u00e1, \u017ee hardware funguje tak, jak je uvedeno, a specifikace pln\u011b popisuje chov\u00e1n\u00ed syst\u00e9mu, ale ve skute\u010dnosti hardware nen\u00ed bez chyb, co\u017e dob\u0159e demonstruj\u00ed pravideln\u011b se objevuj\u00edc\u00ed probl\u00e9my v mechanismu spekulativn\u00edho vykon\u00e1v\u00e1n\u00ed instrukc\u00ed. Otev\u0159en\u00e9 hardwarov\u00e9 platformy usnad\u0148uj\u00ed integraci zm\u011bn souvisej\u00edc\u00edch s bezpe\u010dnost\u00ed \u2014 nap\u0159\u00edklad pro blokov\u00e1n\u00ed v\u0161ech mo\u017en\u00fdch kan\u00e1l\u016f \u00faniku prost\u0159ednictv\u00edm extern\u00edch kan\u00e1l\u016f, kde je mnohem efektivn\u011bj\u0161\u00ed se probl\u00e9mu zbavit hardwarov\u011b, ne\u017e se pokou\u0161et hledat obchvaty softwarov\u011b.<\/p>\n<p>P\u0159ipome\u0148me, \u017ee architektura seL4 <noindex><a rel=\"nofollow\" href=\"http:\/\/sel4.systems\/FAQ\/\">v\u00fdznamn\u00e1<\/a><\/noindex> vyjmut\u00ed \u010d\u00e1st\u00ed pro \u0159\u00edzen\u00ed prost\u0159edk\u016f j\u00e1dra do prostoru u\u017eivatele a pou\u017eit\u00ed pro tyto prost\u0159edky stejn\u00fdch prost\u0159edk\u016f p\u0159\u00edstupu, jak\u00e9 se pou\u017e\u00edvaj\u00ed pro u\u017eivatelsk\u00e9 prost\u0159edky. Mikroj\u00e1dro neposkytuje hotov\u00e9 vysoce\u00farov\u0148ov\u00e9 abstrakce pro spr\u00e1vu soubor\u016f, proces\u016f, s\u00ed\u0165ov\u00fdch spojen\u00ed atd., m\u00edsto toho poskytuje pouze minim\u00e1ln\u00ed mechanismy pro \u0159\u00edzen\u00ed p\u0159\u00edstupu k fyzick\u00e9mu adresn\u00edmu prostoru, p\u0159eru\u0161en\u00ed a prost\u0159edk\u016fm procesoru. Vysoce\u00farov\u0148ov\u00e9 abstrakce a ovlada\u010de pro interakci s hardwarem jsou implementov\u00e1ny odd\u011blen\u011b nad mikroj\u00e1drem ve form\u011b \u00faloh vykon\u00e1van\u00fdch na u\u017eivatelsk\u00e9 \u00farovni. P\u0159\u00edstup t\u011bchto \u00faloh k prost\u0159edk\u016fm, kter\u00e9 m\u00e1 mikroj\u00e1dro k dispozici, je organizov\u00e1n prost\u0159ednictv\u00edm definice pravidel.<\/p>\n<p>RISC-V poskytuje otev\u0159en\u00fd a flexibiln\u00ed syst\u00e9m strojov\u00fdch instrukc\u00ed, kter\u00fd umo\u017e\u0148uje vytv\u00e1\u0159et mikroprocesory pro libovoln\u00e9 oblasti pou\u017eit\u00ed, ani\u017e by vy\u017eadoval licen\u010dn\u00ed poplatky a neukl\u00e1dal podm\u00ednky pro pou\u017eit\u00ed. RISC-V umo\u017e\u0148uje vytv\u00e1\u0159et zcela otev\u0159en\u00e9 SoC a procesory. V sou\u010dasn\u00e9 dob\u011b je na z\u00e1klad\u011b specifikace RISC-V r\u016fzn\u00fdmi spole\u010dnostmi a komunitami pod r\u016fzn\u00fdmi otev\u0159en\u00fdmi licencemi (BSD, MIT, Apache 2.0) k dispozici n\u011bkolik des\u00edtek variant jader mikroprocesor\u016f, SoC a ji\u017e vyr\u00e1b\u011bn\u00fdch \u010dip\u016f. Podpora RISC-V je p\u0159\u00edtomna od verz\u00ed Glibc 2.27, binutils 2.30, gcc 7 a j\u00e1dra Linux 4.15. <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/risc-v-cores\/\">se vyv\u00edj\u00ed<\/a><\/noindex> Release zvukov\u00e9ho subsyst\u00e9mu Linux \u2014 ALSA 1.2.3<\/p>\n<p><noindex><a rel=\"nofollow\" name=\"link\"><\/a><\/noindex><\/p>\n<p>Zdroj: <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\/cs\/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=\"cs_CZ\" \/>\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\/cs\/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\udd47Mikroj\u00e1dro seL4 matematicky verifikov\u00e1no pro architekturu RISC-V | ProHoster","description":"\ud83e\udd47Mikroj\u00e1dro seL4 matematicky verifikov\u00e1no pro architekturu RISC-V | ProHoster","canonical_url":"https:\/\/prohoster.info\/cs\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"cs_CZ","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\/cs\/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\/cs\/wp-json\/wp\/v2\/posts\/84726","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/comments?post=84726"}],"version-history":[{"count":0,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/posts\/84726\/revisions"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/media?parent=84726"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/categories?post=84726"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/cs\/wp-json\/wp\/v2\/tags?post=84726"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}