A Google bejelentette a KataOS projekthez kapcsolódó munkálatainak megnyitását, amely egy biztonságos operációs rendszer létrehozására összpontosít beágyazott hardverek számára. A KataOS rendszerszemélyének komponensei Rust nyelven íródtak, és az seL4 mikrokernelre épülnek, amelynek megbízhatóságáról matematikai bizonyítékok állnak rendelkezésre RISC-V rendszereken, igazolva ezzel, hogy a kód megfelel a formális nyelvben megadott specifikációknak. A projekt kódja Apache 2.0 licenc alatt nyitott.
A rendszer támogatja a RISC-V és ARM64 architektúrákra épülő platformokat. A seL4 és a KataOS hardver környezet feletti működésének szimulálására fejlesztési folyamat során a Renode keretrendszert használják. Referencia megvalósításként a Sparrow hardver-szoftver komplexumot javasolták, amely a KataOS-t összekapcsolja az OpenTitan platformra épülő biztonságos chipekkel. A javasolt megoldás lehetővé teszi a logikailag hitelesített operációs rendszer kernelének ötvözését a bizalmi hardver komponensekkel (RoT, Root of Trust), amelyeket az OpenTitan platform és RISC-V architektúra felhasználásával építettek. A KataOS kódján kívül a Sparrow összes többi komponensét, beleértve a hardver elemet, a későbbiekben tervezik megnyitni.
A platform olyan specializált chipek alkalmazására összpontosít, amelyek gépi tanulási és érzékeny információk feldolgozására készültek, amelyek különleges védelmi szintet és meghibásodás-mentesség igazolását igénylik. Példaként említjük azokat a rendszereket, amelyek képek és hangfelvételek manipulálásával foglalkoznak. A KataOS megbízhatóság-ellenőrzésének használata garantálja, hogy ha a rendszer egy részében meghibásodás történik, az ne terjedjen át a rendszer többi részére, különösen a kernelre és a kritikus részekre.
A seL4 architektúrá figyelemre méltó, hogy a kernelforráskezelési részeit felhasználói térbe helyezik, és ugyanazokat a hozzáférési korlátozási eszközöket alkalmazzák a felhasználói erőforrásokhoz. A mikrokern nem biztosít kész, magas szintű absztrakciókat fájlok, folyamatok, hálózati kapcsolatok kezelésére, helyette csak minimális mechanizmusokat ad a fizikai címzési tér, megszakítások és a processzor erőforrásaihoz való hozzáférés kezelésére. A magas szintű absztrakciók és az eszközökkel való interakciós illesztők külön, a mikrokern felett valósulnak meg feladatok formájában, amelyeket felhasználói szinten hajtanak végre. Az ilyen feladatok hozzáférését a mikrokern erőforrásaihoz szabályok meghatározásával szervezik.
A további védelem érdekében az összes, a mikrokern kivételével létező komponens eredetileg Rust nyelven fejlődik, a memóriával való munka hibáit minimalizáló biztonságos programozási technikák alkalmazásával, amelyek olyan problémákhoz vezethetnek, mint a memóriaterület elérhetősége felszabadulás után, null pointer dereferálás és pufferhatárok túllépése. Rust nyelven készült többek között a seL4 környezetében futó alkalmazásbetöltő, rendszerszolgáltatások, alkalmazásfejlesztési keretrendszer, API a rendszerhívások elérhetőségéhez, folyamatkezelő, dinamikus memóriaelosztási mechanizmus stb. A verifikált buildhez a seL4 projekt fejleszti a CAmkES eszközkészletet. A CAmkES komponensek Rust nyelven is készíthetők.
A memória biztonságos kezelése a Rust-ban a fordítás során biztosított a hivatkozások ellenőrzésén, az objektumok tulajdonjogának nyomon követésén és az objektumok életciklusának (láthatósági területek) figyelembevételén keresztül, valamint a memóriahelyes hozzáférés helyességének értékelésén a kód futtatása alatt. A Rust emellett eszközöket biztosít a számértékek túlcsordulásának védelmére, megköveteli a változók kötelező inicializálását használat előtt, alkalmazza az alapértelmezett változók és hivatkozások változatlanságának (immutable) fogalmát, valamint erős statikus típust biztosít a logikai hibák minimalizálásához.
Forrás: opennet.ru
