Google oznámil objev vývoje souvisejícího s projektem KataOS, jehož cílem je vytvořit bezpečný operační systém pro vestavěný hardware. Komponenty systému KataOS jsou napsány v Rustu a běží na mikrokernelu seL4, pro který byl poskytnut matematický důkaz spolehlivosti na systémech RISC-V, což naznačuje, že kód plně vyhovuje specifikacím uvedeným ve formálním jazyce. Kód projektu je otevřen pod licencí Apache 2.0.
Systém poskytuje podporu pro platformy založené na architekturách RISC-V a ARM64. Pro simulaci provozu seL4 a prostředí KataOS nad hardwarem se během procesu vývoje používá framework Renode. Jako referenční implementace je navržen softwarový a hardwarový komplex Sparrow, který kombinuje KataOS se zabezpečenými čipy založenými na platformě OpenTitan. Navržené řešení umožňuje kombinovat logicky ověřené jádro operačního systému s důvěryhodnými hardwarovými komponentami (RoT, Root of Trust), postavené na platformě OpenTitan a architektuře RISC-V. Kromě kódu KataOS se v budoucnu plánuje otevření všech dalších komponent Sparrow, včetně hardwarové.
Platforma je vyvíjena s ohledem na aplikaci ve specializovaných čipech určených ke spouštění aplikací pro strojové učení a zpracování důvěrných informací, které vyžadují zvláštní úroveň ochrany a potvrzení absence poruch. Příklady takových aplikací zahrnují systémy, které manipulují s obrázky lidí a hlasovými nahrávkami. Použití ověřování spolehlivosti v KataOS zajišťuje, že pokud jedna část systému selže, porucha se nerozšíří do zbytku systému a zejména do jádra a kritických částí.
Architektura seL4 se vyznačuje přesouváním částí pro správu zdrojů jádra do uživatelského prostoru a aplikací stejných nástrojů řízení přístupu pro takové zdroje jako pro uživatelské zdroje. Mikrokernel neposkytuje hotové abstrakce na vysoké úrovni pro správu souborů, procesů, síťových připojení a podobně, místo toho poskytuje pouze minimální mechanismy pro řízení přístupu k fyzickému adresnímu prostoru, přerušením a zdrojům procesoru. Vysokoúrovňové abstrakce a ovladače pro interakci s hardwarem jsou implementovány odděleně nad mikrokernelem ve formě úloh na uživatelské úrovni. Přístup těchto úkolů ke zdrojům, které má mikrojádro k dispozici, je organizován prostřednictvím definice pravidel.
Pro další ochranu jsou všechny komponenty kromě mikrojádra nativně vyvinuty v Rustu pomocí bezpečných programovacích technik, které minimalizují chyby paměti, které vedou k problémům, jako je přístup k paměti po uvolnění, dereference nulového ukazatele a přetečení vyrovnávací paměti. V Rustu byl napsán zavaděč aplikací v prostředí seL4, systémové služby, framework pro vývoj aplikací, API pro přístup k systémovým voláním, správce procesů, mechanismus pro dynamickou alokaci paměti atd. Ověřená sestava využívá sadu nástrojů CAmkES, vyvinutý projektem seL4. Komponenty pro CAmkES lze také vytvářet v Rustu.
Rust prosazuje bezpečnost paměti v době kompilace prostřednictvím kontroly referencí, vlastnictví objektů a sledování životnosti objektů (rozsahy) a vyhodnocováním správnosti přístupů do paměti za běhu. Rust také poskytuje ochranu proti přetečení celých čísel, vyžaduje inicializaci hodnot proměnných před použitím, standardně používá koncept neměnných referencí a proměnných a nabízí silné statické typování pro minimalizaci logických chyb.
Zdroj: opennet.ru