È già abbastanza grave perdere un'ora di lavoro quando il computer si blocca, ma in contesti come l'assistenza sanitaria e l'aviazione, glitch del software possono avere conseguenze molto più gravi. In un caso noto, un bug informatico ha fatto sì che i malati di cancro ricevessero overdose letali da una macchina per radioterapia; in titoli più recenti, software difettoso è stato accusato di incidenti aerei in Etiopia e Indonesia.

Ora i ricercatori dello Stevens Institute of Technology, in collaborazione con l'Università di Yale, stanno sviluppando strumenti che potrebbero rendere molto meno probabili incidenti informatici catastrofici. Guidato da Eric Koskinen, un assistente professore di informatica alla Stevens, il lavoro non mira solo a garantire che i programmi funzionino correttamente in situazioni specifiche, ma utilizza anche algoritmi per determinare se è logicamente possibile, in qualsiasi circostanza, affinché il software produca risultati indesiderati.

"Quello a cui miriamo è una garanzia al 100% che non incontrerai mai un bug, ", ha detto Koskinen.

La squadra di Koskinen, sostenuto da oltre $ 2,5 milioni dall'Office of Naval Research, modella le differenze tra due versioni di un programma. È utile perché i programmatori spesso lavorano basandosi su software esistente, invece di scrivere codice da zero, e i bug possono essere introdotti da una versione all'altra. Questo approccio è particolarmente prezioso per i militari, poiché le agenzie di difesa acquistano spesso software da appaltatori privati, quindi apporta modifiche in-house prima di distribuirle in situazioni mission-critical.

"Hanno bisogno di un modo per confermare di aver apportato correttamente le modifiche all'interno dell'azienda, e non hanno introdotto nuovi problemi, " ha detto Koskinen.

Per dimostrare matematicamente che un programma per computer non potrebbe mai avere alcun tipo di bug, non importa quali circostanze, anticipato o inimmaginabile, Il team di Koskinen utilizza una strategia chiamata logica temporale. Piuttosto che esaminare le singole righe di codice per cercare differenze sintattiche, Il gruppo, compreso l'assistente professore Jun Xu, un esperto in analisi binaria presso Stevens, esamina come si comporta un programma nel tempo. L'idea è di dimostrare che non importa per quanto tempo il programma viene eseguito, non esiste un modo logico per restituire mai un risultato indesiderato.

Modellare la struttura e il comportamento di un programma, piuttosto che analizzare le singole righe di codice, è importante perché le stesse esatte righe di codice possono avere effetti diversi in contesti diversi, proprio come righe di codice che sembrano molto diverse possono ottenere la stessa cosa. È come studiare un documento legale, Koskinen spiega:cambiare una sola parola potrebbe sembrare banale, ma può cambiare l'intero significato del documento. La logica temporale aiuta a modellare il potenziale di un programma, acquisire informazioni approfondite sulle capacità del mondo reale del programma.

L'approccio del team consente inoltre di eliminare i bug nel software commerciale standard per il quale il codice sorgente non è disponibile. Senza il codice sorgente, il team è lasciato a confrontare i programmi per computer utilizzando la versione binaria del codice sorgente. "È difficile vedere se la vulnerabilità è stata davvero eliminata se non è possibile vedere il codice sorgente, " ha detto. "Le tecniche che stiamo costruendo lo faranno:se hai una versione del software di cui ti fidi, le nostre tecniche saranno in grado di aiutarti a individuare i cambiamenti (vulnerabilità negli aggiornamenti software o malware inserito in programmi eseguibili) e decidere se fidarti della nuova versione."

Il team di Koskinen sta anche sviluppando un toolkit che altri ricercatori e membri del pubblico potranno utilizzare per testare il software e stanno ampliando il loro approccio per lavorare con programmi più grandi e problemi più complessi. "Questi sono grandi problemi che affliggono i moderni sistemi informatici, " ha affermato Koskinen. "Questi problemi diventeranno solo più critici, in campi come la sanità, aviazione, veicoli autonomi, e molti altri ancora, quindi è fondamentale sviluppare tecniche pratiche per rendere i sistemi controllati dal computer privi di bug e sicuri da usare."