Rad na formalnoj matematičkoj verifikaciji pouzdanosti i sigurnosti seL4 mikrokernela na sistemima sa arhitekturom skupa instrukcija AArch64 je završen. Verifikacija se sastoji od matematičkog dokaza ispravnosti rada seL4, koji demonstrira potpunu usklađenost sa specifikacijama definiranim u formalnom jeziku. Ovaj dokaz pouzdanosti omogućava upotrebu seL4 u kritičnim sistemima baziranim na ARM64 procesorima koji zahtijevaju visok nivo sigurnosti i garantuju odsustvo kvarova.
seL4 mikrokernel je prvobitno verifikovan za 32-bitne ARM procesore, a kasnije i za 64-bitne x86 i RISC-V procesore. Verifikacija osigurava da, ako se kvar dogodi u jednom dijelu sistema, on se neće proširiti na ostatak sistema i njegove kritične komponente. U kontekstu sigurnosti, verifikacija potvrđuje da kernel pruža odgovarajući nivo izolacije aplikacija, sprečava ih da pristupaju informacijama bez autorizacije i osigurava da, ako su sekundarne aplikacije kompromitovane, napad se neće proširiti na kritične aplikacije.
Arhitektura seL4 mikrokernela je istaknuta po pokretnim dijelovima za upravljanje resursima kernela u korisnički prostor i korištenju istih alata za kontrolu pristupa za takve resurse kao i za korisničke resurse. Mikrokernel ne pruža gotove apstrakcije visokog nivoa za upravljanje datotekama, procesima, mrežnim vezama i slično, već samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekidima i procesorskim resursima. Apstrakcije visokog nivoa i drajveri za interakciju sa hardverom implementirani su odvojeno na vrhu mikrokernela u obliku zadataka na nivou korisnika. Pristup takvih zadataka resursima dostupnim mikrokernelu je organizovan kroz definiciju pravila.
izvor: opennet.ru
