Arbejdet med den formelle matematiske verifikation af pålideligheden og sikkerheden af seL4-mikrokernen på systemer med AArch64-instruktionssætarkitekturen er afsluttet. Verifikationen består af et matematisk bevis for korrektheden af seL4-driften, hvilket demonstrerer fuld overholdelse af de specifikationer, der er defineret i det formelle sprog. Dette bevis for pålidelighed muliggør brugen af seL4 i missionskritiske systemer baseret på ARM64-processorer, der kræver et højt sikkerhedsniveau og garanterer fraværet af fejl.
seL4-mikrokernen blev oprindeligt verificeret til 32-bit ARM-processorer og senere til 64-bit x86- og RISC-V-processorer. Verifikation sikrer, at hvis en fejl opstår i en del af systemet, spreder den sig ikke til resten af systemet og dets kritiske komponenter. I forbindelse med sikkerhed bekræfter verifikation, at kernen yder det passende niveau af applikationsisolering, forhindrer dem i at få adgang til information uden autorisation, og sikrer, at hvis sekundære applikationer kompromitteres, spreder angrebet sig ikke til kritiske applikationer.
seL4-mikrokernens arkitektur er bemærkelsesværdig ved dens fjernelse af dele til styring af kerneressourcer ind i brugerområdet og ved brugen af de samme midler til adgangskontrol for sådanne ressourcer som for brugerressourcer. Mikrokernen leverer ikke færdige abstraktioner på højt niveau til styring af filer, processer, netværksforbindelser osv., men i stedet kun minimale mekanismer til styring af adgang til det fysiske adresseområde, afbrydelser og processorressourcer. Abstraktioner på højt niveau og drivere til interaktion med hardwaren implementeres separat oven på mikrokernen i form af opgaver, der udføres på brugerniveau. Adgang for sådanne opgaver til de ressourcer, der er tilgængelige for mikrokernen, er organiseret ved at definere regler.
Kilde: opennet.ru
