Kompania Google shpalli hapjen e punimeve lidhur me projektin KataOS, i cili synon të krijojë një sistem operativ të sigurt për pajisje të integruara. Komponentët sistemorë të KataOS janë shkruar në gjuhën Rust dhe funksionojnë mbi mikro-bërthamën seL4, për të cilën është ofruar një provë matematike e besueshmërisë në sistemet RISC-V, 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.
Sistemi siguron mbështetje për platformat e bazuara në arkitekturat RISC-V dhe ARM64. Për të simuluar funksionimin e seL4 dhe mjedisit KataOS mbi pajisje gjatë zhvillimit, përdoret framework-u Renode. Si implementim referent është propozuar kompleksi software-harduer Sparrow, i cili kombinon KataOS me çipa të sigurt të bazuar në platformën OpenTitan. Zgjidhja e propozuar lejon kombinimin e një bërthame operativ sistem të verifikuar logjikisht me komponentë harduerik besueshëm (RoT, Root of Trust), të ndërtuar duke përdorur platformën OpenTitan dhe arkitekturën RISC-V. Përveç kodit të KataOS, planifikohet që në të ardhmen të hapen edhe të gjithë komponentët e tjerë të Sparrow, përfshirë përbërësin harduerik.
Platforma po zhvillohet duke u bazuar në aplikimet për çipa të specializuar, të dizajnuar për të ekzekutuar aplikacione për mësimin e makinave dhe trajtimin e informacionit konfidencial, që kërkojnë një nivel të veçantë mbrojtjeje dhe konfirmimi të mungesës së defekteve. Si shembuj të aplikacioneve të tilla përmenden sistemet që manipulojnë imazhet e njerëzve dhe regjistrimet e zërit. Përdorimi i verifikimit të besueshmërisë në KataOS siguron që në rastin e një defekti në një pjesë të sistemit, ky defekt nuk do të përhapet në pjesën tjetër të sistemit dhe, veçanërisht, në bërthamën dhe pjesët kritike.
Arkitektura seL4 veçohet për zhvendosjen e pjesëve për menaxhimin e burimeve të bërthamës në hapësirën e përdoruesit dhe për aplikimin e të njëjtat mjete për ndarjen e aksesit, si për burimet e përdoruesve. Mikro-bërthama nuk ofron abastraksione të larta për menaxhimin e skedarëve, proceseve, lidhjeve rrjetore etj., por ofron vetëm mekanizmat minimalë për menaxhimin e aksesit në hapësirën fizike adresimit, ndërprerjet dhe burimet e procesorit. Abstraksionet dhe drejtuesit e nivelit të lartë për ndërveprimin me pajisjet krijohen veçmas mbi mikro-bërthamën në formën e detyrave që ekzekutohen në nivelin e përdoruesit. Aksesi i këtyre detyrave në burimet që mikro-bërthama ka organizohet përmes përcaktimit të rregullave.
Për mbrojtje shtesë, të gjithë komponentët, përveç mikro-bërthamës, zhvillohen fillimisht në gjuhën Rust duke përdorur teknikat e sigurta të programimit, që minimizojnë gabimet gjatë punës me kujtesën, të cilat çojnë në probleme si aksesimi i hapësirës së kujtesës pas lirimit të saj, dereferencimi i treguesve null dhe dalja jashtë kufijve të tamponëve. Po ashtu, janë shkruar në Rust ngarkuesi i aplikacioneve në ambientin seL4, shërbimet sistemore, framework-u për zhvillimin e aplikacioneve, API për aksesin në thirrjet sistemore, menaxheri i proceseve, mekanizmi i shpërndarjes dinamike të kujtesës, etj. Për ndërtimin e verifikuar përdoret mjetet CAmkES, të zhvilluara nga projekti seL4. Komponentët për CAmkES gjithashtu mund të krijohen në gjuhën Rust.
Puna e sigurt me kujtesën sigurohet në Rust gjatë kompilimit përmes kontrollit të referencave, ndjekjes së pronësisë së objekteve dhe marrjes në konsideratë të kohës së jetës së objekteve (hapësirës së dukshmërisë), si dhe përmes vlerësimit të korrektësisë së aksesit në kujtesë gjatë ekzekutimit të kodit. Rust gjithashtu siguron mjete për mbrojtje nga tepricat e numrave të plotë, kërkon inicializimin e detyruar të vlerave të variablave përpara përdorimit, aplikon 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
