Provedena formalna verifikacija sigurnosti mikrojezgre seL4 za arhitekturu AArch64

Završena je analiza matematičke formalne verifikacije pouzdanosti i sigurnosti rada mikrojezgara seL4 na sustavima s arhitekturom skupa naredbi AArch64. Verifikacija se svodi na matematičko dokazivanje ispravnosti rada seL4, što potvrđuje potpuno usklađivanje sa specifikacijama zadanih na formalnom jeziku. Dokazivanje pouzdanosti omogućuje upotrebu seL4 u kritičnim sustavima temeljenim na ARM64 procesorima, koji zahtijevaju povišeni nivo sigurnosti i jamče odsutnost kvarova.

Izvorno je mikrojezgara seL4 verifikovana za 32-bitne ARM procesore, a kasnije za 64-bitne procesore x86 i RISC-V. Verifikacija jamči da u slučaju kvara u jednom dijelu sustava, taj kvar se neće proširiti na ostatak sustava i njegove kritične dijelove. U kontekstu osiguranja sigurnosti, verifikacija potvrđuje da jezgro osigurava odgovarajući nivo izolacije aplikacija, ne dozvoljavajući im pristup informacijama bez autorizacije, te jamči da, u slučaju kompromitacije sekundarnih aplikacija, napad se neće proširiti na kritične važne aplikacije.

Arhitektura mikrojezgara seL4 odlikuje se izdvojenim dijelovima za upravljanje resursima jezgra u korisnički prostor i primjenom istih sredstava za razdvajanje pristupa kao za korisničke resurse. Mikrojezgara ne pruža gotove visoke apstrakcije za upravljanje datotekama, procesima, mrežnim vezama itd., već pruža samo minimalne mehanizme za upravljanje pristupom fizičkom 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čkoj razini. Pristup takvih zadataka resursima mikrojezgara organizira se putem definiranja pravila.

Izvor: opennet.ru