A Google bejelentette KataOS projektjének nyílt forráskódú kiadását, amelynek célja egy biztonságos operációs rendszer létrehozása beágyazott hardverek számára. A KataOS rendszerkomponensei Rust nyelven íródtak, és az seL4 mikrokernelen futnak, amely matematikai megbízhatósági bizonyítással rendelkezik RISC-V rendszereken, igazolva a formális nyelven meghatározott kódspecifikációk teljes körű betartását. A projekt kódja nyílt forráskódú az Apache 2.0 licenc alatt.
A rendszer támogatja a RISC-V és ARM64 architektúrákon alapuló platformokat. A fejlesztés során a Renode keretrendszert használják az seL4 és a hardveren futó KataOS környezet szimulálására. Referencia implementációként a Sparrow hardver- és szoftverrendszert javasolják, amely a KataOS-t az OpenTitan platformon alapuló biztonságos chipekkel kombinálja. Ez a megoldás egy logikailag ellenőrzött operációs rendszer kernelt kombinál megbízható hardverkomponensekkel (RoT, vagy Root of Trust), amelyeket az OpenTitan platform és a RISC-V architektúra felhasználásával építettek. A KataOS kód mellett az összes többi Sparrow komponens, beleértve a hardvert is, nyílt forráskódú lesz.
A platformot azzal a céllal fejlesztik, hogy speciális chipekben lehessen használni, amelyeket gépi tanulási és érzékeny adatfeldolgozó alkalmazások futtatására terveztek, amelyek speciális szintű védelmet és hibaellenőrzést igényelnek. Ilyen alkalmazások például az emberi képeket és hangfelvételeket manipuláló rendszerek. A KataOS megbízhatósági ellenőrzése biztosítja, hogy ha a rendszer egyik része meghibásodik, az ne terjedjen át a rendszer többi részére, különösen a kernelre és a kritikus komponensekre.
Az seL4 architektúra figyelemre méltó, mivel a kernel erőforrás-kezelését a felhasználói térbe helyezi át, és ugyanazokat a hozzáférés-vezérlési mechanizmusokat alkalmazza ezekre az erőforrásokra, mint a felhasználói erőforrásokra. A mikrokernel nem biztosít kész, magas szintű absztrakciókat a fájlok, folyamatok, hálózati kapcsolatok és hasonlók kezelésére; ehelyett csak minimális mechanizmusokat biztosít a fizikai címtartományhoz, a megszakításokhoz és a processzorerőforrásokhoz való hozzáférés kezelésére. A hardverrel való interakcióhoz szükséges magas szintű absztrakciók és illesztőprogramok külön, felhasználói szinten futó feladatokként vannak megvalósítva a mikrokernel tetején. Ezen feladatok hozzáférése a mikrokernel erőforrásaihoz szabályok definiálásán keresztül történik.
A fokozott védelem érdekében a mikrokernel kivételével minden komponenst kezdetben Rustban fejlesztenek biztonságos programozási technikák alkalmazásával, amelyek minimalizálják a memóriahibákat, amelyek olyan problémákhoz vezethetnek, mint a memória elérése a felszabadítás után, a null pointerek dereferenciálása és a puffer túlcsordulás. A Rustot használják az seL4 környezetben az alkalmazásbetöltőhöz, a rendszerszolgáltatásokhoz, az alkalmazásfejlesztési keretrendszerhez, a rendszerhívások eléréséhez használt API-hoz, a folyamatkezelőhöz, a dinamikus memóriaelosztási mechanizmushoz és más komponensekhez is. Az seL4 projekt által fejlesztett CAmkES eszközkészletet ellenőrzött buildekhez használják. A CAmkES komponensei Rustban is írhatók.
A Rust fordítási időben biztosítja a memória biztonságát a referencia-ellenőrzés, az objektumtulajdonlás nyomon követése és az objektum élettartamának (hatókörének) elszámolása, valamint a futásidejű memória-hozzáférés érvényességének értékelése révén. A Rust védelmet nyújt az egész számok túlcsordulása ellen is, megköveteli a változóértékek kötelező inicializálását használat előtt, megvalósítja a megváltoztathatatlan referenciák és az alapértelmezett változók koncepcióját, és erős statikus típuskezelést kínál a logikai hibák minimalizálása érdekében.
Forrás: opennet.ru
