Controlli e prove

Cosa esegue make ci e cosa mostra ogni controllo, le regole di base che ogni crate rispetta, come leggere il registro seL4 e la distinta base di un'immagine, e come il gate resta veloce.

NoWayOS fa poche affermazioni, e sostiene ognuna con un controllo che chiunque può eseguire. Questa pagina spiega cosa mostra ogni controllo, e cosa non mostra.

Un solo comando per tutto

make ci

make ci è l'intero gate, eseguito in ordine: la scansione dei segreti, i lint, i test, la documentazione, la demo, la build no_std, i controlli su licenze e avvisi di sicurezza, gli atlanti di glifi, le distinte base, il fuzzing e le dimostrazioni Kani, poi i controlli dei sistemi e gli avvii in QEMU. Una modifica passa solo se passano tutti i passaggi.

Cosa mostra ogni controllo

Comando	Cosa mostra
`make test`	Test unitari, di proprietà, della documentazione e su immagini di riferimento: il codice fa ciò che dicono i suoi test, e ogni schermata si disegna esattamente come approvata
`make lint`	rustfmt e clippy, con gli avvisi trattati come errori
`make nostd`	Ogni crate del dispositivo si compila per bare metal (`aarch64-unknown-none`), senza libreria standard
`make deny`	Le regole di base che ogni workspace deve rispettare, poi cargo-deny: licenze, sorgenti, crate vietati e avvisi di sicurezza noti
`make secrets`	L'albero dei sorgenti e ogni commit, analizzati offline alla ricerca di chiavi e credenziali
`make fuzz`	Ogni target di fuzzing, compilato con libFuzzer ed eseguito su input generati, per `FUZZ_SECONDS` (10 s) ciascuno
`make kani`	Le dimostrazioni limitate di Kani: che ogni decoder di record non vada mai in panic, in overflow né legga fuori dai limiti per qualsiasi input fino al record più lungo, con test di mutazione che mostrano che ogni dimostrazione può fallire
`make unsafe-audit`	Il codice `unsafe` compare solo dove l'elenco approvato lo consente
`make pds-miri`	Miri esegue i test dei crate autorizzati a contenere `unsafe`, cercando comportamenti indefiniti
`make sbom`	Una distinta base CycloneDX per ogni workspace
`make image-sbom SYSTEM=NAME`	Un'immagine e la sua distinta base: kernel, loader, monitor e ogni dominio di protezione, con i crate di ciascuno e i relativi hash
`make sel4-config-check`	La posizione di verifica seL4 registrata è quella dell'SDK Microkit fissato
`make qemu-test-all`	Ogni sistema si avvia in QEMU, in ogni configurazione che elenca, e stampa ciò che dice il suo file expect

Le dimostrazioni limitate valgono fino a una dimensione dichiarata dell'input, non per ogni input possibile. Il fuzzing trova i crash; non può dimostrare che non ce ne siano. I test mostrano i casi che testano. Ciascuno vale per ciò che effettivamente mostra.

Le regole di base che ogni crate rispetta

Sono lint e controlli in ogni workspace, non linee guida:

Niente unsafe, tranne che in un breve elenco approvato di crate e file che accedono direttamente all'hardware o alla memoria. Ogni aggiunta all'elenco richiede una motivazione dichiarata e una revisione.
Niente panic sull'input esterno: niente unwrap, expect o panic! nel codice di libreria, niente indicizzazione o aritmetica non controllate, e ogni eccezione a un lint ne dichiara il motivo.
I crate del dispositivo sono no_std e non allocano nulla. Le build di release mantengono i controlli di overflow, e un panic ferma la parte invece di lasciarla andare avanti.
I parser rifiutano l'input sovradimensionato prima di copiarlo, restituiscono errori tipizzati e hanno test di proprietà e un target di fuzzing.
Nessun segreto da nessuna parte, nemmeno chiavi di sviluppo. Le chiavi di test vengono create quando un test gira, e mai conservate.

Leggere i registri di un'immagine

Ogni immagine viene scritta in build/BOARD/SYSTEM/ con due registri accanto.

sel4-config.txt indica l'immagine, il suo hash, la scheda, l'SDK Microkit e il kernel, poi dice dove si colloca l'immagine rispetto alle dimostrazioni di seL4, con una riga status: per ogni motivo, ed elenca ogni opzione del kernel che lo determina accanto al valore della configurazione verificata. Un kernel di debug è una build di sviluppo. Un kernel multi-core o a criticità mista, o una scheda che non è nell'elenco di seL4, è fuori dalle dimostrazioni di seL4. Un kernel che corrisponde a ogni opzione non viene comunque mai definito “verificato”: il registro riporta i fatti e si ferma lì.

sbom.cdx.json è la distinta base del software CycloneDX dell'immagine: ciò di cui è fatta, fino a ogni crate di ogni dominio di protezione, ciascuno con il suo sha256.

Mantenere veloce il gate

L'insieme completo di dimostrazioni e fuzzing richiede molto tempo, quindi il make ci di tutti i giorni esegue Kani, fuzzing e Miri solo dove arriva una modifica. Segue la modifica attraverso ogni crate che ne dipende, e salta ogni controllo i cui input non sono cambiati dall'ultima volta che è passato. make ci CI_SCOPE=full li esegue tutti, senza nulla in cache; make kani, make fuzz e make pds-miri girano sempre per intero.

Kani è il passaggio più affamato: a ogni job di dimostrazione vengono assegnati circa 10 GB di memoria, e KANI_JOBS stabilisce quanti ne girano contemporaneamente. Se make kani esaurisce la memoria, assegnare più memoria alla macchina virtuale di Podman, oppure impostare KANI_JOBS=1.