Byla dokončena práce na matematické formální verifikaci spolehlivosti a bezpečnosti mikrojádra seL4 na systémech s architekturou příkazového systému AArch64. Verifikace se týká matematického důkazu správnosti fungování seL4, který potvrzuje plnou shodu se specifikacemi definovanými ve formálním jazyce. Důkaz spolehlivosti umožňuje použití seL4 v kritických systémech založených na procesorech ARM64, které vyžadují zvýšenou úroveň bezpečnosti a zajišťují absenci selhání.
Původně bylo mikrojádro seL4 verifikováno pro 32bitové procesory ARM a později pro 64bitové procesory x86 a RISC-V. Verifikace zaručuje, že v případě selhání v jedné části systému se toto selhání nešíří na zbývající systém a jeho kritické části. V kontextu zajištění bezpečnosti verifikace potvrzuje, že jádro poskytuje odpovídající úroveň izolace aplikací, nedovoluje jim přístup k informacím bez autorizace a zaručuje, že v případě kompromitace sekundárních aplikací se útok nešíří na kritické aplikace.
Architektura mikrojádra seL4 je pozoruhodná tím, že odděluje části pro správu prostředků jádra do prostoru uživatele a aplikuje na tyto prostředky stejná přístupová omezení jako na uživatelské prostředky. Mikrojádro neposkytuje hotové vysoceúrovňové abstrakce pro správu souborů, procesů, síťových připojení atd., místo toho poskytuje pouze minimální mechanismy pro správu přístupu k fyzickému adresnímu prostoru, přerušením a prostředkům procesoru. Vysoceúrovňové abstrakce a ovladače pro interakci s hardwarem jsou implementovány samostatně nad mikrojádrém ve formě úloh prováděných na uživatelské úrovni. Přístup těchto úloh k prostředkům, které má mikrojádro k dispozici, je organizován prostřednictvím stanovení pravidel.
Zdroj: opennet.ru
