Završen je rad na formalnoj matematičkoj provjeri pouzdanosti i sigurnosti mikrojezgre seL4 na sustavima s arhitekturom skupa instrukcija AArch64. Provjera se sastoji od matematičkog dokaza ispravnosti rada seL4, koji pokazuje potpunu usklađenost sa specifikacijama definiranim u formalnom jeziku. Ovaj dokaz pouzdanosti omogućuje korištenje seL4 u kritičnim sustavima temeljenim na ARM64 procesorima koji zahtijevaju visoku razinu sigurnosti i jamče odsutnost kvarova.
Mikrojezgra seL4 u početku je verificirana za 32-bitne ARM procesore, a kasnije za 64-bitne x86 i RISC-V procesore. Verifikacija osigurava da se kvar, ako se dogodi u jednom dijelu sustava, neće proširiti na ostatak sustava i njegove kritične komponente. U kontekstu sigurnosti, verifikacija potvrđuje da jezgra pruža odgovarajuću razinu izolacije aplikacija, sprječava im pristup informacijama bez autorizacije i osigurava da se napad, ako su sekundarne aplikacije kompromitirane, neće proširiti na kritične aplikacije.
Arhitektura mikrojezgre seL4 značajna je po uklanjanju dijelova za upravljanje resursima jezgre u korisničkom prostoru i po primjeni istih načina kontrole pristupa za takve resurse kao i za korisničke resurse. Mikrokernel ne pruža gotove apstrakcije visoke razine za upravljanje datotekama, procesima, mrežnim vezama i slično, umjesto toga pruža samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekidima i resursima procesora. Apstrakcije visoke razine i upravljački programi za interakciju s hardverom implementirani su zasebno na vrhu mikrojezgre u obliku zadataka na razini korisnika. Pristup takvih zadataka resursima dostupnim mikrojezgri organiziran je kroz definiranje pravila.
Izvor: opennet.ru
