Bol vykonaný formálny overovací test bezpečnosti mikrojadra seL4 pre architektúru AArch64

Dokončili sme prácu na matematickej formálnej verifikácii spoľahlivosti a bezpečnosti mikrojadra seL4 na systémoch s architektúrou inštrukčného súboru AArch64. Verifikácia spočíva v matematickom dôkaze správnosti fungovania seL4, ktorý potvrdzuje úplnú zhodu s predpísanými špecifikáciami v formálnom jazyku. Dôkaz spoľahlivosti umožňuje používanie seL4 v kritických systémoch založených na procesoroch ARM64, ktoré vyžadujú zvýšenú úroveň bezpečnosti a zaručujú neprítomnosť porúch.

Pôvodne bolo mikrojadro seL4 overené pre 32-bitové procesory ARM a neskôr pre 64-bitové procesory x86 a RISC-V. Verifikácia zaručuje, že v prípade poruchy v jednej časti systému sa táto porucha nepresunie na zvyšok systému a jeho kritické časti. V kontexte zabezpečenia verifikácia potvrdzuje, že jadro zabezpečuje primeranú úroveň izolácie aplikácií, neumožňuje im prístup k informáciám bez autorizácie a zaručuje, že v prípade kompromitácie sekundárnych aplikácií sa útok nepresunie na kriticky dôležité aplikácie.

Architektúra mikrojadra seL4 sa vyznačuje presunom častí na správu zdrojov jadra do priestoru používateľa a využívaním pre tieto zdroje rovnakých prístupových mechanizmov ako pre používateľské zdroje. Mikrojadro neposkytuje hotové vysokúrovňové abstrakcie pre správu súborov, procesov, sieťových pripojení a pod., namiesto toho poskytuje iba minimálne mechanizmy pre správu prístupu k fyzikálnemu adresnému priestoru, prerušenia a procecorových zdrojov. Vysokúrovňové abstrakcie a ovládače na interakciu s hardvérom sú implementované samostatne nad mikrojadrom vo forme úloh, ktoré sa vykonávajú na používateľskej úrovni. Prístup týchto úloh k zdrojom mikrojadra je organizovaný prostredníctvom definície pravidiel.

Zdroj: opennet.ru