RISC-V Foundation om å verifisere funksjonen til mikrokjernen på systemer med RISC-V instruksjonssettarkitektur. Verifikasjon kommer ned til påliteligheten til seL4-driften, som indikerer full overensstemmelse med spesifikasjonene spesifisert på det formelle språket. Bevis på pålitelighet seL4 i virksomhetskritiske systemer basert på RISC-V RV64-prosessorer som krever et økt nivå av pålitelighet og garanterer fravær av feil. Utviklere av programvare som kjører på toppen av seL4-kjernen kan være helt sikre på at hvis det er en feil i en del av systemet, vil denne feilen ikke spre seg til resten av systemet og spesielt dets kritiske deler.
seL4 mikrokjernen ble opprinnelig verifisert for 32-biters ARM-prosessorer, og senere for 64-biters x86-prosessorer. Det bemerkes at kombinasjonen av den åpne RISC-V maskinvarearkitekturen med den åpne seL4 mikrokjernen vil oppnå et nytt sikkerhetsnivå, siden maskinvarekomponentene også kan verifiseres fullt ut i fremtiden, noe som er umulig å oppnå for proprietære maskinvarearkitekturer.
Ved verifisering av seL4 antas det at utstyret fungerer som angitt og spesifikasjonen beskriver oppførselen til systemet fullt ut, men i virkeligheten er utstyret ikke fritt for feil, noe som tydelig demonstreres av regelmessig oppståtte problemer i mekanismen for spekulativ utførelse av bruksanvisning. Åpne maskinvareplattformer gjør det enklere å integrere sikkerhetsrelaterte endringer – for eksempel å blokkere alle mulige sidekanallekkasjer, hvor det er mye mer effektivt å bli kvitt problemet i maskinvare enn å prøve å finne løsninger i programvare.
Husk at seL4-arkitekturen bevegelige deler for å administrere kjerneressurser inn i brukerrom og bruke de samme tilgangskontrollmidlene for slike ressurser som for brukerressurser. Mikrokjernen gir ikke ferdige høynivåabstraksjoner for å administrere filer, prosesser, nettverkstilkoblinger og lignende; i stedet gir den bare minimale mekanismer for å kontrollere tilgang til fysisk adresserom, 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å. Tilgang for slike oppgaver til ressursene som er tilgjengelige for mikrokjernen er organisert gjennom definisjonen av regler.
RISC-V gir et åpent og fleksibelt maskininstruksjonssystem som lar mikroprosessorer bygges for vilkårlige applikasjoner uten å kreve royalties eller strenger knyttet til bruk. RISC-V lar deg lage helt åpne SoC-er og prosessorer. Foreløpig basert på RISC-V-spesifikasjonen fra forskjellige selskaper og samfunn under forskjellige gratis lisenser (BSD, MIT, Apache 2.0) flere dusin varianter av mikroprosessorkjerner, SoC-er og allerede produserte brikker. RISC-V-støtte har vært til stede siden utgivelsene av Glibc 2.27, binutils 2.30, gcc 7 og Linux-kjernen 4.15.
Kilde: opennet.ru