Práce na formálním matematickém ověření spolehlivosti a bezpečnosti mikrojádra seL4 na systémech s architekturou instrukční sady AArch64 byla dokončena. Ověření spočívá v matematickém důkazu správnosti fungování seL4, který prokazuje plnou shodu se specifikacemi definovanými ve formálním jazyce. Tento důkaz spolehlivosti umožňuje použití seL4 v kritických systémech založených na procesorech ARM64, které vyžadují vysokou úroveň zabezpečení a zaručují absenci poruch.
Mikrojádro seL4 bylo zpočátku ověřeno pro 32bitové procesory ARM a později pro 64bitové procesory x86 a RISC-V. Ověření zajišťuje, že pokud dojde k selhání v jedné části systému, nerozšíří se do zbytku systému a jeho kritických komponent. V kontextu bezpečnosti ověřování potvrzuje, že jádro poskytuje odpovídající úroveň izolace aplikací, brání jim v přístupu k informacím bez autorizace a zajišťuje, že v případě kompromitace sekundárních aplikací se útok nerozšíří na kritické aplikace.
Architektura mikrojádra seL4 se vyznačuje přesouváním částí pro správu zdrojů jádra do uživatelského prostoru a používáním stejných nástrojů pro řízení přístupu k takovým zdrojům jako k uživatelským zdrojům. Mikrokernel neposkytuje hotové abstrakce na vysoké úrovni pro správu souborů, procesů, síťových připojení a podobně, místo toho poskytuje pouze minimální mechanismy pro řízení přístupu k fyzickému adresnímu prostoru, přerušením a zdrojům procesoru. Vysokoúrovňové abstrakce a ovladače pro interakci s hardwarem jsou implementovány odděleně nad mikrokernelem ve formě úloh na uživatelské úrovni. Přístup těchto úkolů ke zdrojům, které má mikrojádro k dispozici, je organizován prostřednictvím definice pravidel.
Zdroj: opennet.ru
