Dokončano je delo na matematični formalni verifikaciji zanesljivosti in varnosti delovanja mikrojedra seL4 na sistemih z arhitekturo nabora ukazov AArch64. Verifikacija se zmanjšuje na matematični dokaz pravilnosti delovanja seL4, kar pomeni popolno skladnost s specifikacijami, določenimi v formalnem jeziku. Dokaz zanesljivosti omogoča uporabo seL4 v kritičnih sistemih, ki temeljijo na ARM64 procesorjih, ki zahtevajo višjo raven varnosti ter zagotavljajo odsotnost napak.
Sprva je bilo mikrojedro seL4 verificirano za 32-bitne ARM procesorje, nato pa za 64-bitne x86 in RISC-V procesorje. Verifikacija zagotavlja, da v primeru napake v enem delu sistema ta napaka ne bo vplivala na preostali sistem in njegove kritične dele. V kontekstu zagotavljanja varnosti verifikacija potrjuje, da jedro zagotavlja ustrezen nivo izolacije aplikacij, ne dovoljuje jim dostopa do informacij brez avtorizacije in zagotavlja, da v primeru kompromitacije sekundarnih aplikacij napad ne bo prešel na kritične pomembne aplikacije.
Arhitektura mikrojedra seL4 se odlikuje po tem, da delčke za upravljanje virov jedra prenaša v uporabniški prostor in uporablja za te vire iste metode za nadzor dostopa, kot za uporabniške vire. Mikrojedro ne ponuja pripravljene visoko nivojske abstrakcije za upravljanje datotek, procesov, omrežnih povezav itd., temveč zagotavlja le minimalne mehanizme za upravljanje dostopa do fizičnega naslovnega prostora, prekinitev in virov procesorja. Visoko nivojske abstrakcije in gonilniki za interakcijo s strojno opremo se izvajajo ločeno nad mikrojedrom v obliki nalog, ki se izvajajo na uporabniški ravni. Dostop teh nalog do virov mikrojedra je organiziran z določanjem pravil.
Izvor: opennet.ru
