{"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\/nl\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","title":{"rendered":"De seL4 microkernel is wiskundig geverifieerd voor de RISC-V architectuur","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"<p>Organisatie RISC-V Foundation <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-is-verified-on-risc-v\/\">meldde<\/a><\/noindex> over de verificatie van de werking van het microkernelsysteem <noindex><a rel=\"nofollow\" href=\"https:\/\/github.com\/seL4\/seL4\">seL4<\/a><\/noindex>  op systemen met de RISC-V instructieset. De verificatie komt neer op <noindex><a rel=\"nofollow\" href=\"https:\/\/www.opennet.ru\/opennews\/art.shtml?num=23011\">wiskundig bewijs<\/a><\/noindex> van de betrouwbaarheid van seL4, wat aantoont dat het volledig voldoet aan de specificaties die in formele taal zijn vastgesteld. Het bewijs van betrouwbaarheid <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-operating-system-protects-critical-systems-on-risc-v-architecture-from-cyber-attacks\/\">maakt het mogelijk om<\/a><\/noindex> seL4 in kritieke systemen gebaseerd op RISC-V RV64-processoren te gebruiken, die een hoger niveau van betrouwbaarheid vereisen en garant staan voor het ontbreken van fouten. Ontwikkelaars van software die bovenop de seL4-kernel draait, kunnen er volledig op vertrouwen dat in het geval van een storing in een deel van het systeem, deze storing zich niet zal verspreiden naar de rest van het systeem en, met name, naar de kritieke delen ervan. <\/p>\n<p>Oorspronkelijk werd de seL4 microkernelsysteem geverifieerd voor 32-bits ARM-processoren en later voor 64-bits x86-processoren. Het wordt opgemerkt dat de combinatie van de open hardwarearchitectuur RISC-V met de open seL4 microkernel een nieuw niveau van veiligheid zal bereiken, aangezien de hardwarecomponenten in de toekomst ook volledig kunnen worden geverifieerd, wat niet mogelijk is met propri\u00ebtaire hardwarearchitecturen. <\/p>\n<p>Bij de verificatie van seL4 wordt aangenomen dat de hardware functioneert zoals opgegeven en dat de specificatie het gedrag van het systeem volledig beschrijft, maar in werkelijkheid is de hardware niet vrij van fouten, wat goed ge\u00efllustreerd wordt door regelmatig opduikende problemen in het mechanisme voor speculatieve uitvoering van instructies. Open hardwareplatforms vergemakkelijken de integratie van beveiligingsgerelateerde wijzigingen \u2013 bijvoorbeeld om alle mogelijke lekkanalen via zijwegen te blokkeren, waarbij het veel effectiever is om het probleem op hardware-niveau op te lossen dan te proberen softwarematig een omweg te vinden.<\/p>\n<p>Ter herinnering, de architectuur van seL4 <noindex><a rel=\"nofollow\" href=\"http:\/\/sel4.systems\/FAQ\/\">is opmerkelijk<\/a><\/noindex> de onderdelen voor het beheer van de kernresources naar de gebruikersruimte te verplaatsen en dezelfde toegangsbeheermethoden voor deze resources toe te passen als voor gebruikersresources. Het microkern biedt geen kant-en-klare high-level abstraheringen voor het beheer van bestanden, processen, netwerkverbindingen, enzovoort; in plaats daarvan biedt het alleen minimale mechanismen voor toegang tot de fysieke adresruimte, onderbrekingen en CPU-resources. High-level abstraheringen en drivers voor interactie met hardware worden separaat bovenop het microkern ge\u00efmplementeerd in de vorm van taken die op gebruikersniveau worden uitgevoerd. De toegang van deze taken tot de resources van het microkern wordt georganiseerd via het defini\u00ebren van regels.<\/p>\n<p>RISC-V biedt een open en flexibele set van machine-instructies die het mogelijk maakt om microprocessors te cre\u00ebren voor verschillende toepassingsgebieden, zonder royalties te vereisen en zonder voorwaarden voor gebruik. RISC-V maakt het mogelijk om volledig open SoC's en processors te ontwikkelen. Momenteel zijn er op basis van de RISC-V specificatie verschillende bedrijven en gemeenschappen bezig met de ontwikkeling van meerdere open licenties (BSD, MIT, Apache 2.0). <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/risc-v-cores\/\">een vrij alternatief voor XenServer wordt ontwikkeld, waarin functies zijn teruggebracht die uit de gratis versie van XenServer zijn verwijderd.<\/a><\/noindex> een paar tientallen varianten van microprocessor-kernen, SoC's en al geproduceerde chips. Ondersteuning voor RISC-V is aanwezig sinds de release van Glibc 2.27, binutils 2.30, gcc 7 en de Linux-kern 4.15.<\/p>\n<p><noindex><a rel=\"nofollow\" name=\"link\"><\/a><\/noindex><\/p>\n<p>Bron: <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\/nl\/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=\"nl_NL\" \/>\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\/nl\/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\udd47Microkern seL4 wiskundig geverifieerd voor de RISC-V architectuur | ProHoster","description":"De organisatie RISC-V Foundation heeft de verificatie van het functioneren van het microkern aangekondigd.","canonical_url":"https:\/\/prohoster.info\/nl\/blog\/news\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"nl_NL","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\/nl\/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\/nl\/wp-json\/wp\/v2\/posts\/84726","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/comments?post=84726"}],"version-history":[{"count":0,"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/posts\/84726\/revisions"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/media?parent=84726"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/categories?post=84726"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/nl\/wp-json\/wp\/v2\/tags?post=84726"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}