Arbejdet med den matematiske formelle verifikation af pålidelighed og sikkerhed i mikrokerne seL4 på systemer med AArch64 instruktionssætarkitektur er afsluttet. Verifikationen indebærer et matematiske bevis for seL4's korrekthed, hvilket beviser, at den fuldt ud overholder de angivne specifikationer på et formelt sprog. Beviset for pålidelighed muliggør brugen af seL4 i kritiske systemer baseret på ARM64-processorer, der kræver et højt sikkerhedsniveau og garanterer fravær af fejl.
Mikrokerne seL4 blev oprindeligt verificeret for 32-bit ARM-processorer og senere for 64-bit x86 og RISC-V-processorer. Verifikationen sikrer, at hvis der opstår en fejl i en del af systemet, vil denne fejl ikke sprede sig til resten af systemet og dens kritiske dele. I forbindelse med sikkerhed bekræfter verifikationen, at kernen sikrer det rette niveau af isolation for applikationer, forhindrer dem i at få adgang til information uden autorisation og garanterer, at i tilfælde af kompromittering af sekundære applikationer, vil angrebet ikke sprede sig til kritisk vigtige applikationer.
Mikro-arkitekturen seL4 er bemærkelsesværdig for at flytte dele til kernekontrol af ressourcer til brugerens rum og anvende de samme adgangsgrænsningsmetoder til sådanne ressourcer som til brugerressourcer. Mikro-kernen tilbyder ikke foruddefinerede høj-niveau abstraktioner til håndtering af filer, processer, netværksforbindelser osv.; i stedet giver den kun minimale mekanismer til at styre adgangen til fysisk adresseområde, afbrydelser og processoressourcer. Høj-niveau abstraktioner og drivere til interaktion med hardware implementeres separat oven på mikro-kernen som opgaver, der kører på bruger-niveau. Adgangen for disse opgaver til de ressourcer, mikro-kernen råder over, organiseres gennem definering af regler.
Kilde: opennet.ru
