Arbeidet med den formelle matematiske verifiseringen av pÄliteligheten og sikkerheten til seL4-mikrokjernen pÄ systemer med AArch64-instruksjonssettarkitekturen er fullfÞrt. Verifiseringen bestÄr av et matematisk bevis pÄ korrektheten til seL4-operasjonen, som viser full samsvar med spesifikasjonene definert i det formelle sprÄket. Dette beviset pÄ pÄlitelighet muliggjÞr bruk av seL4 i virksomhetskritiske systemer basert pÄ ARM64-prosessorer som krever et hÞyt sikkerhetsnivÄ og garanterer fravÊr av feil.
seL4-mikrokjernen ble opprinnelig verifisert for 32-bits ARM-prosessorer, og senere for 64-bits x86- og RISC-V-prosessorer. Verifisering sikrer at hvis en feil oppstÄr i en del av systemet, vil den ikke spre seg til resten av systemet og dets kritiske komponenter. I sikkerhetssammenheng bekrefter verifisering at kjernen gir riktig nivÄ av applikasjonsisolering, forhindrer dem i Ä fÄ tilgang til informasjon uten autorisasjon, og sikrer at hvis sekundÊre applikasjoner blir kompromittert, vil angrepet ikke spre seg til kritiske applikasjoner.
Arkitekturen til seL4 mikrokjernen er kjent for fjerning av deler for Ä administrere kjerneressurser i brukerrommet og for Ä bruke de samme midlene for tilgangskontroll for slike ressurser som for brukerressurser. Mikrokjernen gir ikke ut-av-boksen hÞynivÄabstraksjoner for Ä administrere filer, prosesser, nettverkstilkoblinger og lignende, i stedet gir den bare minimale mekanismer for Ä kontrollere tilgang til det fysiske adresserommet, avbrudd og prosessorressurser. Abstraksjoner pÄ hÞyt nivÄ og drivere for samhandling med maskinvare implementeres separat pÄ toppen av mikrokjernen i form av oppgaver pÄ brukernivÄ. Tilgangen til slike oppgaver til ressursene som er tilgjengelige for mikrokjernen er organisert gjennom definisjonen av regler.
Kilde: opennet.ru
