Google har annonceret opdagelsen af udviklinger relateret til KataOS-projektet, der sigter mod at skabe et sikkert operativsystem til indlejret hardware. KataOS-systemkomponenter er skrevet i Rust og køres oven på seL4-mikrokernen, for hvilken der er leveret et matematisk bevis for pålidelighed på RISC-V-systemer, hvilket indikerer, at koden fuldt ud overholder specifikationerne angivet i det formelle sprog. Projektkoden er åben under Apache 2.0-licensen.
Systemet understøtter platforme baseret på RISC-V og ARM64 arkitekturer. For at simulere driften af seL4 og KataOS-miljøet oven på hardwaren, bruges Renode-rammeværket under udviklingsprocessen. Som referenceimplementering foreslås Sparrow-software- og hardwarekomplekset, der kombinerer KataOS med sikre chips baseret på OpenTitan-platformen. Den foreslåede løsning giver dig mulighed for at kombinere en logisk verificeret operativsystemkerne med pålidelige hardwarekomponenter (RoT, Root of Trust), bygget ved hjælp af OpenTitan-platformen og RISC-V-arkitekturen. Ud over KataOS-koden er det planlagt at åbne alle andre Sparrow-komponenter, inklusive hardwarekomponenten, i fremtiden.
Platformen udvikles med øje for anvendelse i specialiserede chips designet til at køre applikationer til maskinlæring og behandling af fortrolig information, som kræver et særligt niveau af beskyttelse og bekræftelse af fravær af fejl. Eksempler på sådanne applikationer omfatter systemer, der manipulerer billeder af mennesker og stemmeoptagelser. KataOS' brug af pålidelighedsverifikation sikrer, at hvis en del af systemet fejler, vil fejlen ikke spredes til resten af systemet og især til kernen og kritiske dele.
seL4-arkitekturen er bemærkelsesværdig for bevægelige dele til styring af kerneressourcer til brugerrum og anvendelse af de samme adgangskontrolværktøjer til sådanne ressourcer som for brugerressourcer. Mikrokernen leverer ikke færdige abstraktioner på højt niveau til styring af filer, processer, netværksforbindelser og lignende; i stedet giver den kun minimale mekanismer til at kontrollere adgang til fysisk adresserum, afbrydelser og processorressourcer. Abstraktioner på højt niveau og drivere til interaktion med hardware implementeres separat oven på mikrokernen i form af opgaver på brugerniveau. Adgang til sådanne opgaver til de ressourcer, der er tilgængelige for mikrokernen, organiseres gennem definition af regler.
For yderligere beskyttelse er alle komponenter undtagen mikrokernen oprindeligt udviklet i Rust ved hjælp af sikre programmeringsteknikker, der minimerer hukommelsesfejl, der fører til problemer såsom hukommelsesadgang efter frigørelse, nul-pointer-dereferencer og bufferoverskridelser. En applikationsindlæser i seL4-miljøet, systemtjenester, et framework til applikationsudvikling, et API til at få adgang til systemkald, en procesmanager, en mekanisme til dynamisk hukommelsesallokering osv. blev skrevet i Rust. Den verificerede samling bruger CAmkES-værktøjssættet, udviklet af seL4-projektet. Komponenter til CAmkES kan også oprettes i Rust.
Rust håndhæver hukommelsessikkerhed ved kompilering gennem referencekontrol, objektejerskab og objektlevetidssporing (scopes) og ved at evaluere korrektheden af hukommelsesadgange under kørsel. Rust giver også beskyttelse mod heltalsoverløb, kræver, at variabelværdier initialiseres før brug, bruger konceptet med uforanderlige referencer og variabler som standard og tilbyder stærk statisk skrivning for at minimere logiske fejl.
Kilde: opennet.ru