Google je najavio otkriće razvoja u vezi s projektom KataOS, čiji je cilj stvaranje sigurnog operativnog sistema za ugrađeni hardver. Komponente sistema KataOS su napisane u Rust-u i pokreću se na seL4 mikrokernelu, za koji je obezbeđen matematički dokaz pouzdanosti na RISC-V sistemima, što ukazuje da je kod u potpunosti usklađen sa specifikacijama navedenim u formalnom jeziku. Kod projekta je otvoren pod licencom Apache 2.0.
Sistem pruža podršku za platforme zasnovane na RISC-V i ARM64 arhitekturi. Za simulaciju rada seL4 i KataOS okruženja na vrhu hardvera, Renode framework se koristi tokom procesa razvoja. Kao referentna implementacija, predložen je softversko-hardverski kompleks Sparrow, koji kombinuje KataOS sa sigurnim čipovima baziranim na OpenTitan platformi. Predloženo rešenje vam omogućava da kombinujete logički verifikovanu kernel operativnog sistema sa pouzdanim hardverskim komponentama (RoT, Root of Trust), izgrađenim korišćenjem OpenTitan platforme i RISC-V arhitekture. Pored KataOS koda, planirano je otvaranje svih ostalih Sparrow komponenti, uključujući hardversku komponentu, u budućnosti.
Platforma se razvija s ciljem primjene u specijalizovanim čipovima dizajniranim za pokretanje aplikacija za strojno učenje i obradu povjerljivih informacija, koje zahtijevaju poseban nivo zaštite i potvrdu odsustva kvarova. Primjeri takvih aplikacija uključuju sisteme koji manipulišu slikama ljudi i glasovnim snimcima. KataOS-ova upotreba verifikacije pouzdanosti osigurava da ako jedan dio sistema otkaže, kvar se neće proširiti na ostatak sistema, a posebno na kernel i kritične dijelove.
Arhitektura seL4 je značajna po pokretnim dijelovima za upravljanje resursima kernela u korisnički prostor i primjeni istih alata za kontrolu pristupa za takve resurse kao i za korisničke resurse. Mikrokernel ne pruža gotove apstrakcije visokog nivoa za upravljanje datotekama, procesima, mrežnim vezama i slično; umjesto toga, pruža samo minimalne mehanizme za kontrolu pristupa fizičkom adresnom prostoru, prekidima i procesorskim resursima. Apstrakcije visokog nivoa i drajveri za interakciju sa hardverom implementirani su odvojeno na vrhu mikrokernela u obliku zadataka na nivou korisnika. Pristup takvih zadataka resursima dostupnim mikrokernelu je organizovan kroz definiciju pravila.
Za dodatnu zaštitu, sve komponente osim mikrokernela su izvorno razvijene u Rustu koristeći tehnike bezbednog programiranja koje minimiziraju greške u memoriji koje dovode do problema kao što su pristup memoriji nakon oslobađanja, dereferenciranje nulte pokazivača i prekoračenje bafera. Učitavač aplikacija u okruženju seL4, sistemske usluge, okvir za razvoj aplikacija, API za pristup sistemskim pozivima, menadžer procesa, mehanizam za dinamičku alokaciju memorije, itd. su napisani u Rustu. Verifikovani sklop koristi CAmkES alat, razvijen od strane projekta seL4. Komponente za CAmkES se također mogu kreirati u Rustu.
Rust pojačava sigurnost memorije u vrijeme kompajliranja kroz provjeru referenci, vlasništvo nad objektom i praćenje životnog vijeka objekta (opsezi) i procjenom ispravnosti pristupa memoriji u vrijeme izvođenja. Rust također pruža zaštitu od prekoračenja cijelih brojeva, zahtijeva da se vrijednosti varijabli inicijaliziraju prije upotrebe, koristi koncept nepromjenjivih referenci i varijabli prema zadanim postavkama i nudi snažno statičko kucanje kako bi se minimizirale logičke greške.
izvor: opennet.ru