Befejeződött a seL4 mikrokernel megbízhatóságának és biztonságának matematikai formális verifikációja az AArch64 parancsarchitektúrával rendelkező rendszereken. A verifikáció matematikai bizonyítást jelent a seL4 működésének helyességéről, amely teljes megfelelőséget tanúsít a formális nyelven írt specifikációknak. A megbízhatóság bizonyítása lehetővé teszi a seL4 használatát kritikus rendszerekben ARM64 processzorok alapján, amelyek magasabb biztonsági szintet igényelnek és garantálják a meghibásodások hiányát.
Kezdetben a seL4 mikrokernelt 32-bites ARM processzorokhoz verifikálták, később pedig 64-bites x86 és RISC-V processzorokhoz. A verifikáció garantálja, hogy ha a rendszer egy részén hiba lép fel, ez a hiba nem terjed át a rendszer más részeire és kritikus részeire. A biztonság érdekében a verifikáció megerősíti, hogy a mag megfelelő szintű elszigeteltséget biztosít az alkalmazások számára, nem engedi meg számukra, hogy jogosítvány nélküli információhoz férjenek hozzá, és garantálja, hogy ha a másodlagos alkalmazások kompromittálódnak, a támadás nem terjed át a kritikus fontosságú alkalmazásokra.
A seL4 mikrokernel architektúrája figyelemre méltó, mivel a kernel erőforrás-kezelő részeit a felhasználói térbe helyezi, és ugyanazokat a hozzáférés-vezérlési eszközöket alkalmazza e forrásokhoz, mint a felhasználói erőforrásokhoz. A mikrokernel nem nyújt készen álló, magas szintű absztrakciókat a fájlok, folyamatok, hálózati kapcsolatok stb. kezelésére, hanem csupán minimális mechanizmusokat biztosít a fizikai címzési térhez, megszakításokhoz és a CPU erőforrásokhoz való hozzáférés kezelésére. A magas szintű absztrakciók és az eszközökkel való interakcióra szolgáló driverek külön feladatok formájában valósulnak meg a mikrokernel felett, amelyek felhasználói szinten futnak. Az ilyen feladatok hozzáférését a mikrokernel erőforrásaihoz a szabályok meghatározása révén szervezik.
Forrás: opennet.ru
