Google ha annunciato la scoperta di sviluppi relativi al progetto KataOS, volto a creare un sistema operativo sicuro per hardware embedded. I componenti del sistema KataOS sono scritti in Rust e girano sul microkernel seL4, per il quale è stata fornita una prova matematica di affidabilità sui sistemi RISC-V, indicando che il codice è pienamente conforme alle specifiche specificate nel linguaggio formale. Il codice del progetto è aperto con la licenza Apache 2.0.
Il sistema fornisce supporto per piattaforme basate su architetture RISC-V e ARM64. Per simulare il funzionamento di seL4 e dell'ambiente KataOS sull'hardware, durante il processo di sviluppo viene utilizzato il framework Renode. Come implementazione di riferimento, viene proposto il complesso software e hardware Sparrow, che combina KataOS con chip sicuri basati sulla piattaforma OpenTitan. La soluzione proposta consente di combinare un kernel del sistema operativo logicamente verificato con componenti hardware affidabili (RoT, Root of Trust), costruiti utilizzando la piattaforma OpenTitan e l'architettura RISC-V. Oltre al codice KataOS, in futuro si prevede di aprire tutti gli altri componenti Sparrow, compreso il componente hardware.
La piattaforma è stata sviluppata con un occhio all'applicazione in chip specializzati progettati per eseguire applicazioni di apprendimento automatico ed elaborazione di informazioni riservate, che richiedono uno speciale livello di protezione e conferma dell'assenza di guasti. Esempi di tali applicazioni includono sistemi che manipolano immagini di persone e registrazioni vocali. L'uso della verifica dell'affidabilità da parte di KataOS garantisce che se una parte del sistema fallisce, il guasto non si diffonderà al resto del sistema e, in particolare, al kernel e alle parti critiche.
L'architettura seL4 si distingue per lo spostamento di parti per la gestione delle risorse del kernel nello spazio utente e per l'applicazione degli stessi strumenti di controllo dell'accesso per tali risorse come per le risorse utente. Il microkernel non fornisce astrazioni di alto livello già pronte per la gestione di file, processi, connessioni di rete e simili; fornisce invece solo meccanismi minimi per controllare l'accesso allo spazio degli indirizzi fisici, agli interrupt e alle risorse del processore. Astrazioni e driver di alto livello per l'interazione con l'hardware sono implementati separatamente sul microkernel sotto forma di attività a livello utente. L'accesso di tali compiti alle risorse a disposizione del microkernel è organizzato attraverso la definizione di regole.
Per una protezione aggiuntiva, tutti i componenti tranne il microkernel sono sviluppati nativamente in Rust utilizzando tecniche di programmazione sicure che riducono al minimo gli errori di memoria che portano a problemi come accesso alla memoria dopo la liberazione, dereferenziazioni di puntatori nulli e sovraccarichi del buffer. In Rust sono stati scritti un caricatore di applicazioni nell'ambiente seL4, servizi di sistema, un framework per lo sviluppo di applicazioni, un'API per l'accesso alle chiamate di sistema, un gestore di processi, un meccanismo per l'allocazione dinamica della memoria, ecc. L'assembly verificato utilizza il toolkit CAmkES, sviluppato dal progetto seL4. I componenti per CAmkES possono essere creati anche in Rust.
Rust rafforza la sicurezza della memoria in fase di compilazione attraverso il controllo dei riferimenti, la proprietà degli oggetti e il tracciamento della durata degli oggetti (ambiti) e valutando la correttezza degli accessi alla memoria in fase di esecuzione. Rust fornisce inoltre protezione contro gli overflow di numeri interi, richiede l'inizializzazione dei valori delle variabili prima dell'uso, utilizza il concetto di riferimenti e variabili immutabili per impostazione predefinita e offre una forte tipizzazione statica per ridurre al minimo gli errori logici.
Fonte: opennet.ru