Piattaforma
Costruito a partire dal compito.
L'applicazione si scrive in Rust. NoWayOS la costruisce sul microkernel seL4, insieme ai soli driver che usa. L'immagine che ne esce contiene questo, e nient'altro.
Dall'applicazione all'immagine
Un dispositivo NoWayOS si costruisce, non si configura. Quattro passaggi portano il codice fino a un dispositivo che svolge il suo unico compito, e ogni passaggio lascia qualcosa da verificare.
Scrivere l'applicazione
In Rust, come uno o più domini di protezione. Le schermate si costruiscono con il piccolo nucleo dichiarativo di interfaccia utente di NoWayOS, oppure si progettano in React e si convertono al momento della build con lo Screen Compiler.
Descrivere il sistema
Una descrizione di sistema Microkit dichiara ogni dominio di protezione, regione di memoria, canale e interrupt. Accanto, un file delle concessioni elenca tutto ciò che il sistema concede, e un file expect elenca ciò che il sistema deve stampare quando gira.
systems/hello.system systems/hello.grants systems/hello.expectCompilarlo
Nel container di sviluppo. La build verifica le concessioni rispetto alla descrizione, poi scrive l'immagine con la sua distinta base del software e un registro della sua configurazione seL4.
make image SYSTEM=helloAvviarlo, e lasciare che si verifichi da solo
Prima in QEMU: il sistema si avvia senza schermo e deve stampare, in ordine, ogni riga elencata nel suo file expect, e niente di ciò che il file vieta. Poi su Raspberry Pi 5, verificato con lo stesso file.
make qemu-test SYSTEM=hello
Compartimenti sigillati
Ogni parte di un sistema NoWayOS (lo schermo, l'input, la rete, l'applicazione) gira in un dominio di protezione tutto suo sul microkernel seL4. Un dominio di protezione ha la propria memoria e detiene solo le capability che la descrizione del sistema gli concede: una capability funziona come un badge che apre una sola porta. seL4 le fa rispettare, così una parte raggiunge solo ciò che le è stato dato, e tutto è progettato perché un bug in una parte resti in quella parte.
- Un supervisore riceve i guasti delle altre parti, ferma la parte guasta e riavvia il sistema in uno stato pulito. Se i guasti continuano, il dispositivo entra in uno stato fail-safe, e solo un avvio a freddo lo riporta in funzione.
- Un dominio di protezione watchdog rinfresca il watchdog hardware solo finché ogni altra parte risponde al suo heartbeat.
- I ruoli limitano ciò che può essere dato a ogni parte: la build rifiuta una concessione che il ruolo di una parte non deve mai avere, come un dispositivo per una parte che dovrebbe soltanto disegnare.
Messaggi tipizzati, copiati prima di essere controllati
I domini di protezione comunicano tramite record versionati di dimensione fissa, con un layout esplicito, che viaggiano su ring buffer a produttore singolo in memoria condivisa. Ogni record viene copiato fuori dalla memoria condivisa prima di essere controllato, così il mittente non può modificarlo tra il controllo e l'uso.
Ogni parser di input esterno è sottoposto a fuzzing e costruito per non andare mai in panic, e ogni decoder di messaggi ha dimostrazioni limitate, realizzate con il model checker Kani.
Uno schermo nativo, e nessun browser
L'interfaccia utente è un piccolo nucleo dichiarativo: layout, focus e hit-testing in memoria limitata, disegnati con la libreria Rust embedded-graphics, ridisegnando solo ciò che è cambiato. Il testo proviene da atlanti di glifi disegnati in anticipo, al momento della build, così il dispositivo non analizza mai un file di font. Le applicazioni vedono eventi di tasti, puntatore e tocco, mai USB né altri protocolli di dispositivo.
I designer possono continuare a lavorare in React. Lo Screen Compiler converte in Rust, al momento della build, le schermate scritte nel suo sottoinsieme supportato, e rifiuta tutto ciò che ne esce invece di approssimarlo.
Cosa c'è dentro
| Area | Cosa offre NoWayOS |
|---|---|
| Runtime | Pattern di domini di protezione su Microkit e rust-sel4; un supervisore che ferma una parte guasta e riavvia il sistema in uno stato pulito, con uno stato fail-safe dopo guasti ripetuti; un watchdog |
| Messaggi | Record tipizzati con un layout di trasmissione esplicito, e ring buffer a produttore singolo in memoria condivisa |
| Driver | Display (ramfb di QEMU, il framebuffer del Raspberry Pi 5); input (virtio, tastiere, mouse e tavolette USB); rete (virtio-net, l'Ethernet del Pi 5); host USB (xHCI); UART; timer; la ventola del Pi 5 |
| Rete | Uno stack IP su smoltcp con DHCP e TCP, che si connette solo alle destinazioni consentite da un sistema; un client TLS 1.3 su rustls e RustCrypto |
| Tempo e fiducia | Tempo monotono e ora di calendario come tipi che non si mescolano mai; verifica di firme ECDSA P-256; i record degli aggiornamenti firmati; seed da una sorgente hardware di numeri casuali sottoposta a test di integrità |
| Interfaccia utente | Un nucleo di interfaccia dichiarativo e limitato, con layout, focus e hit-testing; un renderer su embedded-graphics; atlanti di glifi e icone disegnati in anticipo |
| Strumenti | Il container di sviluppo; i frammenti make con cui si costruiscono i repository dei prodotti; i controlli su concessioni, unsafe, licenze e segreti; strumenti per SBOM e per le prove di release; runner per QEMU e Raspberry Pi |
Hardware
| Dove | Il suo ruolo |
|---|---|
| QEMU (AArch64) | Ogni sistema si avvia prima qui, dentro il container di sviluppo, e verifica il proprio output |
| Raspberry Pi 5 | La scheda di riferimento economica che chiunque può acquistare. L'interfaccia utente, l'input USB, i timer e il watchdog oggi girano su di essa |
| NXP i.MX8 | L'hardware di produzione previsto, con una radice di fiducia hardware. Non ancora supportato |
NoWayOS è sviluppato su macchine Apple silicon (arm64). Su x86-64 anche i pacchetti dell'immagine di sviluppo sono fissati e revisionati, ma l'immagine non è ancora stata costruita e testata lì da cima a fondo.
Le fondamenta
NoWayOS poggia sul lavoro di altri, e lo dichiara: seL4, Microkit, rust-sel4, le code di rete del seL4 Device Driver Framework, smoltcp, rustls, RustCrypto ed embedded-graphics.