Google har kunngjort oppdagelsen av utviklingen relatert til KataOS-prosjektet, rettet mot å lage et sikkert operativsystem for innebygd maskinvare. KataOS-systemkomponenter er skrevet i Rust og kjøres på toppen av seL4 mikrokjernen, som det er gitt et matematisk bevis på pålitelighet for på RISC-V-systemer, noe som indikerer at koden fullt ut samsvarer med spesifikasjonene spesifisert i det formelle språket. Prosjektkoden er åpen under Apache 2.0-lisensen.
Systemet gir støtte for plattformer basert på RISC-V og ARM64 arkitekturer. For å simulere driften av seL4 og KataOS-miljøet på toppen av maskinvare, brukes Renode-rammeverket under utviklingsprosessen. Som en referanseimplementering foreslås Sparrow-programvare- og maskinvarekomplekset, som kombinerer KataOS med sikre brikker basert på OpenTitan-plattformen. Den foreslåtte løsningen lar deg kombinere en logisk verifisert operativsystemkjerne med pålitelige maskinvarekomponenter (RoT, Root of Trust), bygget ved hjelp av OpenTitan-plattformen og RISC-V-arkitekturen. I tillegg til KataOS-koden er det planlagt å åpne alle andre Sparrow-komponenter, inkludert maskinvarekomponenten, i fremtiden.
Plattformen utvikles med øye for applikasjon i spesialiserte brikker designet for å kjøre applikasjoner for maskinlæring og behandling av konfidensiell informasjon, som krever et spesielt nivå av beskyttelse og bekreftelse på fravær av feil. Eksempler på slike applikasjoner inkluderer systemer som manipulerer bilder av mennesker og stemmeopptak. KataOS sin bruk av pålitelighetsverifisering sikrer at hvis en del av systemet svikter, vil feilen ikke spre seg til resten av systemet og spesielt til kjernen og kritiske deler.
seL4-arkitekturen er kjent for bevegelige deler for å administrere kjerneressurser inn i brukerområdet og bruke de samme tilgangskontrollverktøyene for slike ressurser som for brukerressurser. Mikrokjernen gir ikke ferdige høynivåabstraksjoner for administrasjon av 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.
For ytterligere beskyttelse er alle komponentene unntatt mikrokjernen utviklet i Rust ved å bruke sikre programmeringsteknikker som minimerer minnefeil som fører til problemer som minnetilgang etter frigjøring, null-peker-dereferanser og bufferoverskridelser. En applikasjonslaster i seL4-miljøet, systemtjenester, et rammeverk for applikasjonsutvikling, en API for tilgang til systemanrop, en prosessbehandler, en mekanisme for dynamisk minneallokering osv. ble skrevet i Rust. Den verifiserte sammenstillingen bruker CAmkES-verktøysettet, utviklet av seL4-prosjektet. Komponenter for CAmkES kan også lages i Rust.
Rust fremtvinger minnesikkerhet ved kompilering gjennom referansekontroll, objekteierskap og objektlevetidssporing (scopes), og ved å evaluere riktigheten av minnetilganger under kjøring. Rust gir også beskyttelse mot heltallsoverløp, krever at variabelverdier initialiseres før bruk, bruker konseptet med uforanderlige referanser og variabler som standard, og tilbyr sterk statisk skriving for å minimere logiske feil.
Kilde: opennet.ru