Arbetet med den formella matematiska verifieringen av tillförlitligheten och säkerheten för seL4-mikrokärnan på system med instruktionsuppsättningsarkitekturen AArch64 har slutförts. Verifieringen består av ett matematiskt bevis på att seL4 fungerar korrekt, vilket visar fullständig överensstämmelse med specifikationerna som definieras i det formella språket. Detta bevis på tillförlitlighet möjliggör användning av seL4 i verksamhetskritiska system baserade på ARM64-processorer som kräver en hög säkerhetsnivå och garanterar frånvaro av fel.
Mikrokärnan seL4 verifierades initialt för 32-bitars ARM-processorer och senare för 64-bitars x86- och RISC-V-processorer. Verifiering säkerställer att om ett fel uppstår i en del av systemet, kommer det inte att sprida sig till resten av systemet och dess kritiska komponenter. I säkerhetssammanhang bekräftar verifiering att kärnan tillhandahåller lämplig nivå av applikationsisolering, förhindrar dem från att komma åt information utan auktorisering och säkerställer att om sekundära applikationer komprometteras, kommer attacken inte att sprida sig till kritiska applikationer.
seL4-mikrokärnans arkitektur är anmärkningsvärd för att den har tagit bort delar för att hantera kärnresurser in i användarutrymmet och för att den använder samma metoder för åtkomstkontroll för sådana resurser som för användarresurser. Mikrokärnan tillhandahåller inte färdiga abstraktioner på hög nivå för att hantera filer, processer, nätverksanslutningar etc., utan tillhandahåller endast minimala mekanismer för att hantera åtkomst till det fysiska adressutrymmet, avbrott och processorresurser. Abstraktioner på hög nivå och drivrutiner för att interagera med hårdvaran implementeras separat ovanpå mikrokärnan i form av uppgifter som utförs på användarnivå. Åtkomst för sådana uppgifter till de resurser som är tillgängliga för mikrokärnan organiseras genom att definiera regler.
Källa: opennet.ru
