Google har tillkännagivit upptäckten av utvecklingar relaterade till KataOS-projektet, som syftar till att skapa ett säkert operativsystem för inbäddad hårdvara. KataOS-systemkomponenter är skrivna i Rust och körs ovanpå seL4-mikrokärnan, för vilken ett matematiskt bevis på tillförlitlighet har tillhandahållits på RISC-V-system, vilket indikerar att koden helt överensstämmer med specifikationerna i det formella språket. Projektkoden är öppen under Apache 2.0-licensen.
Systemet ger stöd för plattformar baserade på RISC-V- och ARM64-arkitekturer. För att simulera driften av seL4 och KataOS-miljön ovanpå hårdvaran, används Renode-ramverket under utvecklingsprocessen. Som referensimplementering föreslås Sparrows mjukvara och hårdvarukomplex, som kombinerar KataOS med säkra chips baserade på OpenTitan-plattformen. Den föreslagna lösningen låter dig kombinera en logiskt verifierad operativsystemkärna med pålitliga hårdvarukomponenter (RoT, Root of Trust), byggda med OpenTitan-plattformen och RISC-V-arkitekturen. Förutom KataOS-koden är det planerat att öppna alla andra Sparrow-komponenter, inklusive hårdvarukomponenten, i framtiden.
Plattformen utvecklas med sikte på applikation i specialiserade chip designade för att köra applikationer för maskininlärning och bearbetning av konfidentiell information, som kräver en speciell nivå av skydd och bekräftelse av frånvaro av fel. Exempel på sådana applikationer är system som manipulerar bilder av människor och röstinspelningar. KataOS användning av tillförlitlighetsverifiering säkerställer att om en del av systemet misslyckas, kommer felet inte att sprida sig till resten av systemet och i synnerhet till kärnan och kritiska delar.
seL4-arkitekturen är anmärkningsvärd för rörliga delar för att hantera kärnresurser i användarutrymme och tillämpa samma åtkomstkontrollverktyg för sådana resurser som för användarresurser. Mikrokärnan tillhandahåller inte färdiga abstraktioner på hög nivå för hantering av filer, processer, nätverksanslutningar och liknande, utan tillhandahåller endast minimala mekanismer för att kontrollera åtkomst till fysiskt adressutrymme, avbrott och processorresurser. Abstraktioner på hög nivå och drivrutiner för interaktion med hårdvara implementeras separat ovanpå mikrokärnan i form av uppgifter på användarnivå. Tillgång till sådana uppgifter till de resurser som är tillgängliga för mikrokärnan organiseras genom definition av regler.
För ytterligare skydd är alla komponenter utom mikrokärnan inbyggt utvecklade i Rust med säkra programmeringstekniker som minimerar minnesfel som leder till problem som minnesåtkomst efter frigöring, nollpekarereferenser och buffertöverskridanden. En applikationsladdare i seL4-miljön, systemtjänster, ett ramverk för applikationsutveckling, ett API för att komma åt systemanrop, en processhanterare, en mekanism för dynamisk minnesallokering etc. skrevs i Rust. Den verifierade sammansättningen använder CAmkES-verktygslådan, utvecklad av seL4-projektet. Komponenter för CAmkES kan också skapas i Rust.
Rust upprätthåller minnessäkerheten vid kompilering genom referenskontroll, objektägande och objektlivstidsspårning (scopes) och genom att utvärdera riktigheten av minnesåtkomster under körning. Rust ger också skydd mot heltalsspill, kräver att variabelvärden initieras före användning, använder konceptet med oföränderliga referenser och variabler som standard, och erbjuder stark statisk typning för att minimera logiska fel.
Källa: opennet.ru