Google oznámil objav vývoja súvisiaceho s projektom KataOS zameraným na vytvorenie bezpečného operačného systému pre vstavaný hardvér. Komponenty systému KataOS sú napísané v jazyku Rust a bežia na mikrojadre seL4, pre ktoré je poskytnutý matematický dôkaz spoľahlivosti na systémoch RISC-V, čo naznačuje úplný súlad kódu so špecifikáciami špecifikovanými vo formálnom jazyku. Kód projektu je otvorený pod licenciou Apache 2.0.
Systém poskytuje podporu pre platformy založené na architektúrach RISC-V a ARM64. Na simuláciu fungovania seL4 a prostredia KataOS nad hardvérom sa pri vývoji používa framework Renode. Ako referenčná implementácia je navrhnutý hardvérový a softvérový systém Sparrow, ktorý kombinuje KataOS so zabezpečenými čipmi založenými na platforme OpenTitan. Navrhované riešenie umožňuje kombinovať logicky overené jadro operačného systému s dôveryhodnými hardvérovými komponentmi (RoT, Root of Trust) vybudovanými na platforme OpenTitan a architektúre RISC-V. Okrem kódu KataOS sa v budúcnosti plánuje otvorenie všetkých ostatných komponentov Sparrowa, vrátane hardvérového komponentu.
Platforma sa vyvíja s ohľadom na účelovo vytvorené čipy pre aplikácie strojového učenia a ochrany súkromia, ktoré vyžadujú špecifickú úroveň ochrany a uistenia, že nedôjde k žiadnym zlyhaniam. Ako príklad takýchto aplikácií sa uvádzajú systémy, ktoré manipulujú s obrázkami ľudí a hlasovými nahrávkami. Použitie overovania spoľahlivosti v KataOS zaisťuje, že v prípade zlyhania jednej časti systému sa táto porucha nerozšíri do zvyšku systému a najmä do jadra a kritických častí.
Architektúra seL4 je pozoruhodná tým, že presúva časti na riadenie zdrojov jadra do užívateľského priestoru a aplikuje rovnaké riadenie prístupu pre tieto zdroje ako pre užívateľské zdroje. Mikrokernel neposkytuje predpripravené abstrakcie na vysokej úrovni pre správu súborov, procesov, sieťových pripojení a podobne, namiesto toho poskytuje len minimálne mechanizmy na riadenie prístupu k fyzickému adresnému priestoru, prerušeniam a zdrojom procesora. Vysokoúrovňové abstrakcie a ovládače pre interakciu s hardvérom sú implementované oddelene na vrchole mikrojadra vo forme úloh na užívateľskej úrovni. Prístup takýchto úloh k zdrojom dostupným pre mikrokernel je organizovaný prostredníctvom definície pravidiel.
Pre dodatočnú ochranu sú všetky komponenty okrem mikrojadra pôvodne vyvinuté v Ruste pomocou bezpečných programovacích techník, ktoré minimalizujú chyby pri práci s pamäťou, čo vedie k problémom, ako je prístup k pamäťovej oblasti po jej uvoľnení, dereferencovanie nulových ukazovateľov a pretečenie vyrovnávacej pamäte. V Ruste je napísaný zavádzač aplikácií v prostredí seL4, systémové služby, framework pre vývoj aplikácií, API pre prístup k systémovým volaniam, manažér procesov, mechanizmus dynamickej alokácie pamäte atď. Na overenú montáž sa používa CAmkES toolkit vyvinutý projektom seL4. Komponenty pre CAmkES je možné vytvárať aj v Ruste.
Bezpečnosť pamäte je v Rust zabezpečená v čase kompilácie prostredníctvom kontroly referencií, sledovania vlastníctva objektu a životnosti objektu (rozsahu), ako aj hodnotením správnosti prístupu do pamäte počas vykonávania kódu. Rust tiež poskytuje ochranu proti pretečeniu celých čísel, vyžaduje inicializáciu premenných pred použitím, štandardne aplikuje koncept nemenných referencií a premenných a ponúka silné statické typovanie na minimalizáciu logických chýb.
Zdroj: opennet.ru