Google ha annunciato l'apertura di progetti legati a KataOS, un sistema operativo sicuro progettato per dispositivi embedded. I componenti di sistema di KataOS sono scritti in Rust e vengono eseguiti su un microkernel seL4, per il quale sono state fornite prove matematiche di affidabilità sui sistemi RISC-V, che attestano la completa conformità del codice alle specifiche definite in un linguaggio formale. Il codice del progetto è aperto sotto licenza Apache 2.0.
Il sistema supporta piattaforme basate su architetture RISC-V e ARM64. Per simulare il funzionamento di seL4 e dell'ambiente KataOS sopra l'hardware durante il processo di sviluppo, viene utilizzato il framework Renode. Come implementazione di riferimento, è proposto un complesso software e hardware chiamato Sparrow, che combina KataOS con chip sicuri basati sulla piattaforma OpenTitan. La soluzione proposta consente di unire un kernel di 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 di KataOS, in futuro è previsto l'apertura di tutti gli altri componenti di Sparrow, compresi quelli hardware.
La piattaforma si sviluppa tenendo conto dell'uso in chip specializzati, progettati per eseguire applicazioni per l'apprendimento automatico e l'elaborazione di informazioni riservate, che richiedono un particolare livello di protezione e conferma dell'assenza di malfunzionamenti. Un esempio di tali applicazioni è rappresentato da sistemi che manipolano le immagini delle persone e le registrazioni vocali. L'uso di KataOS per la verifica dell'affidabilità garantisce che, in caso di guasto in una parte del sistema, tale guasto non si propaghi al resto del sistema e, in particolare, al nucleo e alle parti critiche.
L'architettura seL4 è notevole per l'estrazione delle parti di gestione delle risorse del nucleo nell'area utente e per l'applicazione agli stessi risorse degli stessi strumenti di accesso impiegati per le risorse utente. Il microkernel non offre astrazioni di alto livello pronte per la gestione di file, processi, connessioni di rete, ecc.; al contrario, fornisce solo meccanismi minimi per gestire l'accesso allo spazio fisico degli indirizzi, alle interruzioni e alle risorse della CPU. Le astrazioni di alto livello e i driver per interagire con l'hardware vengono implementati separatamente sopra il microkernel sotto forma di attività eseguite a livello utente. L'accesso a queste risorse da parte delle attività che operano a livello utente è organizzato attraverso la definizione di regole.
Per una maggiore sicurezza, tutti i componenti, ad eccezione del microkernel, sono inizialmente sviluppati in Rust utilizzando pratiche di programmazione sicure che minimizzano gli errori di gestione della memoria, evitando problemi come l'accesso alla memoria dopo la sua liberazione, dereferenziazione di puntatori nulli e overflow del buffer. In Rust sono scritti anche il caricatore delle applicazioni nell'ambiente seL4, i servizi di sistema, il framework per lo sviluppo di applicazioni, l'API per l'accesso alle chiamate di sistema, il gestore dei processi, il meccanismo di allocazione dinamica della memoria, e così via. Per la build verificata è stato utilizzato lo strumento CAmkES, sviluppato dal progetto seL4. I componenti per CAmkES possono essere creati anche in Rust.
La gestione sicura della memoria in Rust avviene durante la fase di compilazione attraverso la verifica dei riferimenti, il monitoraggio della proprietà degli oggetti e la gestione della durata di vita degli oggetti (scope), nonché attraverso la valutazione della correttezza dell'accesso alla memoria durante l'esecuzione del codice. Rust offre anche strumenti per proteggere contro il overflow intero, richiede l'inizializzazione obbligatoria delle variabili prima del loro utilizzo, applica il concetto di immutabilità (immutable) per riferimenti e variabili per impostazione predefinita, e propone un forte sistema di tipi statici per minimizzare gli errori logici.
Fonte: opennet.ru
