Verso il software incraccabile: la verifica formale

Tradurre il software in matematica e poi sottoporlo a prove specifiche per assicurarsi che non ci siano errori. Togliendo i bug si tolgono le armi ai criminali informatici e si rende il software più sicuro. Finora era un lavoro difficile, ma la DARPA ha dimostrato che oggi è possibile.

Avatar di Valerio Porcu

a cura di Valerio Porcu

Senior Editor

Alla DARPA sono riusciti a realizzare un software inattaccabile, o almeno questo è quanto si deduce dai recenti esperimenti eseguiti su un elicottero non pilotato - un drone chiamato Little Bird. I test sono iniziati nel 2015, quando a un team di hacker è stato chiesto di penetrare nei sistemi del Little Bird e prenderne il controllo.

Il primo tentativo ha avuto successo e gli assaltatori digitali hanno preso il controllo del mezzo. Come sempre ci sono riusciti scovando degli errori - bug - nel software e sfruttandoli per raggiungere l'obiettivo. Partendo da lì, i ricercatori della DARPA (Defence Advanced Research Projects Agency) si sono messi al lavoro per sviluppare un software più resistente, vale a dire privo di errori almeno nelle parti più sensibili. E pare che ci siano riusciti con la verifica formale - più o meno si tratta di tradurre il codice in linguaggio matematico e poi controllare se è corretto.

Il primo passo è stato dividere il software originale del Little Bird, che nasce "monolitico", e creare elementi a sé stanti che si potessero verificare separatamente. Infine il software così modificato e verificato è stato installato sul drone prodotto da Boeing.

Fisher Kathleen TuftsEng 615x410
Kathleen Fisher

Al Red Team, questo il nome del team incaricato di sviluppare un attacco, sono state date sei settimane di tempo con il drone, e un elevato livello di accesso ai suoi sistemi - molto più di quello che avrebbe un vero attaccante in un contesto reale.

Avevano per esempio accesso ai sistemi video, ma non a funzioni essenziali come i controlli di volo. Prima sarebbe bastato, ma al secondo tentativo non sono riusciti a superare le nuove difese di Little Bird. In altre parole non sono riusciti a uscire da quelle specifiche partizioni del software, e il veicolo è rimasto sicuro.

"Quel risultato ha fatto saltare tutti in piedi alla DARPA, per dire oddio, possiamo davvero usare questa tecnologia in sistemi importanti", ha commentato Kathleen Fisher, docente di informatica presso la Tufts University e coordinatrice del progetto HACMS (High-Assurance Cyber Military Systems).

La tecnica che ha reso possibile questo storico risultato è nota come verifica formale (Wikipedia in inglese); prevede che il software sia reinterpretato in linguaggio matematico e poi verificato con strumenti noti. "Un intero programma si può testare con la stessa certezza che i matematici usano per verificare i teoremi", scrive Kevin Harnett su Quanta Magazine.

ulb gallery lrg 03 960
Boeing Little Bird

"Scrivi una formula matematica che descrive il comportamento del programma e tramite l'uso di alcuni indicatori (proof checker) controllerà la correttezza del codice", spiega Bryan Parno, che si occupa di verifica formale per Microsoft Research.

Più facile a dirsi che a farsi, tant'è che l'idea esiste dalla metà degli anni '70. Più precisamente dal 1976, quando Edsger W. Dijkstra, pubblicò il libro A Discipline of Programming. Fino a oggi però si è ritenuto che non valesse la pena, che il gravoso lavoro necessario non avesse senso, e che fosse meglio fare un software con qualche bug e poi correggerlo strada facendo. Questo fino a che i computer erano isolati tra loro, e al massimo andava in crash il PC.

Dare una traduzione matematica a concetti come "proteggi la password" è piuttosto difficile, come ricorda ancora Parno. "Che cosa significa matematicamente? Definirlo potrebbe richiedere la stesura di una descrizione matematica su cosa significhi mantenere un segreto, o cosa significa che un algoritmo crittografico è sicuro", spiega il ricercatore di Microsoft.

Oggi però le cose sono cambiate: non solo per la sicurezza militare, di cui si occupa la DARPA, ma anche per tutti noi. Con la Rete Globale, c'è anche un rischio globale per i dati, da quelli personali alle transazioni bancarie, passando per la gestione delle infrastrutture e i mezzi di trasporto. Di pari passo, gli strumenti per la verifica formale del software si sono evoluti, e oggi è una strada decisamente più percorribile grazie anche a strumenti come Coq o Isabelle.

Poi arrivò Internet, che fece per gli errori di programmazione ciò che il viaggio aereo fece per la diffusione delle malattie infettive. Quando tutti i computer sono collegati gli uni agli altri, un bug fastidioso ma tollerabile può portare a problemi di sicurezza in cascata, continua Harnett.

La verifica formale è importante anche perché riduce o azzera la necessità di un test sul campo. Prendiamo le auto a guida autonoma: oggi serve metterle su strada per trovare bug grandi e piccoli, con test che possono durare anche anni. Con questo nuovo approccio, il software richiederebbe meno verifiche pratiche, e sarebbe intrinsecamente più corretto. Questo perché la verifica formale consente di eliminare un gran numero di possibili problemi, che sarebbero quasi impossibili da prevedere con la programmazione tradizionale. Ed è una cosa che oggi sembra più necessaria che mai.

"Ecco quello che non capiamo del tutto", commenta Andrew Appel, nome di rilievo nel campo della verifica formale e professore a Princeton, "Ci sono alcuni tipi di software che sono esposti a tutti gli hacker su Internet, quindi se c'è un bug in quel software potrebbe benissimo diventare una vulnerabilità di sicurezza".

Il problema è sotto gli occhi di tutti noi, visto che non passa giorno senza che ci sia almeno una notizia che parli di violazioni informatiche o altri problemi di sicurezza. Che sia necessario software più affidabile e più sicuro è un'ovvietà, mentre ancora non abbiamo un metodo per farlo davvero. Potremmo trovare una risposta nella verifica formale.