RISC-V Foundation kunngjorde at de har verifisert funksjonaliteten til seL4-mikrokjernen på systemer med RISC-V instruksjonssettarkitektur . Verifiseringsprosessen er redusert til et matematisk bevis på seL4s pålitelighet, noe som indikerer full samsvar med spesifikasjonene definert i et formelt språk.
Pålitelighetstesten tillater bruk av seL4 i virksomhetskritiske systemer basert på RV64 RISC-V-prosessorer , som krever et høyere nivå av pålitelighet og ikke garanterer feil.
Programvareutviklere som kjører på toppen av seL4-kjernen, kan være helt sikre på at i tilfelle en feil i en del av systemet, vil denne feilen ikke spre seg til resten av systemet og spesielt til de kritiske delene.
Om seL4
seL4-arkitekturen er kjent for å fjerne deler for å administrere kjerneressurser fra brukerområdet og bruke de samme tilgangskontrollmetodene for slike ressurser som for brukerressurser.
Mikrokjernen tilbyr ikke ferdige abstraksjoner på høyt nivå for å administrere filer, prosesser, nettverkstilkoblinger osv., men gir bare minimale mekanismer for å kontrollere tilgang til det fysiske adresserommet , avbrudd og prosessorressurser.
Abstraksjoner på høyt nivå og drivere for samhandling med datamaskinen implementeres separat på toppen av mikrokjernen i form av oppgaver som utføres på brukernivå.
Tilgangen til slike oppgaver til ressursene som er tilgjengelige i mikrokjernen er organisert gjennom definisjon av regler.
RISC-V tilbyr et åpent og fleksibelt maskininstruksjonssystem som tillater opprettelse av mikroprosessorer for vilkårlige applikasjoner, uten å kreve fradrag og uten å pålegge bruksbetingelser.
RISC-V lar deg lage helt åpne prosessorer og SoC-er. For øyeblikket, på grunnlag av RISC-V-spesifikasjonen, utvikler flere selskaper og lokalsamfunn under forskjellige gratis lisenser (BSD, MIT, Apache 2.0) flere titalls varianter av allerede produserte mikroprosessorkjerner, SoC og chips.
RISC-V-støtte har eksistert siden utgivelsen av Glibc 2.27, binutils 2.30, gcc 7 og Linux 4.15-kjernen.
Om seL4 mikrokernel testing
Opprinnelig ble seL4-mikrokjernen verifisert for 32-bits ARM-prosessorer , og senere for 64-bits x86-prosessorer.
Det observeres at kombinasjonen av den åpne RISC-V-maskinvarearkitekturen med den åpne seL4-mikrokjernen vil oppnå et nytt sikkerhetsnivå , siden maskinvarekomponenter i fremtiden også kan verifiseres fullt ut, noe som er umulig å oppnå for proprietære maskinvarearkitekturer.
Når vi sjekker seL4, må vi anta at maskinvaren fungerer som den skal (det vil si som spesifisert). Det antar at det er en entydig spesifikasjon i utgangspunktet, noe som ikke er tilfelle for all maskinvare.
Men selv når en slik spesifikasjon eksisterer, og den er formell (det vil si ritten i en matematisk formalisme som støtter matematisk resonnement om dens egenskaper), hvordan vet vi at den faktisk fanger oppførselen til maskinvaren?
Virkeligheten er at vi kan være ganske sikre på at det ikke er det. Maskinvare er ikke forskjellig fra programvare ved at begge er buggy.
Men å ha en åpen ISA har fordeler som går utover å være royaltyfri. Den ene er at den tillater implementering av maskinvare med åpen kildekode.
Når du sjekker seL4 antas det at utstyret fungerer som angitt, og spesifikasjonen beskriver systemets oppførsel, men faktisk er utstyret ikke feilfritt, noe som godt demonstreres av problemer som regelmessig oppstår i den spekulative kjøremekanismen .
Åpne maskinvareplattformer forenkler integreringen av sikkerhetsrelaterte endringer, for eksempel for å blokkere alle mulige lekkasjekanaler gjennom tredjepartskanaler, der det er mye mer effektivt å bli kvitt et problem med maskinvare enn å prøve å finne løsninger med programvare.
Til slutt, hvis du vil vite mer om det, kan du lese artikkelen på følgende lenke.