Formell sikkerhetsverifikasjon av mikro-kjernen seL4 for AArch64-arkitekturen er fullført.

Arbeidet med matematisk formell verifikasjon av påliteligheten og sikkerheten til mikro-kjernen seL4 på systemer med AArch64 instruksjonssettarkitektur er avsluttet. Verifikasjonen reduseres til et matematisk bevis på korrektheten av seL4, som bekrefter fullstendig overensstemmelse med spesifikasjonene fastsatt på et formelt språk. Beviset på pålitelighet tillater bruk av seL4 i kritiske systemer basert på ARM64-prosessorer som krever et høyere sikkerhetsnivå og garanterer fravær av feil.

Mikro-kjernen seL4 ble opprinnelig verifisert for 32-bits ARM-prosessorer, og senere for 64-bits x86- og RISC-V-prosessorer. Verifikasjonen garanterer at dersom det oppstår en feil i en del av systemet, vil ikke denne feilen spre seg til resten av systemet og dets kritiske deler. I konteksten av sikkerhet bekrefter verifikasjonen at kjernen gir tilstrekkelig nivå av applikasjonsisolasjon, forhindrer dem i å få tilgang til informasjon uten autorisasjon, og garanterer at i tilfelle av kompromittering av sekundære applikasjoner, vil ikke angrepet spre seg til kritisk viktige applikasjoner.

Arkitekturen til mikrokjernen seL4 er bemerkelsesverdig for å ha flyttet deler av kjernens ressursstyring til brukerens rom, og anvendte de samme tilgangskontrollmidlene for disse ressursene som for brukerrressurser. Mikrokjernen gir ingen klare høynivå-abstraksjoner for håndtering av filer, prosesser, nettverksforbindelser osv.; den gir kun minimale mekanismer for å håndtere tilgang til fysisk adresseområde, avbrudd og prosessorressurser. Høynivå-abstraksjoner og drivere for å interagere med maskinvare implementeres separat over mikrokjernen i form av oppgaver som kjører på brukernivå. Tilgangen til mikrokjernens ressurser for slike oppgaver er organisert gjennom definerte regler.

Kilde: opennet.ru