Google har meddelat att de \u00f6ppnar upp arbetet relaterat till projektet KataOS, som syftar till att skapa ett s\u00e4kert operativsystem f\u00f6r inbyggda enheter. Systemkomponenterna i KataOS \u00e4r skrivna i Rust och k\u00f6rs ovanp\u00e5 mikrok\u00e4rnan seL4, f\u00f6r vilken det finns en matematiskt bevisad tillf\u00f6rlitlighet p\u00e5 RISC-V-system, vilket vittnar om att koden helt \u00f6verensst\u00e4mmer med de specifikationer som angetts p\u00e5 ett formellt spr\u00e5k. Projektkoden \u00e4r \u00f6ppet under Apache 2.0-licensen. <\/p>\n
Systemet erbjuder st\u00f6d f\u00f6r plattformar baserade p\u00e5 arkitekturerna RISC-V och ARM64. F\u00f6r att simulera arbetet av seL4 och KataOS-milj\u00f6n ovanp\u00e5 h\u00e5rdvaran under utveckling anv\u00e4nds ramverket Renode. Som en referensimplementation f\u00f6resl\u00e5s det programvaru- och h\u00e5rdvarukomplex som kallas Sparrow, vilket kombinerar KataOS med s\u00e4kra chip baserade p\u00e5 OpenTitan-plattformen. Den f\u00f6reslagna l\u00f6sningen m\u00f6jligg\u00f6r en kombination av logiskt verifierad operativsystemk\u00e4rna med tillf\u00f6rlitliga h\u00e5rdvarukomponenter (RoT, Root of Trust), byggda med hj\u00e4lp av OpenTitan-plattformen och RISC-V-arkitekturen. F\u00f6rutom koden i KataOS planeras det att \u00e4ven \u00f6ppna alla andra komponenter av Sparrow, inklusive den h\u00e5rdvarubaserade delen. <\/p>\n
Plattformen utvecklas med avseende p\u00e5 anv\u00e4ndning i specialiserade chip, avsedda f\u00f6r att k\u00f6ra applikationer f\u00f6r maskininl\u00e4rning och behandling av konfidentiell information, som kr\u00e4ver en s\u00e4rskild niv\u00e5 av skydd och f\u00f6rs\u00e4kran om fr\u00e5nvaro av fel. Exempel p\u00e5 s\u00e5dana applikationer inkluderar system som hanterar bilder av m\u00e4nniskor och r\u00f6stinspelningar. Anv\u00e4ndningen av tillf\u00f6rlitlighetsverifiering i KataOS s\u00e4kerst\u00e4ller att om ett fel uppst\u00e5r i en del av systemet, s\u00e5 sprider sig inte detta fel till resten av systemet och specifikt inte till k\u00e4rnan och kritiska delar. <\/p>\n
seL4:s arkitektur \u00e4r anm\u00e4rkningsv\u00e4rd genom att dela upp delar av k\u00e4rnresurshantering i anv\u00e4ndarutrymmet och till\u00e4mpa samma \u00e5tkomstkontrollmedel p\u00e5 dessa resurser som f\u00f6r anv\u00e4ndarresurser. Mikrok\u00e4rnan erbjuder inga f\u00e4rdiga h\u00f6g-niv\u00e5 abstraktioner f\u00f6r hantering av filer, processer, n\u00e4tverksanslutningar m.m., utan tillhandah\u00e5ller endast minimala mekanismer f\u00f6r att hantera \u00e5tkomst till fysisk adressering, avbrott och CPU-resurser. H\u00f6g-niv\u00e5 abstraktioner och drivrutiner f\u00f6r kommunikation med h\u00e5rdvara implementeras separat ovanp\u00e5 mikrok\u00e4rnan i form av uppgifter som k\u00f6rs p\u00e5 anv\u00e4ndarniv\u00e5. \u00c5tkomsten f\u00f6r dessa uppgifter till den resurs som mikrok\u00e4rnan tillhandah\u00e5ller organiseras genom att definiera regler. <\/p>\n
F\u00f6r \u00f6kad s\u00e4kerhet utvecklas alla komponenter, f\u00f6rutom mikrok\u00e4rnan, ursprungligen i programmeringsspr\u00e5ket Rust med hj\u00e4lp av s\u00e4kra programmeringsmetoder som minimerar minnesfel, vilket kan leda till problem som \u00e5tkomst till minnesomr\u00e5den efter att de har frigjorts, avreferering av nullpekare och buffer\u00f6verskridanden. Applikationsladdaren i seL4-milj\u00f6n, systemtj\u00e4nster, ramverk f\u00f6r applikationsutveckling, API f\u00f6r \u00e5tkomst till systemanrop, processhanterare, mekanism f\u00f6r dynamisk minnesallokering, etc., \u00e4r ocks\u00e5 skrivna i Rust. F\u00f6r verifierade byggen anv\u00e4nds verktyget CAmkES, som utvecklas av seL4-projektet. Komponenter f\u00f6r CAmkES kan \u00e4ven skapas i Rust. <\/p>\n