{"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\/it\/blog\/novosti-interneta\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","title":{"rendered":"Il microkernel seL4 \u00e8 matematicamente verificato per l'architettura RISC-V","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"<p>Organizzazione RISC-V Foundation <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-is-verified-on-risc-v\/\">ha annunciato<\/a><\/noindex> sulla verifica del funzionamento del microkernel <noindex><a rel=\"nofollow\" href=\"https:\/\/github.com\/seL4\/seL4\">seL4<\/a><\/noindex>  su sistemi con architettura del set di istruzioni RISC-V. La verifica consiste in <noindex><a rel=\"nofollow\" href=\"https:\/\/www.opennet.ru\/opennews\/art.shtml?num=23011\">una dimostrazione matematica<\/a><\/noindex> dell'affidabilit\u00e0 di seL4, che attesta la piena conformit\u00e0 alle specifiche formalmente definite. La dimostrazione dell'affidabilit\u00e0 <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/2020\/06\/sel4-operating-system-protects-critical-systems-on-risc-v-architecture-from-cyber-attacks\/\">permette di utilizzare<\/a><\/noindex> seL4 in sistemi critici basati su processori RISC-V RV64, che richiedono un elevato livello di affidabilit\u00e0 e garantiscono l'assenza di guasti. Gli sviluppatori di software che operano sopra il kernel seL4 possono essere completamente certi che, in caso di guasto in una parte del sistema, tale guasto non si propagher\u00e0 al resto del sistema e, in particolare, alle sue parti critiche. <\/p>\n<p>Originariamente, il microkernel seL4 \u00e8 stato verificato per processori ARM a 32 bit, e successivamente per processori x86 a 64 bit. Si osserva che la combinazione dell'architettura hardware open source RISC-V con il microkernel open source seL4 consentir\u00e0 di raggiungere un nuovo livello di sicurezza, poich\u00e9 i componenti hardware potrebbero anche essere completamente verificati, cosa non ottenibile con architetture hardware proprietarie. <\/p>\n<p>Nella verifica di seL4 si presume che l'hardware funzioni come dichiarato e che la specifica descriva completamente il comportamento del sistema, ma in realt\u00e0 l'hardware non \u00e8 esente da errori, come dimostrano regolarmente i problemi emersi nel meccanismo di esecuzione speculativa delle istruzioni. Le piattaforme hardware aperte semplificano l'integrazione delle modifiche relative alla sicurezza \u2014 ad esempio, per bloccare tutti i possibili canali di fuga attraverso canali esterni, dove \u00e8 molto pi\u00f9 efficace risolvere il problema a livello hardware piuttosto che cercare soluzioni a livello software.<\/p>\n<p>Ricordiamo che l'architettura seL4 <noindex><a rel=\"nofollow\" href=\"http:\/\/sel4.systems\/FAQ\/\">si distingue per<\/a><\/noindex> con estrazione di parti per la gestione delle risorse del kernel nello spazio utente e utilizzo per tali risorse degli stessi strumenti di accesso controllato come per le risorse utente. Il microkernel non fornisce astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; invece, offre solo meccanismi minimi per la gestione dell'accesso allo spazio indirizzi fisico, alle interruzioni e alle risorse della CPU. Le astrazioni di alto livello e i driver per l'interazione con l'hardware vengono implementati separatamente sopra il microkernel sotto forma di task eseguiti a livello utente. L'accesso di tali task alle risorse disponibili del microkernel \u00e8 organizzato attraverso la definizione di regole.<\/p>\n<p>RISC-V offre un'architettura aperta e flessibile per set di istruzioni, consentendo la creazione di microprocessori per applicazioni diverse senza costi di licenza n\u00e9 condizioni restrittive sull'uso. RISC-V permette lo sviluppo di SoC e processori completamente aperti. Attualmente, sulla base della specifica RISC-V, diverse aziende e comunit\u00e0 stanno lavorando a chip gi\u00e0 prodotti con diverse licenze aperte (BSD, MIT, Apache 2.0). <noindex><a rel=\"nofollow\" href=\"https:\/\/riscv.org\/risc-v-cores\/\">si sviluppa<\/a><\/noindex> un'ampia gamma di core di microprocessori, SoC e chip gi\u00e0 in produzione. Il supporto per RISC-V \u00e8 disponibile a partire dalle versioni di Glibc 2.27, binutils 2.30, gcc 7 e del kernel 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-novosti-interneta"],"aioseo_notices":[],"aioseo_head":"\n\t\t<!-- All in One SEO 4.9.10 - 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 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\" \/>\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\/it\/blog\/novosti-interneta\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v\" \/>\n\t<meta name=\"generator\" content=\"All in One SEO (AIOSEO) 4.9.10\" \/>\n\t\t<meta property=\"og:locale\" content=\"it_IT\" \/>\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 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\" \/>\n\t\t<meta property=\"og:url\" content=\"https:\/\/prohoster.info\/it\/blog\/novosti-interneta\/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\udd47Il microkernel seL4 \u00e8 verificato matematicamente per l'architettura RISC-V | ProHoster","description":"L'organizzazione RISC-V Foundation ha annunciato la verifica del microkernel seL4 su sistemi basati sull'architettura del set di istruzioni RISC-V. La verifica consiste in una dimostrazione matematica della correttezza di seL4, che attesta la completa conformit\u00e0 alle specifiche definite in linguaggio formale. La prova di correttezza consente di utilizzare seL4 in sistemi critici basati su processori RISC-V RV64, che richiedono un elevato livello di affidabilit\u00e0 e garantiscono l'assenza di","canonical_url":"https:\/\/prohoster.info\/it\/blog\/novosti-interneta\/mikroyadro-sel4-matematicheski-verificzirovano-dlya-arhitektury-risc-v","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"it_IT","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 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","og:url":"https:\/\/prohoster.info\/it\/blog\/novosti-interneta\/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"},"gt_translate_keys":[{"key":"link","format":"url"}],"_links":{"self":[{"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/posts\/84726","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/comments?post=84726"}],"version-history":[{"count":0,"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/posts\/84726\/revisions"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/media?parent=84726"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/categories?post=84726"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/it\/wp-json\/wp\/v2\/tags?post=84726"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}