{"id":183094,"date":"2026-08-25T04:53:36","date_gmt":"2026-08-25T02:53:36","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/vypolnena-formalnaya-verifikacziya-bezopasnosti-mikroyadra-sel4-dlya-arhitektury-aarch64"},"modified":"2026-08-25T04:53:42","modified_gmt":"2026-08-25T02:53:42","slug":"formal-security-verification-completed-for-the-sel4-microkernel-on-aarch64","status":"publish","type":"post","link":"https:\/\/prohoster.info\/hr\/blog\/news\/formal-security-verification-completed-for-the-sel4-microkernel-on-aarch64","title":{"rendered":"Provedena formalna verifikacija sigurnosti mikrojezgre seL4 za arhitekturu AArch64","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"

Zavr\u0161ena je analiza matemati\u010dke formalne verifikacije pouzdanosti i sigurnosti rada mikrojezgara seL4 na sustavima s arhitekturom skupa naredbi AArch64. Verifikacija se svodi na matemati\u010dko dokazivanje ispravnosti rada seL4, \u0161to potvr\u0111uje potpuno uskla\u0111ivanje sa specifikacijama zadanih na formalnom jeziku. Dokazivanje pouzdanosti omogu\u0107uje upotrebu seL4 u kriti\u010dnim sustavima temeljenim na ARM64 procesorima, koji zahtijevaju povi\u0161eni nivo sigurnosti i jam\u010de odsutnost kvarova. <\/p>\n

Izvorno je mikrojezgara seL4 verifikovana za 32-bitne ARM procesore, a kasnije za 64-bitne procesore x86 i RISC-V. Verifikacija jam\u010di da u slu\u010daju kvara u jednom dijelu sustava, taj kvar se ne\u0107e pro\u0161iriti na ostatak sustava i njegove kriti\u010dne dijelove. U kontekstu osiguranja sigurnosti, verifikacija potvr\u0111uje da jezgro osigurava odgovaraju\u0107i nivo izolacije aplikacija, ne dozvoljavaju\u0107i im pristup informacijama bez autorizacije, te jam\u010di da, u slu\u010daju kompromitacije sekundarnih aplikacija, napad se ne\u0107e pro\u0161iriti na kriti\u010dne va\u017ene aplikacije. <\/p>\n

Arhitektura mikrojezgara seL4 odlikuje se izdvojenim dijelovima za upravljanje resursima jezgra u korisni\u010dki prostor i primjenom istih sredstava za razdvajanje pristupa kao za korisni\u010dke resurse. Mikrojezgara ne pru\u017ea gotove visoke apstrakcije za upravljanje datotekama, procesima, mre\u017enim vezama itd., ve\u0107 pru\u017ea samo minimalne mehanizme za upravljanje pristupom fizi\u010dkom adresnom prostoru, prekidima i resursima procesora. Visoke apstrakcije i drajveri za interakciju s hardverom ostvaruju se odvojeno iznad mikrojezgara u obliku zadataka koji se izvode na korisni\u010dkoj razini. Pristup takvih zadataka resursima mikrojezgara organizira se putem definiranja pravila.
\n
Izvor: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"

\u0417\u0430\u0432\u0435\u0440\u0448\u0435\u043d\u0430 \u0440\u0430\u0431\u043e\u0442\u0430 \u043d\u0430\u0434 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439 \u043d\u0430\u0434\u0451\u0436\u043d\u043e\u0441\u0442\u0438 \u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\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 AArch64. \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 \u043a\u043e\u0440\u0440\u0435\u043a\u0442\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 ARM64, \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 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u0438 […]<\/p>\n","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"author":10,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[702],"tags":[],"class_list":["post-183094","post","type-post","status-publish","format-standard","hentry","category-news"],"aioseo_notices":[],"aioseo_head":"\n\t\t\n\t\n\t\n\t\n\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\t\t\n\n","aioseo_head_json":{"title":"\ud83e\udd47U\u010dinjena je formalna verifikacija sigurnosti mikrojezgara seL4 za arhitekturu AArch64 | ProHoster","description":"Zavr\u0161ena je analiza matemati\u010dke formalne verifikacije pouzdanosti i sigurnosti rada mikrojezgara seL4 na sustavima s arhitekturom skupa naredbi AArch64.","canonical_url":"https:\/\/prohoster.info\/hr\/blog\/news\/formal-security-verification-completed-for-the-sel4-microkernel-on-aarch64","robots":"max-image-preview:large","keywords":"","webmasterTools":{"miscellaneous":""},"schema":null,"og:locale":"hr_HR","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\u0412\u044b\u043f\u043e\u043b\u043d\u0435\u043d\u0430 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u0430\u044f \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u044f \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\u0438 \u043c\u0438\u043a\u0440\u043e\u044f\u0434\u0440\u0430 seL4 \u0434\u043b\u044f \u0430\u0440\u0445\u0438\u0442\u0435\u043a\u0442\u0443\u0440\u044b AArch64 | ProHoster","og:description":"\u0417\u0430\u0432\u0435\u0440\u0448\u0435\u043d\u0430 \u0440\u0430\u0431\u043e\u0442\u0430 \u043d\u0430\u0434 \u043c\u0430\u0442\u0435\u043c\u0430\u0442\u0438\u0447\u0435\u0441\u043a\u043e\u0439 \u0444\u043e\u0440\u043c\u0430\u043b\u044c\u043d\u043e\u0439 \u0432\u0435\u0440\u0438\u0444\u0438\u043a\u0430\u0446\u0438\u0435\u0439 \u043d\u0430\u0434\u0451\u0436\u043d\u043e\u0441\u0442\u0438 \u0438 \u0431\u0435\u0437\u043e\u043f\u0430\u0441\u043d\u043e\u0441\u0442\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 AArch64.","og:url":"https:\/\/prohoster.info\/hr\/blog\/news\/formal-security-verification-completed-for-the-sel4-microkernel-on-aarch64","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":"2026-08-25T02:53:36+00:00","article:modified_time":"2026-08-25T02:53:42+00:00","article:publisher":"https:\/\/www.facebook.com\/prohoster"},"aioseo_meta_data":{"post_id":"183094","title":null,"description":null,"keywords":null,"keyphrases":{"focus":[],"additional":[]},"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":"default","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":"2026-08-26 09:14:56","updated":"2026-08-26 09:14:56","focus_keyword":null,"additional_keywords":null,"truseo_locale":null},"gt_translate_keys":[{"key":"link","format":"url"}],"_links":{"self":[{"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/posts\/183094","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/users\/10"}],"replies":[{"embeddable":true,"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/comments?post=183094"}],"version-history":[{"count":1,"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/posts\/183094\/revisions"}],"predecessor-version":[{"id":183095,"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/posts\/183094\/revisions\/183095"}],"wp:attachment":[{"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/media?parent=183094"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/categories?post=183094"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/prohoster.info\/hr\/wp-json\/wp\/v2\/tags?post=183094"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}