RISC-V verifiserte seL4-mikrokjernen på deres RV64-prosessorer

RISC-V Foundation kunngjorde at den har bekreftet hvordan mikrokjernen fungerer seL4 i systemer med instruksjonssettarkitekturen RISC-V. Der bekreftelsesprosessen reduseres til det matematiske beviset for påliteligheten til seL4, som indikerer full samsvar med spesifikasjonene spesifisert på et formelt språk.

Pålitelighetstesting gjør at seL4 kan brukes i oppdragskritiske systemer basert på RISC-V-prosessorer RV64, som krever høyere 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 i brukerområdet og bruke de samme tilgangskontrollmetodene for slike ressurser som for brukerressurser.

Mikrokjernen gir ikke abstraksjoner på høyt nivå allerede forberedt på å administrere filer, prosesser, nettverkstilkoblinger osv., men i stedet gir bare minimale mekanismer for å kontrollere tilgangen til det fysiske adresseområdet, avbryter 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 gir et åpent og fleksibelt system av maskininstruksjoner som tillater å lage mikroprosessorer for vilkårlige applikasjoner, uten at det kreves fradrag og uten å pålegge bruksvilkår.

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 mikrokernel seL4 ble bekreftet for 32-biters ARM-prosessorer, Og senere for x86 64-biters prosessorer.

Det observeres at kombinasjonen av RISC-V åpen maskinvarearkitektur med den åpne mikrokjernen seL4 vil oppnå et nytt sikkerhetsnivå, da fremtidige maskinvarekomponenter 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 integrering av endringer relatert til sikkerhet, 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 se merknaden i følgende lenke.