Sicurezza

Si fa gli affari suoi.

Un dispositivo NoWayOS lascia fuori ciò che non serve al suo compito e sigilla ciò che resta in compartimenti. Questa pagina spiega su cosa si fonda, cosa è dimostrato, cosa non lo è ancora e cosa spetta a chi lo adotta.

Cosa resta fuori

Un'immagine NoWayOS contiene la sua applicazione, i driver che quell'applicazione usa e il microkernel seL4. Non ci sono motore di browser, sistema a finestre, shell, gestore di pacchetti né account utente: nessuno è mai stato incluso, quindi nessuno è lì da sfruttare, correggere o configurare male. NoWayOS è progettato per ridurre software e servizi non necessari: se il compito non lo richiede, non è nell'immagine.

È questo il significato del nome: non c'è modo di sfruttare ciò che non è mai stato incluso. È un'affermazione su ciò che manca, non la promessa che niente possa andare storto. Ciò che è incluso può comunque avere bug; le affermazioni sono che ce n'è molto meno, e che un bug resta nel suo compartimento.

Bloccare un sistema generalista lo rende sicuro per configurazione: le funzioni messe sotto chiave sono ancora presenti, e un solo bug può aggirare ogni impostazione. NoWayOS punta a essere sicuro per costruzione: quelle funzioni non ci sono mai state.

Come si contiene un guasto

Ogni parte gira nel proprio dominio di protezione, con la propria memoria, e detiene solo le capability che la descrizione del sistema le concede. seL4 le fa rispettare.
Ogni concessione è elencata nel file delle concessioni del sistema, e la build fallisce se la descrizione concede qualcosa che il file non elenca, o viceversa. Allargare una concessione viene revisionato come una modifica di sicurezza.
I messaggi tra le parti sono record di dimensione fissa, copiati fuori dalla memoria condivisa prima di essere controllati, così un mittente non può modificare un record dopo che ha superato il controllo.
L'input è ostile finché non viene controllato. Ogni parser di input esterno è sottoposto a fuzzing e costruito per non andare mai in panic, e le applicazioni vedono eventi di tasti, puntatore e tocco, mai protocolli di dispositivo.
Un supervisore ferma una parte che va in guasto e riavvia il sistema in uno stato pulito. Guasti ripetuti portano il dispositivo in uno stato fail-safe fino a un avvio a freddo.

Cosa coprono le dimostrazioni di seL4, e cosa no

seL4 è un microkernel di circa 10.000 righe, con dimostrazioni di correttezza e sicurezza verificate a macchina. Le dimostrazioni sono un risultato raro, e valgono per configurazioni specifiche su piattaforme specifiche. Questa è la posizione esatta:

NoWayOS gira sul microkernel seL4, che ha dimostrazioni di correttezza e sicurezza verificate a macchina per configurazioni specifiche sul nostro hardware; NoWayOS usa la configurazione a criticità mista di seL4, le cui dimostrazioni sono in corso.

Piattaforma: la configurazione verificata AArch64 di seL4 elenca il Raspberry Pi 5 e gli i.MX8M Mini, Plus e Quad di NXP.
Scheduling: Microkit compila il kernel a criticità mista (MCS) di seL4, le cui dimostrazioni per AArch64 sono in corso. Quindi oggi nessuna immagine NoWayOS rientra nelle dimostrazioni completate di seL4.
Core: le dimostrazioni riguardano kernel single-core. Un'immagine che usa più core ne resta fuori, e lo dichiara.
Sopra il kernel: gli strumenti di Microkit e i domini di protezione e i driver di NoWayOS non sono coperti dalle dimostrazioni di seL4. La loro affidabilità si fonda su Rust, sull'isolamento, sulla revisione, sui test e sulle dimostrazioni limitate di NoWayOS stesso.

Ogni immagine registra la sua configurazione in un sel4-config.txt accanto a sé. Ecco cosa dice di sé il registro di una build di sviluppo del sistema hello:

system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list

Anche un'immagine il cui kernel corrispondesse a ogni opzione della configurazione verificata non verrebbe definita “verificata”, qui. Il registro riporta i fatti, e i fatti bastano.

Le prove, e il comando per ciascuna

Ogni affermazione di questa pagina è accompagnata dalle sue prove, e ogni prova nasce da un comando che chiunque può eseguire nel container di sviluppo. make ci li esegue in ordine, e make ci CI_SCOPE=full esegue ogni dimostrazione e ogni target di fuzzing; Controlli e prove li spiega uno per uno.

L'affermazione	La prova	Il comando
Ogni concessione è messa per iscritto.	Il file delle concessioni di ogni sistema, verificato rispetto alla descrizione del sistema a ogni build.	`make qemu-test SYSTEM=hello`
Una parte non può raggiungere ciò che non le è stato concesso.	Test di isolamento le cui sonde tentano letture e scritture non concesse, che seL4 deve fermare, e una variante con una concessione allargata di proposito, che deve fallire.	`make qemu-test SYSTEM=isolation-test`
I decoder di messaggi reggono per ogni input fino a un limite.	Dimostrazioni Kani per ogni decoder di record di messaggi, con test di mutazione che mostrano che le dimostrazioni possono fallire.	`make kani`
I parser di input esterno resistono a input ostili.	Un target di fuzzing per ogni parser di input non attendibile. Un crash, una volta corretto, diventa un test di regressione.	`make fuzz`
Il codice unsafe sta solo dove è approvato.	Un elenco dei pochi crate e file autorizzati a usarlo, fatto rispettare da make ci, con Miri eseguito su quei crate.	`make unsafe-audit`
Ogni componente è noto.	Una distinta base del software CycloneDX per ogni workspace e ogni immagine di sistema, ciascun componente con il suo hash.	`make image-sbom SYSTEM=hello`
Licenze e avvisi di sicurezza sono verificati.	cargo-deny su ogni workspace: licenze, sorgenti, crate vietati e avvisi di sicurezza noti.	`make deny`
Nel codice non ci sono segreti.	L'albero dei sorgenti e ogni commit analizzati, offline, alla ricerca di chiavi e credenziali.	`make secrets`
La configurazione seL4 di ogni immagine è registrata.	Un sel4-config.txt accanto a ogni immagine, e un controllo che i valori di riferimento del registro corrispondano all'SDK Microkit fissato.	`make sel4-config-check`

Le prove di un'immagine

Non serve costruire nulla per vedere come sono fatte le prove. Eccole tutte, per un'immagine reale: ui-interactive, l'interfaccia utente cliccabile, compilata per QEMU il 1° novembre 2026.

La sua distinta base del software (CycloneDX 1.5): 62 parti, dal kernel seL4 e dal loader di Microkit a ogni crate di ogni dominio di protezione, ciascuna con il suo SHA-256.
Il registro della sua configurazione seL4: il kernel che esegue, opzione per opzione rispetto alla configurazione verificata di seL4, e senza giri di parole dove resta fuori dalle dimostrazioni.
La sua descrizione di sistema: ogni dominio di protezione, regione di memoria, interrupt e canale, così come li costruisce Microkit.
Il suo file delle concessioni: le stesse concessioni messe per iscritto, un fatto per riga, che la build verifica rispetto alla descrizione.
La schermata che disegna, confrontata pixel per pixel con questa immagine approvata ogni volta che il suo test viene eseguito.

Cosa resta a carico di chi lo adotta

NoWayOS è una piattaforma, non un prodotto certificato. Un dispositivo sicuro dipende anche da come viene messo in servizio e gestito, e quella parte spetta a chi lo costruisce e lo gestisce.

Sicurezza fisica. Una periferica collegata o una mano sul cavo di alimentazione possono comunque mettere fuori servizio un dispositivo. Involucri, porte e alimentazione fanno parte del progetto del prodotto costruito su NoWayOS.
Cosa concede ogni sistema. NoWayOS verifica che un sistema e il suo file delle concessioni concordino. Se quelle concessioni siano giuste per il compito è una decisione di progetto, e come tale va revisionata.
Reti e back end. Un dispositivo si connette solo alle destinazioni che il suo sistema consente. Proteggere ciò che quei servizi fanno con quanto ricevono spetta a loro.
Chiavi e aggiornamenti. Gli aggiornamenti firmati, con ritorno sicuro alla versione precedente, sono progettati ma non ancora costruiti. Chi detiene le chiavi di firma, e come viene approvata una release, è una decisione operativa.
Certificazione. I prodotti regolamentati che girano su NoWayOS hanno una certificazione propria. NoWayOS è progettato per fornire le prove di cui hanno bisogno; non è certificato in sé.

Non ancora costruito

Avvio sicuro e attestazione spettano all'hardware di produzione, con una radice di fiducia hardware. Nessuno dei due è stato costruito.
Aggiornamenti firmati applicati sul dispositivo. I record degli aggiornamenti e i relativi controlli esistono; il percorso che applica un aggiornamento su un dispositivo non ancora.
Il Raspberry Pi 5 è una scheda di sviluppo, non un dispositivo irrobustito. Chi ne ha uno in mano può sostituirne il software, e su di esso l'accesso alla memoria dei dispositivi USB non è ancora confinato.

Parole che qui non troverà

Non definiamo NoWayOS “inattaccabile”, “a prova di manomissione” o “a prova di bomba”, e non parliamo di “superficie di attacco zero”. Niente lo è, e se lo facessimo farebbe bene a smettere di leggere. Le affermazioni di questa pagina sono più modeste, e ognuna è accompagnata dalle sue prove.

Segnalare una vulnerabilità

Si prega di segnalare le vulnerabilità in privato, tramite la segnalazione privata delle vulnerabilità di GitHub nella scheda Security del repository o via email a security@nowayos.com, come descritto nel SECURITY.md di ogni repository, e non in una issue pubblica. Poiché ogni parte gira nel proprio compartimento, tutto è progettato perché una falla resti dov'è mentre si prepara una correzione.