Google har annonceret åbningen af udviklingsarbejdet relateret til projektet KataOS, som sigter mod at skabe et sikkert operativsystem til indlejrede enheder. Systemkomponenterne i KataOS er skrevet i Rust og kører oven på mikrokernen seL4, for hvilken der på RISC-V systemer er givet et matematisk bevis for pålidelighed, der viser, at koden er helt i overensstemmelse med specifikationerne angivet på det formelle sprog. Koden til projektet er åbnet under Apache 2.0-licensen.
Systemet understøtter platforme baseret på RISC-V og ARM64-arkitektur. For at simulere driften af seL4 og KataOS-miljøet på hardware under udviklingen bruges rammeværket Renode. Som referenceimplementering tilbydes det software-hardware kompleks Sparrow, der kombinerer KataOS med sikre chips baseret på OpenTitan-platformen. Den foreslåede løsning muliggør en kombination af et logisk verificeret operativsystemkernel med pålidelige hardwarekomponenter (RoT, Root of Trust), bygget ved hjælp af OpenTitan-platformen og RISC-V-arkitekturen. Udover koden til KataOS planlægges det også at åbne alle andre komponenter af Sparrow, inklusive hardwarekomponenten.
Platformen udvikler sig med henblik på brug i specialiserede chips designet til at køre applikationer til maskinlæring og behandling af fortrolige oplysninger, der kræver et særligt niveau af beskyttelse og bekræftelse af, at der ikke er fejl. Eksempler på sådanne applikationer inkluderer systemer, der manipulerer billeder af mennesker og lydoptagelser. Brug af pålidelighedsverifikation i KataOS sikrer, at i tilfælde af en fejl i en del af systemet, vil denne fejl ikke sprede sig til resten af systemet, især til kernen og kritiske dele.
seL4-arkitekturen er bemærkelsesværdig ved at flytte dele af kerneressourcehåndtering til brugerrum og anvende de samme adgangsbegrænsningsmetoder til disse ressourcer, som til brugerressourcer. Mikrokernen tilbyder ikke færdige høj-niveau abstraktioner til filhåndtering, processer, netværksforbindelser osv.; i stedet leverer den kun minimale mekanismer til at styre adgangen til fysisk adresserum, afbrydelser og processorressourcer. Høj-niveau abstraktioner og drivere til interaktion med hardware implementeres separat oven på mikrokernen i form af opgaver, der kører på brugerniveau. Adgangen for disse opgaver til de ressourcer, som mikrokernen har, organiseres gennem etablering af regler.
For yderligere beskyttelse udvikles alle komponenter undtagen mikrokernen oprindeligt i Rust ved hjælp af sikre programmeringsmetoder, der minimerer hukommelsesfejl, som kan føre til problemer som adgang til frigivet hukommelse, dereferencering af nulpegepunkter og bufferoverskridelse. Også applikationsloaderen i seL4-miljøet, systemtjenester, udviklingsrammeværk til applikationer, API til adgang til systemopkald, procesmanager, dynamisk hukommelsesfordelingsmekanisme osv. er skrevet i Rust. CAmkES-værktøjet, som udvikles af seL4-projektet, anvendes til verificerbar opbygning. Komponenter til CAmkES kan også oprettes i Rust.
Sikker hukommelsesarbejde sikres i Rust under kompilering gennem referencekontrol, sporing af ejerskab af objekter og håndtering af objektlivscyklus (synlighed) samt ved at vurdere korrektheden af hukommelsesadgang under kørsel af koden. Rust tilbyder også værktøjer til at beskytte mod heltalsoverflow, kræver, at variabler skal initialiseres, før de anvendes, anvender begrebet uforanderlighed (immutable) for referencer og variabler som standard og tilbyder stærk statisk typing for at minimere logiske fejl.
Kilde: opennet.ru
