Quando si tratta di sicurezza, quello che non sai può farti del male.

La maggior parte delle persone non pensa mai alla crittografia che sta alla base delle attività online sicure, inclusi servizi bancari, acquisti e comunicazioni. Ma tutti si affidano a programmi per computer per generare un numero casuale che funge da chiave per sbloccare la comunicazione crittografata. Il problema è che piccoli errori di programmazione possono rendere vulnerabili questi sistemi, e tali vulnerabilità possono spesso essere molto difficili da rilevare.

"Ogni volta che ti connetti ad Amazon per fornire loro il numero della tua carta di credito, ogni volta che accedi da qualche parte tramite una connessione sicura, dipendi da chiavi crittografiche generate casualmente, " ha detto Andrew Appel, l'Eugene Higgins Professore di Informatica a Princeton. "E se l'avversario, la spia che sta cercando di leggere i tuoi messaggi o di impersonarti, potrebbe indovinare quale numero casuale stava usando il tuo computer, quindi potrebbe sapere quale chiave utilizzerai e potrebbe impersonare il tuo traffico e leggere i tuoi messaggi."

La ricerca di Appel si è a lungo concentrata sull'intersezione tra informatica e politica pubblica. Ha scritto molto sulla tecnologia delle macchine per il voto e ha testimoniato davanti al Congresso sui metodi per garantire il sistema elettorale degli Stati Uniti. In lavori recenti, la sua ricerca si è concentrata sulla verifica formale, un insieme di strumenti "per specificare cosa dovrebbero fare i programmi, per la creazione di programmi conformi a tali specifiche, e per verificare che i programmi si comportino esattamente come specificato, " secondo il sito web di DeepSpec, un progetto multi-istituzionale guidato da Appel.

In un esempio di verifica matematica della correttezza di una funzione critica, Il gruppo di Appel ha sviluppato un metodo per verificare la forza dei generatori di numeri casuali che costituiscono la base della maggior parte dei sistemi di crittografia. In un documento che è nato dal lavoro di tesi senior di Katherine Ye '16, il team (che comprendeva anche ricercatori della Johns Hopkins University e Oracle) ha esaminato un generatore di numeri casuali comunemente usato e ha prodotto una prova completa e controllata dalla macchina che il sistema è davvero sicuro. I metodi convenzionali come il test esaustivo non possono dire se un generatore di numeri casuali è sicuro.

Commentando il lavoro, Eugene Spafford, leader nella sicurezza e assicurazione delle informazioni presso la Purdue University, ha detto che la ricerca è un progresso significativo. "Come molte altre ricerche, potrebbe non applicarsi direttamente alla tua vita e alla mia in questo momento, ma sta costruendo una serie di risultati che potrebbero [portare] a risultati molto importanti in futuro".