Spoločnosť Google oznámila otvorenie svojich prác súvisiacich s projektom KataOS, ktorý je zameraný na vytvorenie zabezpečeného operačného systému pre vstavané zariadenia. Systémové komponenty KataOS sú napísané v jazyku Rust a bežia na mikrojadre seL4, pre ktoré bolo na systémoch RISC-V poskytnuté matematické dôkazové osvedčenie o spoľahlivosti, preukazujúce, že kód je v plnom súlade so špecifikáciami uvedenými v 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 činnosti seL4 a prostredia KataOS na hardvéri počas vývoja sa používa rámec Renode. Ako referenčná implementácia bol navrhnutý softvérovo-hardvérový komplex Sparrow, kombinujúci KataOS s bezpečnými čipmi na platforme OpenTitan. Navrhnuté riešenie umožňuje zlúčiť logicky overené jadro operačného systému s dôveryhodnými hardvérovými komponentmi (RoT, Root of Trust), postavenými s použitím platformy OpenTitan a architektúry RISC-V. Okrem kódu KataOS sa plánuje v budúcnosti otvoriť aj všetky ostatné komponenty Sparrow, vrátane hardvérovej súčasti.
Platforma sa vyvíja s ohľadom na aplikácie v špecializovaných čipoch, určených na vykonávanie aplikácií pre strojové učenie a spracovanie citlivých informácií, ktoré vyžadujú zvláštnu úroveň zabezpečenia a potvrdenia neprítomnosti porúch. Ako príklad takýchto aplikácií sa uvádzajú systémy manipulujúce s obrazmi ľudí a hlasovými nahrávkami. Použitie verifikácie spoľahlivosti v KataOS zaručuje, že v prípade poruchy v jednej časti systému sa táto porucha neprenáša na zvyšok systému, najmä na jadro a kritické časti.
Architektúra seL4 je pozoruhodná tým, že presúva časti správy zdrojov jadra do používateľského priestoru a aplikuje na tieto zdroje rovnaké prostriedky prístupu, aké sú určené pre používateľské zdroje. Mikrojadro neposkytuje hotové vysokolevelové abstrakcie pre správu súborov, procesov, sieťových pripojení a pod., namiesto toho poskytuje iba minimálne mechanizmy na správu prístupu k fyzickému adresnému priestoru, prerušenia a procesorové zdroje. Vysokolevelové abstrakcie a ovládače pre interakciu s hardvérom sú realizované oddelene nad mikrojadrom vo forme úloh vykonávaných na používateľskej úrovni. Prístup týchto úloh k zdrojom dostupným v mikrojadre je organizovaný prostredníctvom definovania pravidiel.
Pre dodatočnú ochranu sú všetky komponenty, okrem mikrojadra, pôvodne vyvíjané v jazyku Rust s použitím bezpečných prístupov k programovaniu, ktoré minimalizujú chyby pri práci s pamäťou, vedúce k takým problémom, ako je prístup k oblasti pamäte po jej uvoľnení, dereferencovanie nulových ukazovateľov a prekročenie hraníc vyrovnávacej pamäte. V Rust je taktiež napísaný načítač aplikácií v prostredí seL4, systémové služby, rámec na vývoj aplikácií, API pre prístup k systémovým volaniam, manažér procesov, mechanizmus dynamického prideľovania pamäte a pod. Pre verifikovanú zostavu je použitý nástroj CAmkES, ktorý vyvíja projekt seL4. Komponenty pre CAmkES môžu byť tiež vytvárané v jazyku Rust.
Bezpečná práca s pamäťou je zabezpečená v Rust počas kompilácie prostredníctvom kontroly referencií, sledovania vlastníctva objektov a zohľadnenia životnosti objektov (oblastí viditeľnosti), ako aj prostredníctvom hodnotenia správnosti prístupu k pamäti počas vykonávania kódu. Rust taktiež poskytuje prostriedky na ochranu pred pretečením celých čísel, požaduje povinnú inicializáciu hodnôt premenných pred ich použitím, aplikuje koncept nemennosti (immutable) referencií a premenných predvolene a ponúka silnú statickú typizáciu na minimalizáciu logických chýb.
Zdroj: opennet.ru
