Matematisk verifikation tester, om softwaren kører som annonceret

Når det kommer til sikkerhed, hvad du ikke ved kan skade dig.

De fleste mennesker tænker aldrig på den kryptering, der ligger til grund for sikre onlineaktiviteter, herunder bankvirksomhed, indkøb og kommunikation. Men alle er afhængige af computerprogrammer til at generere et tilfældigt tal, der fungerer som en nøgle til at låse op for krypteret kommunikation. Problemet er, at små programmeringsfejl kan gøre disse systemer sårbare, og disse sårbarheder kan ofte være meget svære at opdage.

"Når du opretter forbindelse til Amazon for at give dem dit kreditkortnummer, når du logger på et sted via en sikker forbindelse, du er afhængig af tilfældigt genererede kryptografiske nøgler, " sagde Andrew Appel, Eugene Higgins professor i datalogi ved Princeton. "Og hvis modstanderen, spionen, der forsøger at læse dine beskeder eller efterligne dig, kunne gætte hvilket tilfældigt tal din computer brugte, så kan den vide, hvilken nøgle du skal bruge, og den kan efterligne din trafik og læse dine beskeder."

Appels forskning har længe fokuseret på krydsfeltet mellem databehandling og offentlig politik. Han har skrevet meget om stemmemaskineteknologi og har vidnet for Kongressen om metoder til at sikre det amerikanske valgsystem. I det seneste arbejde, hans forskning har fokuseret på formel verifikation, et sæt værktøjer "til at specificere, hvad programmer skal gøre, til byggeprogrammer, der er i overensstemmelse med disse specifikationer, og for at verificere, at programmer opfører sig nøjagtigt som specificeret, "ifølge webstedet for DeepSpec, et multi-institution projekt, som Appel leder.

I et eksempel på matematisk kontrol af rigtigheden af ​​en kritisk funktion, Appels gruppe udviklede en metode til at verificere styrken af ​​tilfældige talgeneratorer, der danner grundlaget for de fleste krypteringssystemer. I et papir, der voksede fra Katherine Ye '16's seniorafhandling, holdet (som også omfattede forskere ved Johns Hopkins University og Oracle) undersøgte en almindeligt brugt tilfældig talgenerator og producerede et omfattende og maskintjekket bevis på, at systemet faktisk er sikkert. Konventionelle metoder såsom udtømmende test kan ikke fortælle, om en tilfældig talgenerator er sikker.

kommenterer arbejdet, Eugene Spafford, en leder inden for informationssikkerhed og forsikring ved Purdue University, sagde, at forskningen er et betydeligt fremskridt. "Som meget andet forskning, det gælder måske ikke direkte for dit liv og mit i øjeblikket, men det er ved at opbygge et sæt resultater, der kan [føre til] meget vigtige resultater i fremtiden."