Compania Google a anunțat deschiderea lucrărilor legate de proiectul KataOS, destinat creării unui sistem de operare securizat pentru echipamente încorporate. Componentele sistemului KataOS sunt scrise în limbajul Rust și rulează deasupra unui microkernel seL4, pentru care în sistemele RISC-V a fost furnizată o dovadă matematică a fiabilității, dovedind conformitatea completă a codului cu specificațiile definite într-un limbaj formal. Codul proiectului este disponibil sub licența Apache 2.0.
Sistemul asigură suport pentru platforme bazate pe arhitecturi RISC-V și ARM64. Pentru simularea funcționării seL4 și a mediului KataOS deasupra echipamentului, în timpul dezvoltării se utilizează cadrul Renode. Ca implementare de referință, a fost propus un complex hardware-software Sparrow, combinând KataOS cu cipuri securizate bazate pe platforma OpenTitan. Soluția propusă permite combinarea unei nuclee de sistem de operare verificate logic cu componente hardware de încredere (RoT, Root of Trust), construite folosind platforma OpenTitan și arhitectura RISC-V. Pe lângă codul KataOS, se preconizează deschiderea tuturor celorlalte componente Sparrow, inclusiv partea hardware.
Platforma se dezvoltă având în vedere utilizarea în cipuri specializate, destinate să execute aplicații pentru învățarea automată și procesarea informațiilor confidențiale, care necesită un anumit nivel de protecție și confirmare a lipsei defecțiunilor. Un exemplu de astfel de aplicații sunt sistemele care manipulează imagini ale oamenilor și înregistrări vocale. Utilizarea în KataOS a verificării fiabilității garantează că, în cazul unei defecțiuni într-o parte a sistemului, aceasta nu se va răspândi la restul sistemului, în special la nucleu și părțile critice.
Arhitectura seL4 este remarcabilă prin externalizarea părților de gestionare a resurselor nucleului în spațiul utilizatorului și prin aplicarea acelorași mijloace de separare a accesului pentru aceste resurse ca pentru resursele utilizatorului. Microkernelul nu oferă abstractions de nivel înalt gata făcute pentru gestionarea fișierelor, proceselor, conexiunilor de rețea etc.; în schimb, oferă doar mecanisme minime pentru gestionarea accesului la spațiul de adresare fizic, la întreruperi și la resursele procesorului. Abstracțiile de nivel înalt și driverele pentru interacțiunea cu hardware-ul sunt implementate separat, deasupra microkernelului, sub formă de sarcini executate la nivel de utilizator. Accesul acestor sarcini la resursele disponibile în microkernel este organizat prin definirea unor reguli.
Pentru o protecție suplimentară, toate componentele, cu excepția microkernelului, sunt inițial dezvoltate în limbajul Rust, folosind tehnici de programare sigure, care minimizează erorile în exploatarea memoriei, ce pot duce la probleme precum accesarea unei zone de memorie după ce aceasta a fost eliberată, dereferințierea pointerilor nuli și depășirea limitelor buffer-ului. În Rust sunt scrise, de asemenea, încărcătorul de aplicații în mediul seL4, serviciile de sistem, cadrul pentru dezvoltarea aplicațiilor, API-ul pentru accesul la apelurile de sistem, managerul de procese, mecanismul de alocare dinamică a memoriei ș.a. Pentru compilarea verificată este folosit uneltele CAmkES, dezvoltate de proiectul seL4. Componentele pentru CAmkES pot fi, de asemenea, create în limbajul Rust.
Siguranța în exploatarea memoriei este asigurată în Rust în timpul compilării prin verificarea referințelor, urmărirea proprietății obiectelor și luarea în considerare a duratei de viață a obiectelor (zona de vizibilitate), precum și prin evaluarea corectitudinii accesului la memorie în timpul execuției codului. Rust oferă, de asemenea, mijloace pentru prevenirea depășirii întregului, impune inițializarea obligatorie a valorilor variabilelor înainte de utilizare, aplică conceptul de imutabilitate (immutable) pentru referințe și variabile în mod implicit și oferă o tipizare statică puternică pentru minimizarea erorilor logice.
Sursa: opennet.ro
