Cosa può promettere una dimostrazione

Di solito ci si fida del software perché è stato testato. Qualcuno ha pensato ai modi in cui poteva andare storto, li ha provati e lo ha visto cavarsela. Funziona bene, fino al caso a cui nessuno aveva pensato.

Una dimostrazione parte dall'altro capo. Non prova dei casi. Mostra, con la matematica, che un'affermazione vale per tutti.

Tutti i casi, non solo quelli provati

Prendiamo una piccola promessa: questo codice non legge mai oltre la fine del suo buffer. Un test può dargli mille input, o un miliardo, e riferire che nessuno lo ha fatto sbagliare. Una dimostrazione dice una cosa di tipo diverso: non c'è input che lo faccia sbagliare. Non ne è stato trovato nessuno, e non ne esiste nessuno.

Il prezzo è il rigore. Una dimostrazione richiede un enunciato esatto di ciò che il codice deve fare, la sua specifica, e un argomento che colleghi a essa ogni riga del codice. Per il software reale quell'argomento è troppo lungo perché una persona lo controlli a occhio. Così lo controlla un computer.

Verificata a macchina

Ecco cosa significa “verificata a macchina”. La dimostrazione viene scritta per intero, in un linguaggio che un programma chiamato assistente di dimostrazione sa leggere, e il programma controlla ogni passaggio con le regole della logica. Non si stanca a pagina novecento, e non si fida della parola di nessuno.

Le dimostrazioni di seL4 sono verificate così, in un assistente di dimostrazione chiamato Isabelle/HOL. Sono pubbliche, e chiunque può rieseguirle.

Cosa dicono le dimostrazioni di seL4

seL4 è il kernel su cui gira ogni sistema NoWayOS: circa 10.000 righe di codice, e l'unico codice con il controllo totale del dispositivo. La dimensione è il punto. Un argomento su diecimila righe si può portare a termine. Uno su decine di milioni, non ancora.

La seL4 Foundation espone le dimostrazioni a strati:

• Il codice fa ciò che dice la specifica, e nulla di più. Ne segue un elenco di cose che il kernel non può fare: uscire da un buffer, seguire un puntatore nullo, perdere memoria, dividere per zero.
• Il programma che gira corrisponde al codice che è stato dimostrato. In mezzo c'è un compilatore, perciò un'ulteriore dimostrazione ne controlla l'output.
• Il kernel può tenere separate le parti di un sistema. Una parte non può modificare i dati di un'altra, né leggerli, né toglierle le risorse di cui ha bisogno, a meno che non le sia stato concesso il diritto di farlo.
• Un sistema può avviarsi nello stato per cui è stato progettato, con esattamente le concessioni che la sua descrizione elenca.

Non tutti gli strati sono completi per ogni processore e ogni configurazione. È importante, e ci torneremo.

Cosa dà per scontato una dimostrazione

Una dimostrazione è ampia esattamente quanto il suo enunciato, e poggia sulle sue assunzioni. seL4 mette le proprie per iscritto: che l'hardware si comporti come dice il suo modello, che poche centinaia di righe del codice di più basso livello siano corrette, che il codice eseguito prima dell'avvio del kernel abbia fatto il suo lavoro. La dimostrazione di riservatezza non copre i tempi di esecuzione.

Non dice nulla sul fatto che la specifica chieda la cosa giusta, e nulla sul software sopra il kernel. Un kernel dimostrato isolerà fedelmente un programma che contiene un bug. Il bug è ancora lì. Semplicemente non può raggiungere nient'altro.

Non è una debolezza delle dimostrazioni. È ciò che le rende preziose: dicono con precisione cosa coprono, e così Lei sa con precisione cosa resta.

Dove si trova NoWayOS

Ecco la posizione, senza giri di parole. NoWayOS gira su seL4, ma oggi nessuna immagine NoWayOS rientra nelle dimostrazioni completate di seL4. NoWayOS usa la configurazione a criticità mista di seL4, le cui dimostrazioni per i nostri processori sono in corso. E le dimostrazioni di seL4 non hanno mai coperto il codice proprio di NoWayOS. Perciò non diciamo che NoWayOS è “verificato formalmente”, e non lo diremo.

Ogni immagine dice a che punto è. Un file accanto a essa elenca la configurazione del suo kernel, opzione per opzione, a fronte di quella che seL4 ha dimostrato. Sicurezza ne mostra uno vero.

Dimostrazioni più piccole, le nostre

Il codice di NoWayOS ottiene la sua garanzia per un'altra via: Rust, isolamento, revisione, test e dimostrazioni di un tipo più modesto.

Ogni decoder dei messaggi che passano tra le parti di un sistema ha dimostrazioni limitate, realizzate con un model checker chiamato Kani. Una dimostrazione limitata copre ogni input fino a una dimensione dichiarata, qui il record più lungo che un decoder accetta. Entro quel limite è una dimostrazione vera: nessun input manda il decoder in panic, in overflow o a leggere fuori dai limiti. Oltre il limite non dice nulla, ed è per questo che il limite è l'input più lungo che esista.

Poi rompiamo i decoder di proposito, per assicurarci che le dimostrazioni se ne accorgano. Una dimostrazione che non può fallire non vale più di un test che non può fallire.

La sua misura onesta

Una dimostrazione non rende nulla “inattaccabile”. Rende vera un'affermazione, in tutti i casi, sotto assunzioni che Lei può leggere. Conosca l'affermazione e le assunzioni, e saprà che cosa ha in mano.

Ecco perché NoWayOS è costruito sul kernel che le ha, e perché Le dice, immagine per immagine, fin dove arrivano.