A Google megnyitotta a KataOS biztonságos operációs rendszer kódját

A Google bejelentette a KataOS projekthez kapcsolódó fejlesztések felfedezését, amelyek célja egy biztonságos operációs rendszer létrehozása a beágyazott hardverekhez. A KataOS rendszerkomponensek Rust nyelven íródnak, és a seL4 mikrokernel tetején futnak, amihez a megbízhatóság matematikai bizonyítéka RISC-V rendszereken található, jelezve, hogy a kód teljes mértékben megfelel a hivatalos nyelvben megadott specifikációknak. A projekt kódja az Apache 2.0 licenc alatt van nyitva.

A rendszer támogatja a RISC-V és ARM64 architektúrákon alapuló platformokat. A seL4 és a KataOS környezet hardveren felüli működésének szimulálásához a Renode keretrendszert használják a fejlesztés során. Referencia megvalósításként a Sparrow hardver- és szoftverrendszert javasolják, amely a KataOS-t az OpenTitan platformon alapuló biztonságos chipekkel kombinálja. A javasolt megoldás lehetővé teszi a logikailag ellenőrzött operációs rendszer kernel és az OpenTitan platform és a RISC-V architektúra felhasználásával készült megbízható hardverkomponensek (RoT, Root of Trust) kombinálását. A KataOS kódon kívül a tervek szerint a jövőben megnyitják a Sparrow összes többi összetevőjét is, beleértve a hardverkomponenst is.

A platform fejlesztése során a gépi tanulási és adatvédelmi alkalmazások futtatására tervezett, célzott chipeket szem előtt tartva, amelyek meghatározott szintű védelmet és biztosítékot igényelnek, hogy nincsenek hibák. Az ilyen alkalmazások példájaként olyan rendszereket adunk, amelyek manipulálják az emberekről készült képeket és a hangfelvételeket. A megbízhatóság-ellenőrzés használata a KataOS-ban biztosítja, hogy a rendszer egy részének meghibásodása esetén ez a hiba ne terjedjen át a rendszer többi részére, és különösen a kernelre és a kritikus részekre.

A seL4 architektúra figyelemre méltó arról, hogy a kernel erőforrások kezeléséhez szükséges alkatrészeket a felhasználói térbe mozgatja, és ugyanazokat a hozzáférés-szabályozásokat alkalmazza az ilyen erőforrásokhoz, mint a felhasználói erőforrásokhoz. A mikrokernel nem ad azonnali, magas szintű absztrakciókat a fájlok, folyamatok, hálózati kapcsolatok és hasonlók kezeléséhez, ehelyett csak minimális mechanizmusokat biztosít a fizikai címtérhez, a megszakításokhoz és a processzorerőforrásokhoz való hozzáférés szabályozásához. A magas szintű absztrakciók és a hardverrel való interakcióhoz szükséges illesztőprogramok külön vannak implementálva a mikrokernel tetején, felhasználói szintű feladatok formájában. Az ilyen feladatoknak a mikrokernel rendelkezésére álló erőforrásokhoz való hozzáférése szabályok meghatározásán keresztül történik.

A további védelem érdekében a mikrokernel kivételével az összes összetevőt eredetileg a Rustban fejlesztették biztonságos programozási technikákkal, amelyek minimalizálják a memóriával végzett munka során előforduló hibákat, ami olyan problémákhoz vezet, mint a memóriaterület elérése annak felszabadítása után, a nulla mutatók hivatkozásának megszüntetése és a puffertúllépés. A seL4 környezetben lévő alkalmazásbetöltő, a rendszerszolgáltatások, az alkalmazásfejlesztő keretrendszer, a rendszerhívásokhoz való hozzáférés API-ja, a folyamatkezelő, a dinamikus memóriafoglalási mechanizmus stb. Rustban vannak megírva. Az ellenőrzött összeállításhoz a seL4 projekt által kifejlesztett CAmkES eszközkészletet használják. A CAmkES komponensei Rustban is létrehozhatók.

A memóriabiztos kezelést a Rust fordítási időben biztosítja a referenciaellenőrzés, az objektum tulajdonjogának és az objektum élettartamának (hatókörének) nyomon követésével, valamint a kódvégrehajtás során a memória-hozzáférés helyességének értékelésével. A Rust védelmet is nyújt az egész számok túlcsordulása ellen, megköveteli a változók inicializálását használat előtt, alapértelmezés szerint alkalmazza a megváltoztathatatlan hivatkozások és változók koncepcióját, és erős statikus gépelést kínál a logikai hibák minimalizálása érdekében.

Forrás: opennet.ru

Hozzászólás