Come si compone un sistema

Ogni dispositivo NoWayOS è un sistema: un insieme fisso di parti, dichiarato prima della build, ciascuna isolata dalle altre da seL4. Nulla viene aggiunto in fase di esecuzione. Questa pagina spiega i pezzi e come si collegano.

Domini di protezione

Un dominio di protezione è una parte di un sistema: un programma con la propria memoria, che detiene solo le capability che gli sono concesse. In seL4 una capability è 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 non può toccare nulla che le sue capability non indichino, e seL4 lo fa rispettare.

Un sistema tipico ha un dominio di protezione per ogni funzione: un driver del display, il percorso dell'input, lo stack di rete, l'interfaccia utente, l'applicazione, un timer, un supervisore e un watchdog. Ognuno è un piccolo programma Rust, no_std, che dopo l'avvio non alloca nulla.

La descrizione del sistema

La descrizione di sistema Microkit (systems/NAME.system, un file XML) dichiara l'intero sistema: ogni dominio di protezione con la sua priorità, il suo budget e il suo stack; ogni regione di memoria e chi la mappa; ogni canale; ogni interrupt.

• Le descrizioni indicano i dispositivi per nome, mai per indirizzo: phys_addr="@NAME". Gli indirizzi vengono dal file della scheda in platforms/, ciascuno con la sua fonte, così la stessa descrizione si compila per QEMU e per il Raspberry Pi 5.
• I canali collegano due domini di protezione, per le notifiche (segnali senza dati, tra cui gli interrupt) e le chiamate di procedura protette (chiamate sincrone verso una parte con priorità più alta).

La descrizione è il progetto di sicurezza del sistema, quindi ogni sua modifica viene revisionata come una modifica di sicurezza.

Il file delle concessioni

Accanto a ogni descrizione, systems/NAME.grants elenca tutto ciò che il sistema concede, un fatto per riga: priorità, budget, memoria, dispositivi, interrupt e canali. La build fallisce se i due non concordano, in un senso o nell'altro.

Ogni dominio di protezione ha anche un ruolo (ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock o test), e la build rifiuta una concessione che il suo ruolo non deve mai avere. A un'interfaccia utente non si può consegnare per errore un dispositivo di rete, e uno strumento di test non può infilarsi in un prodotto.

Messaggi tipizzati

I domini di protezione comunicano tramite messaggi tipizzati: record versionati di dimensione fissa, con un layout esplicito, che viaggiano su ring buffer a produttore singolo e consumatore singolo in memoria condivisa.

• Copia, poi verifica. Chi riceve copia ogni record fuori dalla memoria condivisa prima di convalidarlo, così il mittente non può modificarlo tra il controllo e l'uso (il bug noto come double-fetch).
• I decoder non possono andare in panic. Ogni decoder restituisce un errore tipizzato per qualsiasi input malformato, e ha dimostrazioni Kani limitate e un target di fuzzing.
• Ogni lato ha la propria vista. Il produttore e il consumatore vedono il ring attraverso viste di memoria separate, e gli indici condivisi usano l'ordinamento acquire e release.

Input

Le applicazioni vedono eventi di input canonici, tasti, movimenti del puntatore e tocchi, verificati rispetto allo schermo e limitati nella frequenza. Non vedono mai USB né altri protocolli di dispositivo; il percorso dell'input li analizza in domini di protezione propri, trattando ogni byte come ostile.

Guasti, il supervisore e lo stato fail-safe

Quando un dominio di protezione fa qualcosa che seL4 non consente, oppure va in panic, seL4 lo ferma e segnala un guasto al suo genitore.

• Il supervisore è il genitore delle altre parti. Riceve ogni guasto, lo segnala e resetta la scheda, così il sistema riparte in uno stato pulito. È costruito e testato nei sistemi di test in QEMU.
• Lo stato fail-safe è dove va un dispositivo quando i guasti continuano: per impostazione predefinita, al quarto riavvio dall'ultimo avvio a freddo, oppure al secondo guasto in una parte sensibile per la sicurezza, come l'archiviazione o gli aggiornamenti. Restano in funzione solo il supervisore, il watchdog e, dove possibile, il display, e solo un avvio a freddo, da dispositivo spento, riporta in funzione il dispositivo.
• Il dominio di protezione watchdog rinfresca il watchdog hardware solo finché ogni altra parte risponde al suo heartbeat. Se una smette di rispondere, l'hardware resetta la scheda.

Memoria e tempo

• La memoria è fissata quando si costruisce l'immagine. Il codice del dispositivo non alloca nulla: ogni buffer e ogni coda ha una dimensione stabilita, da nowayos-bounded. L'unica eccezione, il client TLS, lavora in un'arena fissa tutta sua.
• Due tipi di tempo che non si mescolano mai. Il tempo monotono conta dall'avvio e non va mai all'indietro; ogni timeout lo usa. L'ora di calendario, cioè la data e l'ora del giorno, viene da una fonte autenticata. Sono tipi Rust diversi, quindi non si può passare l'uno dove è previsto l'altro.

Costruire i propri sistemi

I sistemi e i domini di protezione di un prodotto vivono in un repository a parte, accanto a nowayos, mai al suo interno. Il Makefile di quel repository imposta SYSTEM_REPO := $(CURDIR) e include i frammenti make di NoWayOS:

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

A quel punto make image, make qemu-test, make qemu-test-all e i controlli funzionano sulle sue cartelle systems/ e pds/, con il container di sviluppo, i file delle schede, le regole sulle concessioni e i controlli di NoWayOS. Le variabili sono documentate in cima a tools/make/system.mk. Lo Showcase è costruito esattamente così.