När det kommer till säkerhet, det du inte vet kan skada dig.

De flesta människor tänker aldrig på krypteringen som ligger till grund för säkra onlineaktiviteter inklusive bankverksamhet, shopping och kommunikation. Men alla förlitar sig på datorprogram för att generera ett slumptal som fungerar som en nyckel för att låsa upp krypterad kommunikation. Problemet är att små programmeringsfel kan göra dessa system sårbara, och dessa sårbarheter kan ofta vara mycket svåra att upptäcka.

"När du ansluter till Amazon för att ge dem ditt kreditkortsnummer, när du loggar in någonstans via en säker anslutning, du är beroende av slumpmässigt genererade kryptografiska nycklar, sa Andrew Appel, Eugene Higgins professor i datavetenskap vid Princeton. "Och om motståndaren, spionen som försöker läsa dina meddelanden eller imitera dig, kunde gissa vilket slumptal din dator använde, då kan den veta vilken nyckel du kommer att använda och den kan imitera din trafik och läsa dina meddelanden."

Appels forskning har länge fokuserat på skärningspunkten mellan databehandling och offentlig politik. Han har skrivit mycket om röstmaskinsteknik och har vittnat inför kongressen om metoder för att säkra det amerikanska valsystemet. I det senaste arbetet, hans forskning har fokuserat på formell verifiering, en uppsättning verktyg "för att specificera vad program ska göra, för att bygga program som överensstämmer med dessa specifikationer, och för att verifiera att program fungerar exakt som specificerat, " enligt webbplatsen för DeepSpec, ett flerinstitutionellt projekt som Appel leder.

I ett exempel på att matematiskt kontrollerar korrektheten av en kritisk funktion, Appels grupp utvecklade en metod för att verifiera styrkan hos slumptalsgeneratorer som ligger till grund för de flesta krypteringssystem. I en artikel som växte fram från Katherine Ye '16s senioravhandlingsarbete, teamet (som även inkluderade forskare vid Johns Hopkins University och Oracle) undersökte en vanligt förekommande slumptalsgenerator och tog fram ett omfattande och maskinkontrollerat bevis på att systemet verkligen är säkert. Konventionella metoder som uttömmande tester kan inte avgöra om en slumpgenerator är säker.

Kommenterar arbetet, Eugene Spafford, en ledare inom informationssäkerhet och försäkran vid Purdue University, sa att forskningen är ett betydande framsteg. "Som mycket annan forskning, det kanske inte direkt gäller ditt och mitt liv för tillfället, men det bygger upp en uppsättning resultat som kan [leda till] mycket viktiga resultat i framtiden."