Le parole, spiegate semplicemente.

Un font disegnato in anticipo, al momento della build, sotto forma di immagini dei suoi caratteri, così un dispositivo può disegnare il testo senza mai analizzare un file di font.

Un dispositivo che dimostra a un servizio remoto, in modo crittografico, quale software ha avviato. Mostra cosa è stato caricato all'avvio, non tutto ciò che è accaduto dopo. Prevista per NoWayOS sull'hardware di produzione; non ancora costruita.

Un avvio da dispositivo spento, a differenza di un reset. Solo un avvio a freddo riporta un dispositivo NoWayOS fuori dal suo stato fail-safe.

Il secure boot: un dispositivo che si rifiuta di avviare software non firmato dal suo produttore. Previsto per NoWayOS sull'hardware di produzione; non ancora costruito.

In Microkit, una connessione dichiarata tra due domini di protezione, per le notifiche (segnali senza dati, tra cui gli interrupt) e le chiamate di procedura protette.

In seL4, un token non falsificabile che indica un oggetto del kernel e i diritti che si hanno su di esso, come un badge che apre una sola porta. Un dominio di protezione può toccare solo ciò che le sue capability indicano.

L'immagine container con le versioni fissate che contiene l'intera toolchain di NoWayOS: le toolchain Rust, l'SDK Microkit, QEMU e gli strumenti di controllo. Ogni target di make gira al suo interno, quindi alla propria macchina servono solo Podman e make (più Python 3.11 per pilotare un Raspberry Pi 5).

La regola per cui un messaggio viene copiato fuori dalla memoria condivisa prima di essere convalidato, così il mittente non può modificarlo tra il controllo e l'uso. Previene il double-fetch.

Un formato standard aperto per le distinte base del software. NoWayOS ne scrive una per ogni workspace e ogni immagine di sistema. Vedi SBOM.

L'adattatore da USB a seriale di Raspberry Pi. Sul connettore di debug del Raspberry Pi 5 trasporta il log di avvio e carica le immagini di test.

Il file XML di Microkit che dichiara ogni dominio di protezione, regione di memoria, canale e interrupt di un sistema. È il progetto di sicurezza del sistema, e ogni sua modifica viene revisionata come tale.

Una dimostrazione che una proprietà vale per ogni input fino a una dimensione dichiarata. NoWayOS dimostra così i suoi decoder di messaggi, con Kani.

Una parte isolata di un sistema Microkit: un programma con la propria memoria, che detiene solo le capability che gli sono concesse esplicitamente. I compartimenti sigillati di NoWayOS.

Un bug in cui il codice controlla dei dati in memoria condivisa e poi li rilegge, lasciando all'altra parte il tempo di modificarli nel frattempo. Lo previene la regola copia, poi verifica.

Una libreria Rust di grafica 2D per dispositivi senza uno stack grafico di sistema operativo. L'interfaccia utente di NoWayOS disegna con questa libreria.

Un errore come leggere oltre la fine di un buffer o usare memoria dopo averla liberata. Microsoft e Google hanno riferito, ciascuna per conto proprio, che circa il 70% dei loro bug di sicurezza gravi è di questo tipo; il Rust sicuro li esclude.

systems/NAME.grants: tutto ciò che un sistema concede, un fatto per riga: priorità, budget, memoria, dispositivi, interrupt e canali. La build fallisce se la descrizione del sistema e il file delle concessioni non concordano.

systems/NAME.expect: le righe che un sistema deve stampare, in ordine, e il testo che fa fallire il test se compare in qualsiasi punto. Lo stesso file verifica un sistema in QEMU e sul Raspberry Pi 5.

Mettere alla prova un parser con milioni di input generati, finché uno non lo manda in crash o non viola un controllo. Ogni parser di input esterno di NoWayOS ha un target di fuzzing.

Ciò che seL4 segnala quando un dominio di protezione fa qualcosa che il kernel non consente, oppure va in panic. La parte resta ferma finché il suo gestore dei guasti non interviene.

La famiglia di processori Arm industriali di NXP, e l'hardware di produzione previsto per NoWayOS. Non ancora supportata.

Un model checker per Rust che dimostra proprietà per ogni input fino a un limite. NoWayOS lo usa per dimostrare che i suoi decoder di messaggi non vanno mai in panic, in overflow né leggono fuori dai limiti.

La configurazione di seL4 con budget e periodi di scheduling, quella che Microkit compila. Le sue dimostrazioni per AArch64 sono in corso, quindi oggi nessuna immagine NoWayOS rientra nelle dimostrazioni completate di seL4.

Un record di dimensione fissa con un layout esplicito, passato tra domini di protezione attraverso la memoria condivisa e controllato alla ricezione. Vedi copia, poi verifica.

Un kernel ridotto al minimo indispensabile, con driver, rete e schermo che girano al di fuori di esso, ciascuno nel proprio compartimento. seL4 è un microkernel.

Il framework della seL4 Foundation per sistemi seL4 statici costruiti con domini di protezione dichiarati in una descrizione del sistema.

Un interprete per Rust che rileva i comportamenti indefiniti. NoWayOS lo esegue sui pochi crate autorizzati a contenere codice unsafe.

La data e l'ora del giorno, da una fonte autenticata. NoWayOS la tiene separata dal tempo monotono, come tipo distinto.

Un emulatore di macchine open source. Ogni sistema NoWayOS si avvia lì, e verifica il proprio output, prima di toccare l'hardware.

La scheda economica che NoWayOS usa come hardware di riferimento.

Un linguaggio di programmazione il cui codice sicuro esclude gli errori di sicurezza della memoria. Il codice di NoWayOS è interamente in Rust.

Il supporto Rust della seL4 Foundation, compreso il crate per scrivere domini di protezione Microkit.

Una libreria TLS scritta in Rust. Il client TLS 1.3 di NoWayOS è costruito su di essa, insieme a RustCrypto.

Una distinta base del software (software bill of materials): l'elenco di ogni componente e versione contenuti in un software. NoWayOS ne scrive una in formato CycloneDX per ogni workspace e ogni immagine di sistema.

Lo strumento di NoWayOS che, al momento della build, converte le schermate React scritte in TSX secondo un sottoinsieme supportato in Rust per l'interfaccia utente di NoWayOS. Rifiuta tutto ciò che esce dal sottoinsieme invece di approssimarlo.

Il seL4 Device Driver Framework: un progetto di riferimento per i driver su Microkit, basato su code in memoria condivisa. Le code di rete di NoWayOS lo seguono.

Un microkernel di circa 10.000 righe, mantenuto dalla seL4 Foundation, con dimostrazioni di correttezza e sicurezza verificate a macchina per configurazioni specifiche. NoWayOS gira su seL4.

Il registro scritto accanto a ogni immagine NoWayOS: la sua configurazione seL4, e se quella configurazione rientra nelle dimostrazioni completate di seL4.

Rendere più sicuro un dispositivo generalista modificandone le impostazioni. Le funzioni sono ancora lì, e un solo bug può aggirare ogni impostazione.

Realizzare un dispositivo che non può fare le cose rischiose perché non sono mai state incluse. L'approccio di NoWayOS.

Un sistema operativo costruito per l'unico compito di un dispositivo, invece di essere costruito per far girare qualsiasi cosa e poi bloccato su una sola. Tre caratteristiche lo definiscono: è costruito per un solo compito (la sua immagine contiene l'applicazione, i driver che usa e il kernel, e nient'altro); è sigillato all'interno (ogni parte nel proprio compartimento, con accesso solo a ciò che le è stato concesso); e mette le carte in tavola (le prove di ciò che contiene lo accompagnano). Non è una modalità kiosk, che blocca su un'unica app un sistema sicuro per configurazione. NoWayOS è un Single Purpose OS: un computer che non ha altro da fare.

Uno stack TCP/IP in Rust che non alloca memoria durante l'esecuzione. Lo stack di rete di NoWayOS è costruito su di esso.

Dove va un dispositivo NoWayOS quando i guasti continuano: restano in funzione solo il supervisore, il watchdog e, dove possibile, il display, fino a un avvio a freddo.

Tutto ciò che un attaccante potrebbe provare a usare contro un dispositivo: il suo codice, i servizi, le interfacce e gli input. Meno codice e meno funzioni ne lasciano di meno.

Il dominio di protezione che riceve i guasti delle altre parti, li segnala e riavvia il sistema in uno stato pulito.

Il tempo contato dall'avvio, mai impostato e mai all'indietro. Ogni timeout di NoWayOS lo usa, e non si mescola mai con l'ora di calendario.

Un sistema che cerca di raggiungere ciò che non gli è stato concesso, e che seL4 deve fermare. Una variante con una concessione allargata di proposito deve fallire, a dimostrazione che il test può fallire.

Tutto ciò che deve essere corretto perché una proprietà di sicurezza regga. Per un sistema NoWayOS: il kernel seL4, il loader e il monitor di Microkit e i domini di protezione su cui quella proprietà si basa.

Codice Rust di cui il compilatore non può verificare la sicurezza della memoria. Vietato in ogni crate di NoWayOS, tranne in un breve elenco revisionato che i controlli fanno rispettare.

Una dimostrazione matematica, controllata al computer, che un software rispetta la sua specifica. seL4 ce l'ha per configurazioni specifiche. Il codice di NoWayOS si affida invece a Rust, all'isolamento, ai test e alle dimostrazioni limitate.

Un timer hardware che resetta la scheda a meno che il software non lo rinfreschi. Il dominio di protezione watchdog di NoWayOS lo rinfresca solo finché ogni altra parte risponde al suo heartbeat.