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 \u00e8 fornita una prova matematica di affidabilit\u00e0, che dimostra la completa conformit\u00e0 del codice alle specifiche fornite in linguaggio formale. Il codice del progetto \u00e8 aperto sotto licenza Apache 2.0. <\/p>\n
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 \u00e8 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. <\/p>\n
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\u00e0 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. <\/p>\n
L'architettura seL4 \u00e8 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 \u00e8 organizzato attraverso la definizione di regole. <\/p>\n
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 \u00e8 stato utilizzato l'ambiente di sviluppo CAmkES, sviluppato dal progetto seL4. I componenti per CAmkES possono anche essere creati in linguaggio Rust. <\/p>\n