13 novembre 2026
Attacchiamo la nostra build a ogni modifica
Un test di sicurezza che non può fallire non dimostra nulla. Per questo i test di NoWayOS arrivano con versioni costruite per fallire, e i suoi controlli stanno dove una pull request non può arrivare.
Ecco una domanda scomoda per qualsiasi test di sicurezza: è mai fallito? Un test che non è mai fallito potrebbe passare perché il sistema è solido, oppure perché il test non vede proprio nulla. Da fuori, le due cose sono identiche.
Perciò NoWayOS non si limita a testare la propria sicurezza. La attacca, a ogni modifica, e verifica che gli attacchi vengano fermati.
Allungare la mano su ciò che non è proprio
Ogni parte di un sistema NoWayOS gira nel proprio compartimento su seL4, con soltanto ciò che le è stato concesso. I test di isolamento mandano apposta delle sonde oltre quei confini. Una legge un indirizzo che non le è mai stato dato. Una scrive su una pagina che può soltanto leggere. Una, che ha esattamente ciò che ha l'interfaccia utente, prova a scrivere sulla pagina di controllo del display, che l'interfaccia può soltanto leggere. Un'altra, che ha esattamente ciò che ha il client di rete, prova a scrivere nella memoria del driver di rete.
seL4 deve fermarle tutte, e una parte estranea deve continuare a girare, intatta.
Un test costruito per fallire
Poi arriva il colpo di scena. Accanto al test di isolamento dell'interfaccia utente c'è una variante con una concessione allargata apposta: alla controfigura dell'interfaccia viene data la pagina privata del display. Il test di quella variante deve fallire. Se mai passasse, il test di isolamento sarebbe cieco, e la build lo direbbe.
La stessa idea attraversa il resto dei controlli. Ogni decoder dei messaggi tra le parti ha dimostrazioni limitate, dal model checker Kani, che non va mai in panic, in overflow né legge fuori dai limiti. I controlli a mutazione poi rompono deliberatamente i decoder, per mostrare che le dimostrazioni se ne accorgono. Ogni parser di input esterno è sottoposto a fuzzing con dati ostili.
Tutto questo fa parte di make ci, il controllo che ogni modifica deve superare. I test di isolamento girano ogni volta; una dimostrazione o una sessione di fuzzing viene ripetuta ogni volta che cambia il codice che copre.
Un test costruito per fallire
Il testLa sonda cerca di raggiungere una pagina che non le è mai stata concessa. seL4 la ferma, e il test passa.
La varianteUna concessione viene allargata apposta. La sonda passa, quindi questo test deve fallire. Se mai passasse, il primo test sarebbe cieco.
Controlli fuori portata
Un controllo è forte solo quanto la mano che può modificarlo. Perciò i controlli che ogni contributo a NoWayOS deve superare sono definiti in Defence Agent, un repository pubblico a sé. Una pull request che tocca un controllo viene segnalata al maintainer.
Defence Agent mette alla prova se stesso allo stesso modo: venti pull request truccate, ciascuna con dentro qualcosa che a un revisore potrebbe sfuggire. C'è testo nascosto da destra a sinistra in un commento, una lettera scambiata con la sua sosia cirillica, una dipendenza prelevata direttamente da un repository git, un workflow che eseguirebbe codice non attendibile. Ognuna deve essere scoperta, mentre tre vere modifiche del passato devono passare.
Prove, non aggettivi
Niente di tutto questo rende un dispositivo “inattaccabile”. Niente lo fa, e non lo diremo mai. Ciò che Le dà sono prove: una traccia di ciò che è stato tentato, di ciò che è stato fermato, e il comando che lo mostra. Legga le prove di un'immagine reale, oppure i controlli stessi.