{"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\/pl\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","title":{"rendered":"Mikrokernel seL4 matematycznie zweryfikowany dla architektury RISC-V","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"<p>Organizacja RISC-V Foundation <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-is-verified-on-risc-v\/\">powiedzia\u0142a<\/a><\/noindex> o weryfikacji dzia\u0142ania mikroj\u0105dra <noindex><a rel=\"nofollow\" href=\"https:\/\/github.com\/seL4\/seL4\">seL4<\/a><\/noindex>  na systemach z architektur\u0105 zestawu instrukcji RISC-V. Weryfikacja sprowadza si\u0119 do <noindex><a rel=\"nofollow\" href=\"https:\/\/www.opennet.ru\/opennews\/art.shtml?num=23011\">matematycznego dowodu<\/a><\/noindex> niezawodno\u015bci dzia\u0142ania seL4, co \u015bwiadczy o pe\u0142nej zgodno\u015bci z wymaganiami okre\u015blonymi w formalnych specyfikacjach j\u0119zykowych. Dow\u00f3d niezawodno\u015bci <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-operating-system-protects-critical-systems-on-risc-v-architecture-from-cyber-attacks\/\">umo\u017cliwia zastosowanie<\/a><\/noindex> seL4 w systemach krytycznych opartych na procesorach RISC-V RV64, wymagaj\u0105cych wysokiego poziomu niezawodno\u015bci i gwarantuj\u0105cych brak awarii. Programi\u015bci oprogramowania dzia\u0142aj\u0105cego na rdzeniu seL4 mog\u0105 by\u0107 ca\u0142kowicie pewni, \u017ce w przypadku awarii w jednej cz\u0119\u015bci systemu, awaria ta nie rozprzestrzeni si\u0119 na pozosta\u0142\u0105 cz\u0119\u015b\u0107 systemu, w tym na jego krytyczne elementy. <\/p>\n<p>Pocz\u0105tkowo mikroj\u0105dro seL4 zosta\u0142o zweryfikowane dla 32-bitowych procesor\u00f3w ARM, a p\u00f3\u017aniej dla 64-bitowych procesor\u00f3w x86. Zauwa\u017ca si\u0119, \u017ce po\u0142\u0105czenie otwartej architektury sprz\u0119towej RISC-V z otwartym mikroj\u0105drem seL4 pozwoli osi\u0105gn\u0105\u0107 nowy poziom bezpiecze\u0144stwa, poniewa\u017c komponenty sprz\u0119towe w przysz\u0142o\u015bci r\u00f3wnie\u017c mog\u0105 by\u0107 w pe\u0142ni weryfikowane, co nie jest mo\u017cliwe w przypadku zamkni\u0119tych architektur sprz\u0119towych. <\/p>\n<p>Podczas weryfikacji seL4 zak\u0142ada si\u0119, \u017ce sprz\u0119t dzia\u0142a zgodnie z deklaracjami, a specyfikacja w pe\u0142ni opisuje zachowanie systemu, ale w rzeczywisto\u015bci sprz\u0119t nie jest wolny od b\u0142\u0119d\u00f3w, co dobrze ilustruj\u0105 regularnie pojawiaj\u0105ce si\u0119 problemy zwi\u0105zane z mechanizmem spekulatywnego wykonania instrukcji. Otwarte platformy sprz\u0119towe u\u0142atwiaj\u0105 integracj\u0119 zmian zwi\u0105zanych z bezpiecze\u0144stwem \u2014 na przyk\u0142ad w celu zablokowania wszystkich mo\u017cliwych kana\u0142\u00f3w wycieku przez zewn\u0119trzne \u017ar\u00f3d\u0142a, gdzie skuteczniej jest rozwi\u0105za\u0107 problem sprz\u0119towo, ni\u017c pr\u00f3bowa\u0107 szuka\u0107 obej\u015b\u0107 programowo.<\/p>\n<p>Przypominamy, \u017ce architektura seL4 <noindex><a rel=\"nofollow\" href=\"http:\/\/sel4.systems\/FAQ\/\">jest niezwyk\u0142a<\/a><\/noindex> przeniesieniem element\u00f3w do zarz\u0105dzania zasobami j\u0105dra do przestrzeni u\u017cytkownika oraz zastosowaniem dla tych zasob\u00f3w tych samych \u015brodk\u00f3w ograniczania dost\u0119pu, co dla zasob\u00f3w u\u017cytkownika. Mikroj\u0105dro nie zapewnia gotowych wysokopoziomowych abstrakcji do zarz\u0105dzania plikami, procesami, po\u0142\u0105czeniami sieciowymi itp., zamiast tego dostarcza jedynie minimalne mechanizmy do zarz\u0105dzania dost\u0119pem do fizycznej przestrzeni adresowej, przerwaniami i zasobami procesora. Wysokopoziomowe abstrakcje i sterowniki do interakcji z sprz\u0119tem s\u0105 realizowane osobno na mikroj\u0105drem w formie zada\u0144 wykonywanych na poziomie u\u017cytkownika. Dost\u0119p tych zada\u0144 do zasob\u00f3w mikroj\u0105dra jest organizowany poprzez okre\u015blenie regu\u0142.<\/p>\n<p>RISC-V oferuje otwarty i elastyczny system instrukcji maszynowych, umo\u017cliwiaj\u0105cy tworzenie mikroprocesor\u00f3w do dowolnych zastosowa\u0144, nie wymagaj\u0105c przy tym op\u0142at i nie nak\u0142adaj\u0105c warunk\u00f3w na u\u017cytkowanie. RISC-V pozwala na tworzenie w pe\u0142ni otwartych SoC i procesor\u00f3w. Obecnie na podstawie specyfikacji RISC-V r\u00f3\u017cne firmy i spo\u0142eczno\u015bci tworz\u0105 pod r\u00f3\u017cnymi wolnymi licencjami (BSD, MIT, Apache 2.0) <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/risc-v-cores\/\">rozwijana jest<\/a><\/noindex> kilkadziesi\u0105t wariant\u00f3w rdzeni mikroprocesor\u00f3w, SoC i ju\u017c produkowanych chip\u00f3w. Wsparcie dla RISC-V jest obecne od wyda\u0144 Glibc 2.27, binutils 2.30, gcc 7 i j\u0105dra Linux 4.15.<\/p>\n<p><noindex><a rel=\"nofollow\" name=\"link\"><\/a><\/noindex><\/p>\n<p>\u0179r\u00f3d\u0142o: <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.1.1 - 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\/pl\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v\" \/>\n\t<meta name=\"generator\" content=\"All in One SEO (AIOSEO) 5.0.1.1\" \/>\n\t\t<meta property=\"og:locale\" content=\"pl_PL\" \/>\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\/pl\/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\u0105dro seL4 zosta\u0142o matematycznie zweryfikowane dla architektury RISC-V | ProHoster","description":"Organizacja RISC-V Foundation poinformowa\u0142a o weryfikacji dzia\u0142ania microkernel.","canonical_url":"https:\/\/prohoster.info\/pl\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"pl_PL","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\/pl\/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\/pl\/wp-json\/wp\/v2\/posts\/84726","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/comments?post=84726"}],"version-history":[{"count":0,"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/posts\/84726\/revisions"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/media?parent=84726"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/categories?post=84726"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/pl\/wp-json\/wp\/v2\/tags?post=84726"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}