Google har meddelat att de öppnar upp arbetet relaterat till projektet KataOS, som syftar till att skapa ett säkert operativsystem för inbyggda enheter. Systemkomponenterna i KataOS är skrivna i Rust och körs ovanpå mikrokärnan seL4, för vilken det finns en matematiskt bevisad tillförlitlighet på RISC-V-system, vilket vittnar om att koden helt överensstämmer med de specifikationer som angetts på ett formellt språk. Projektkoden är öppet under Apache 2.0-licensen.
Systemet erbjuder stöd för plattformar baserade på arkitekturerna RISC-V och ARM64. För att simulera arbetet av seL4 och KataOS-miljön ovanpå hårdvaran under utveckling används ramverket Renode. Som en referensimplementation föreslås det programvaru- och hårdvarukomplex som kallas Sparrow, vilket kombinerar KataOS med säkra chip baserade på OpenTitan-plattformen. Den föreslagna lösningen möjliggör en kombination av logiskt verifierad operativsystemkärna med tillförlitliga hårdvarukomponenter (RoT, Root of Trust), byggda med hjälp av OpenTitan-plattformen och RISC-V-arkitekturen. Förutom koden i KataOS planeras det att även öppna alla andra komponenter av Sparrow, inklusive den hårdvarubaserade delen.
Plattformen utvecklas med avseende på användning i specialiserade chip, avsedda för att köra applikationer för maskininlärning och behandling av konfidentiell information, som kräver en särskild nivå av skydd och försäkran om frånvaro av fel. Exempel på sådana applikationer inkluderar system som hanterar bilder av människor och röstinspelningar. Användningen av tillförlitlighetsverifiering i KataOS säkerställer att om ett fel uppstår i en del av systemet, så sprider sig inte detta fel till resten av systemet och specifikt inte till kärnan och kritiska delar.
seL4:s arkitektur är anmärkningsvärd genom att dela upp delar av kärnresurshantering i användarutrymmet och tillämpa samma åtkomstkontrollmedel på dessa resurser som för användarresurser. Mikrokärnan erbjuder inga färdiga hög-nivå abstraktioner för hantering av filer, processer, nätverksanslutningar m.m., utan tillhandahåller endast minimala mekanismer för att hantera åtkomst till fysisk adressering, avbrott och CPU-resurser. Hög-nivå abstraktioner och drivrutiner för kommunikation med hårdvara implementeras separat ovanpå mikrokärnan i form av uppgifter som körs på användarnivå. Åtkomsten för dessa uppgifter till den resurs som mikrokärnan tillhandahåller organiseras genom att definiera regler.
För ökad säkerhet utvecklas alla komponenter, förutom mikrokärnan, ursprungligen i programmeringsspråket Rust med hjälp av säkra programmeringsmetoder som minimerar minnesfel, vilket kan leda till problem som åtkomst till minnesområden efter att de har frigjorts, avreferering av nullpekare och bufferöverskridanden. Applikationsladdaren i seL4-miljön, systemtjänster, ramverk för applikationsutveckling, API för åtkomst till systemanrop, processhanterare, mekanism för dynamisk minnesallokering, etc., är också skrivna i Rust. För verifierade byggen används verktyget CAmkES, som utvecklas av seL4-projektet. Komponenter för CAmkES kan även skapas i Rust.
Säker minneshantering upprätthålls i Rust under kompilering genom att kontrollera referenser, spåra ägarskap av objekt och ta hänsyn till objekts livslängd (tillgänglighet), samt genom att utvärdera korrekt åtkomst till minnet under kodens körning. Rust tillhandahåller också medel för att skydda mot heltalsöverflöden, kräver obligatorisk initialisering av variabelvärden innan användning, tillämpar konceptet av oföränderliga (immutable) referenser och variabler som standard samt erbjuder stark statisk typning för att minimera logiska fel.
Källa: opennet.ru
