Google annuncia un nuovo sistema operativo: si chiama KataOS ed è matematicamente sicuro

Google ha annunciato un nuovo sistema operativo: si chiama KataOS ed è pensato per i sistemi embedded. Si basa sul microkernel seL4 e usa Rust come linguaggio di programmazione. Proprio questi due elementi lo rendono un sistema operativo particolarmente interessante, dato che ne aumentano significativamente il livello di sicurezza offerto.

Google annuncia KataOS per offrire un sistema operativo sicuro

seL4 è un microkernel focalizzato sulla sicurezza. Il kernel è quella parte del sistema operativo che fa da supervisore dei processi e mette a disposizione dei programmi le primitive per interfacciarsi con l'hardware; un microkernel è una versione particolare di un kernel che delega molte funzioni a programmi "normali" così da aumentare il livello di sicurezza e da rendere tali funzioni più facili da gestire in caso di crash (dato che un malfunzionamento non porta al blocco dell'intero sistema).

seL4 si differenzia dalla maggior parte degli altri kernel disponibili per via del fatto che è stato sviluppato per essere sicuro, e tale sicurezza è certificata attraverso dimostrazioni matematiche. Scrive Google sul suo blog che "KataOS fornisce una piattaforma che è sicura (ed è verificabile come tale) che protegge la privacy dell'utente perché è logicamente impossibile per le applicazioni fare breccia nelle protezioni hardware di sicurezza del kernel e le componenti del sistema sono verificabili come sicure. KataOS è anche implementato quasi integralmente in Rust, il che fornisce un forte punto di partenza per la sicurezza del software, dato che elimina intere classi di bug, come gli errori 'off-by-one' [in cui un ciclo viene eseguito una volta in più o in meno, ad esempio; NdR] e i buffer overflow."

Rust è un linguaggio di programmazione creato da Mozilla che punta proprio alla correttezza e all'eliminazione dei problemi che nascono in linguaggi come il C quali gli errori di puntamento, le allocazioni errate di memoria e così via; in altri termini, è un linguaggio che elimina alla radice tutta una serie di possibili bug e problemi che emergono normalmente ed è quindi considerato più sicuro rispetto ai linguaggi "tradizionali".

Google intende usare KataOS come sistema operativo per i dispositivi embedded, ma non è noto in che forma e per quali dispositivi nello specifico: Fuchsia, un altro progetto dell'azienda, è infatti già usato in alcuni dispositivi che potremmo definire "embedded" come il Nest Hub. Google parla di "machine learning ambientale" come ambito di applicazione, cosa che fa pensare a oggetti come altoparlanti intelligenti e simili in grado di eseguire operazioni di apprendimento a partire dall'ambiente circostante.

KataOS è pensato per essere eseguito su processori RISC-V e Google sta preparando il rilascio della documentazione e dei sorgenti dell'intero progetto (hardware incluso), chiamato Sparrow ("passero"), affinché sia possibile verificarne la sicurezza.