Kompania Google shpalli hapjen e zhvillimeve që lidhen me projektin KataOS, i cili është fokusuar në krijimin e një sistemi operativ të mbrojtur për pajisje të integruara. Komponentët sistemorë të KataOS janë shkruar në gjuhën Rust dhe ekzekutohen mbi mikro-bërthamen seL4, për të cilin në sistemet RISC-V është ofruar një provë matematikore besueshmërie, që dëshmon për përputhshmërinë e plotë të kodit me specifikimet e caktuara në një gjuhë formale. Kodi i projektit është i hapur nën licencën Apache 2.0.
Në sistem është siguruar mbështetje për platformat e bazuara në arkitekturën RISC-V dhe ARM64. Për simulimin e punës së seL4 dhe ambientit KataOS mbi pajisje gjatë zhvillimit, përdoret sistemi i kornizës Renode. Si një zgjidhje standarde propozohet kompleksi softuerik-hardware Sparrow, i cili kombinon KataOS me çipe të mbrojtura në bazë të platformës OpenTitan. Zgjidhja e propozuar lejon kombinimin e bërthames së sistemit operativ të verifikuar logjikisht me komponentë hardware të besueshëm (RoT, Root of Trust), të ndërtuar me platformën OpenTitan dhe arkitekturën RISC-V. Përveç kodit të KataOS, planifikohet që më tej të hapen të gjitha komponentët e tjera të Sparrow, duke përfshirë komponentën hardware.
Platforma po zhvillohet me një sy në përdorimin në çipa të specializuar, të dizajnuar për të ekzekutuar aplikacione për mësimin e makinës dhe përpunimin e informacioneve të ndjeshme, të cilëve u kërkohet një nivel i veçantë mbrojtjeje dhe konfirmimi të papërfshirjes së defekteve. Si një shembull i tillë aplikacionesh përmenden sistemet që manipullojnë imazhe të njerëzve dhe regjistrime të zërit. Përdorimi i verifikimit të besueshmërisë në KataOS garanton se në rast të një defekti në një pjesë të sistemit, ky defekt nuk do të përhapet në pjesën tjetër të sistemit dhe, konkretisht, në bërthamën dhe pjesët kritike.
Arkitektura seL4 është veçanërisht e dukshme për ndarjen e pjesëve për menaxhimin e burimeve të bërthamës në hapësirën e përdoruesit dhe përdorimin e të njëjtave mjete ndarëse për këto burime, ashtu si për burimet e përdoruesit. Mikro-bërthama nuk ofron abstraksione të gatshme të nivelit të lartë për menaxhimin e skedarëve, proceseve, lidhjeve rrjetërore etj., por ofron vetëm mekanizma minimale për menaxhimin e aksesit në hapësirën fizike të adresave, ndërprerjet dhe burimet e procesorit. Abstraksionet dhe drejtuesit e nivelit të lartë për ndërveprimin me pajisjet realizohen veçmas mbi mikro-bërthamën në formën e detyrave që ekzekutohen në nivelin e përdoruesit. Aksi i këtyre detyrave në burimet që ka mikro-bërthama organizohet përmes përcaktimit të rregullave.
Për një mbrojtje shtesë, të gjitha komponentet, përveç mikro-bërthamës, zhvillohen fillimisht në gjuhën Rust duke përdorur praktika të sigurta programimi, që minimizojnë gabimet që kanë të bëjnë me kujtesën, të cilat çojnë në probleme të tilla si referimi në hapësirën e kujtesës pas çlirimit të saj, dereferencimi i treguesve të nul dhe dalja jashtë kufijve të buferit. Edhe menaxhuesi i aplikacioneve në mjedisin seL4, shërbimet sistemike, struktura për zhvillimin e aplikacioneve, API për qasje në thirrjet sistemike, menaxheri i proceseve, mekanizmi i shpërndarjes dinamike të kujtesës etj. janë shkruar në Rust. Për ndërtimin e verifikuar përdoret mjet CAmkES, i zhvilluar nga projekti seL4. Komponentët për CAmkES gjithashtu mund të krijohen në gjuhën Rust.
Sigurimi i punës së sigurt me kujtesën sigurohet në Rust gjatë kompilimit përmes kontrollit të referencave, gjurmimit të pronësisë së objekteve dhe llogaritjes së jetëgjatësisë së objekteve (fusha e dukshmërisë), si dhe përmes vlerësimit të saktësisë së aksesit në kujtesë gjatë ekzekutimit të kodit. Rust gjithashtu ofron mjete për mbrojtje nga mbinxehjet numërike, kërkon inicializimin e detyrueshëm të vlerave të variablave para përdorimit, zbatojnë konceptin e referencave dhe variablave të pandryshueshëm (immutable) si parazgjedhje dhe ofron një tipizim të fortë statik për minimizimin e gabimeve logjike.
Burimi: opennet.ru
