Společnost Google oznámila otevření prací souvisejících s projektem KataOS, jehož cílem je vytvoření zabezpečeného operačního systému pro vestavěné zařízení. Systémové komponenty KataOS jsou napsány v jazyce Rust a běží nad mikrokernelem seL4, pro který byly na systémech RISC-V poskytnuty matematické důkazy o spolehlivosti, potvrzující plné soulady kódu se specifikacemi stanovenými formálním jazykem. Kód projektu je dostupný pod licencí Apache 2.0.
Systém podporuje platformy založené na architekturách RISC-V a ARM64. Pro simulaci práce seL4 a prostředí KataOS na hardware během vývoje se používá framework Renode. Jako referenční implementace byl navržen softwarově-hardwareový komplex Sparrow, který kombinuje KataOS s zabezpečenými čipy založenými na platformě OpenTitan. Navrhované řešení umožňuje spojit logicky verifikované jádro operačního systému se důvěryhodnými hardwarovými komponenty (RoT, Root of Trust), postavenými pomocí platformy OpenTitan a architekturou RISC-V. Kromě kódu KataOS se plánuje také zveřejnění všech ostatních komponent Sparrow, včetně hardwarové části.
Platforma se vyvíjí s ohledem na použití ve specializovaných čipech určených pro provádění aplikací strojového učení a zpracování důvěrných informací, které vyžadují zvláštní úroveň ochrany a potvrzení absence selhání. Jako příklad takových aplikací jsou uváděny systémy manipulující s obrazy lidí a hlasovými nahrávkami. Použití verifikace spolehlivosti v KataOS zaručuje, že v případě selhání jedné části systému se toto selhání nešíří na zbytek systému a zejména na jádro a kritické části.
Architektura seL4 se vyznačuje oddělením částí pro správu zdrojů jádra do uživatelského prostoru a použitím stejných prostředků pro kontrolu přístupu k těmto zdrojům jako pro uživatelské zdroje. Mikro-jádro neposkytuje hotové vysoceúrovňové abstrakce pro správu souborů, procesů, síťových připojení atd., místo toho poskytuje pouze minimální mechanismy pro správu přístupu k fyzickému adresnímu prostoru, přerušením a zdrojům procesoru. Vysoceúrovňové abstrakce a ovladače pro interakci s hardwarem jsou implementovány odděleně nad mikro-jádrem ve formě úloh běžících na uživatelské úrovni. Přístup těchto úloh k dostupným zdrojům mikro-jádra je organizován prostřednictvím definování pravidel.
Pro dodatečnou ochranu jsou všechny komponenty, kromě mikro-jádra, původně vyvíjeny v jazyce Rust pomocí bezpečných programovacích technik, které minimalizují chyby při práci s pamětí, vedoucí k problémům jako je přístup do oblasti paměti po jejím uvolnění, dereferencování nulových ukazatelů a ohraničení bufferu. V Rustu jsou mimo jiné napsány načítače aplikací v prostředí seL4, systémové služby, framework pro vývoj aplikací, API pro přístup k systémovým volání, správce procesů, mechanismus dynamického rozdělení paměti apod. Pro verifikovanou konstrukci je využíván nástroj CAmkES, vyvíjený projektem seL4. Komponenty pro CAmkES mohou být také vytvářeny v jazyce Rust.
Bezpečné zacházení s pamětí je v Rustu zajištěno během kompilace pomocí kontroly odkazů, sledování vlastnictví objektů a zohlednění doby života objektů (oblastí viditelnosti), jakož i hodnocením správnosti přístupu k paměti během vykonávání kódu. Rust také poskytuje prostředky na ochranu před přetečením celých čísel, vyžaduje povinnou inicializaci hodnot proměnných před použitím, aplikuje koncept neměnnosti (immutable) odkazů a proměnných ve výchozím nastavení a nabízí silnou statickou typizaci pro minimalizaci logických chyb.
Zdroj: opennet.ru
