Práca na formálnom matematickom overení spoľahlivosti a bezpečnosti mikrojadra seL4 na systémoch s architektúrou inštrukčnej sady AArch64 bola dokončená. Overenie pozostáva z matematického dôkazu správnosti fungovania seL4, ktorý preukazuje plný súlad so špecifikáciami definovanými vo formálnom jazyku. Tento dôkaz spoľahlivosti umožňuje použitie seL4 v kritických systémoch založených na procesoroch ARM64, ktoré vyžadujú vysokú úroveň bezpečnosti a zaručujú absenciu porúch.
Mikrojadro seL4 bolo pôvodne overené pre 32-bitové procesory ARM a neskôr pre 64-bitové procesory x86 a RISC-V. Overenie zabezpečuje, že ak dôjde k zlyhaniu v jednej časti systému, nerozšíri sa do zvyšku systému a jeho kritických komponentov. V kontexte bezpečnosti overenie potvrdzuje, že jadro poskytuje primeranú úroveň izolácie aplikácií, bráni im v prístupe k informáciám bez autorizácie a zabezpečuje, že ak dôjde k napadnutiu sekundárnych aplikácií, útok sa nerozšíri na kritické aplikácie.
Architektúra mikrojadra seL4 sa vyznačuje presúvaním častí na správu zdrojov jadra do užívateľského priestoru a využívaním rovnakých nástrojov na riadenie prístupu k takýmto zdrojom ako k užívateľským zdrojom. Mikrokernel neposkytuje hotové abstrakcie na vysokej úrovni pre správu súborov, procesov, sieťových pripojení a podobne, namiesto toho poskytuje len minimálne mechanizmy na riadenie prístupu k fyzickému adresnému priestoru, prerušeniam a zdrojom procesora. Vysokoúrovňové abstrakcie a ovládače pre interakciu s hardvérom sú implementované oddelene na vrchole mikrojadra vo forme úloh na užívateľskej úrovni. Prístup takýchto úloh k zdrojom dostupným pre mikrokernel je organizovaný prostredníctvom definície pravidiel.
Zdroj: opennet.ru
