Als het om veiligheid gaat, wat je niet weet, kan je pijn doen.

De meeste mensen denken nooit na over de codering die ten grondslag ligt aan veilige online activiteiten, waaronder bankieren, winkelen en communicatie. Maar ze vertrouwen allemaal op computerprogramma's om een ​​willekeurig getal te genereren dat dient als sleutel om versleutelde communicatie te ontgrendelen. Het probleem is dat kleine programmeerfouten deze systemen kwetsbaar kunnen maken, en die kwetsbaarheden kunnen vaak erg moeilijk te detecteren zijn.

"Telkens wanneer je verbinding maakt met Amazon om ze je creditcardnummer te geven, wanneer je ergens inlogt via een beveiligde verbinding, je bent afhankelijk van willekeurig gegenereerde cryptografische sleutels, " zei Andrew Appel, de Eugene Higgins hoogleraar computerwetenschappen aan Princeton. "En als de tegenstander, de spion die uw berichten probeert te lezen of u probeert na te doen, kon raden welk willekeurig nummer uw computer gebruikte, dan zou het kunnen weten welke sleutel je gaat gebruiken en het zou je verkeer kunnen nabootsen en je berichten kunnen lezen."

Appels onderzoek heeft zich lange tijd gericht op het snijvlak van informatica en openbaar beleid. Hij heeft uitgebreid geschreven over stemmachinetechnologie en heeft voor het Congres getuigd over methoden om het Amerikaanse verkiezingssysteem te beveiligen. In het recente werk, zijn onderzoek heeft zich gericht op formele verificatie, een set tools "om te specificeren wat programma's moeten doen, voor het bouwen van programma's die voldoen aan die specificaties, en om te verifiëren dat programma's zich precies gedragen zoals gespecificeerd, " volgens de website van DeepSpec, een multi-institutioneel project dat Appel leidt.

In een voorbeeld van het wiskundig controleren van de juistheid van een kritieke functie, Appels groep ontwikkelde een methode om de sterkte te verifiëren van random number generators die de basis vormen van de meeste encryptiesystemen. In een paper dat voortkwam uit het afstudeerwerk van Katherine Ye '16, het team (waartoe ook onderzoekers van de Johns Hopkins University en Oracle behoorden) onderzocht een veelgebruikte generator voor willekeurige getallen en produceerde een uitgebreid en machinaal gecontroleerd bewijs dat het systeem inderdaad veilig is. Conventionele methoden zoals uitputtende tests kunnen niet zeggen of een generator van willekeurige getallen veilig is.

Commentaar op het werk, Eugene Spafford, een leider in informatiebeveiliging en assurance aan de Purdue University, zei dat het onderzoek een belangrijke vooruitgang is. “Net als veel ander onderzoek, het is op dit moment misschien niet direct van toepassing op jouw leven en het mijne, maar het bouwt een reeks resultaten op die in de toekomst tot zeer belangrijke resultaten kunnen leiden."