L'azienda Google ha annunciato l'apertura dei risultati legati al progetto KataOS, mirato a creare un sistema operativo sicuro per apparecchiature incorporate. I componenti di sistema di KataOS sono scritti in linguaggio Rust e vengono eseguiti su un microkernel seL4, per il quale sui sistemi RISC-V è fornita una prova matematica di affidabilità, che dimostra la completa conformità del codice alle specifiche fornite in linguaggio formale. Il codice del progetto è aperto sotto licenza Apache 2.0.
Il sistema supporta piattaforme basate sulle architetture RISC-V e ARM64. Per simulare il funzionamento di seL4 e dell'ambiente KataOS su hardware durante il processo di sviluppo viene utilizzato il framework Renode. Come implementazione di riferimento è stato proposto un complesso software-hardware chiamato Sparrow, che combina KataOS con chip protetti basati sulla piattaforma OpenTitan. La soluzione proposta consente di combinare 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 si prevede di rendere pubblici anche tutti gli altri componenti di Sparrow, comprese le parti hardware.
La piattaforma si sviluppa con un occhio all'applicazione in chip specializzati, destinati a eseguire applicazioni per l'apprendimento automatico e la gestione di informazioni riservate, che richiedono un livello particolare di protezione e conferma dell'assenza di guasti. Come esempio di tali applicazioni si citano i sistemi che manipolano immagini di persone e registrazioni vocali. L'uso della verifica di affidabilità in KataOS garantisce che, in caso di guasto in una parte del sistema, tale guasto non si diffonda al resto del sistema e, in particolare, al kernel e alle parti critiche.
L'architettura seL4 è notevole per l'estrazione di parti per la gestione delle risorse del nucleo nello spazio utente e per l'applicazione per tali risorse degli stessi strumenti di accesso che si utilizzano per le risorse utente. Il microkernel non fornisce astrazioni ad alto livello pronte per la gestione di file, processi, connessioni di rete, ecc., ma offre solo meccanismi minimi per gestire l'accesso allo spazio di indirizzamento fisico, alle interruzioni e alle risorse della CPU. Le astrazioni ad alto livello e i driver per l'interazione con l'hardware vengono implementati separatamente sopra il microkernel sotto forma di task eseguiti a livello utente. L'accesso a queste risorse da parte delle task è organizzato attraverso la definizione di regole.
Per una protezione aggiuntiva, tutti i componenti, tranne il microkernel, vengono sviluppati inizialmente in linguaggio Rust utilizzando pratiche di programmazione sicure che minimizzano gli errori nella gestione della memoria, causando problemi come l'accesso a una zona di memoria dopo la sua liberazione, la dereferenziazione di puntatori nulli e l'overflow del buffer. In Rust sono scritti anche il caricatore di 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 di processi, il meccanismo di allocazione dinamica della memoria, ecc. Per la build verificata è stato utilizzato l'ambiente di sviluppo CAmkES, sviluppato dal progetto seL4. I componenti per CAmkES possono anche essere creati in linguaggio Rust.
La gestione sicura della memoria viene garantita in Rust durante la compilazione attraverso il controllo dei riferimenti, il tracciamento della proprietà degli oggetti e la gestione del ciclo di vita degli oggetti (scope), nonché attraverso la valutazione della correttezza dell'accesso alla memoria durante l'esecuzione del codice. Rust fornisce anche strumenti per proteggere da overflow interi, richiede l'inizializzazione obbligatoria dei valori delle variabili prima dell'uso, applica il concetto di immutabilità (immutable) dei riferimenti e delle variabili per impostazione predefinita e offre una forte tipizzazione statica per minimizzare gli errori logici.
Fonte: opennet.ru
