En matière de sécurité, ce que vous ne savez pas peut vous blesser.

La plupart des gens ne pensent jamais au cryptage qui sous-tend les activités en ligne sécurisées, notamment les opérations bancaires, achats et communication. Mais tous s'appuient sur des programmes informatiques pour générer un nombre aléatoire qui sert de clé pour déverrouiller la communication cryptée. Le problème est que de petites erreurs de programmation peuvent rendre ces systèmes vulnérables, et ces vulnérabilités peuvent souvent être très difficiles à détecter.

"Chaque fois que vous vous connectez à Amazon pour leur donner votre numéro de carte de crédit, chaque fois que vous vous connectez quelque part via une connexion sécurisée, vous dépendez de clés cryptographiques générées aléatoirement, " a déclaré Andrew Appel, le professeur Eugene Higgins d'informatique à Princeton. « Et si l'adversaire, l'espion qui essaie de lire vos messages ou de vous faire passer pour, pourrait deviner quel nombre aléatoire votre ordinateur utilisait, alors il pourrait savoir quelle clé vous allez utiliser et il pourrait usurper l'identité de votre trafic et lire vos messages."

Les recherches d'Appel se concentrent depuis longtemps sur l'intersection de l'informatique et des politiques publiques. Il a beaucoup écrit sur la technologie des machines à voter et a témoigné devant le Congrès sur les méthodes de sécurisation du système électoral américain. Dans des travaux récents, ses recherches ont porté sur la vérification formelle, un ensemble d'outils "pour spécifier ce que les programmes doivent faire, pour les programmes de construction conformes à ces spécifications, et pour vérifier que les programmes se comportent exactement comme spécifié, " selon le site de DeepSpec, un projet multi-institutionnel que mène Appel.

Dans un exemple de vérification mathématique de l'exactitude d'une fonction critique, Le groupe d'Appel a développé une méthode pour vérifier la force des générateurs de nombres aléatoires qui constituent la base de la plupart des systèmes de cryptage. Dans un article issu du travail de thèse senior de Katherine Ye '16, l'équipe (qui comprenait également des chercheurs de l'Université Johns Hopkins et d'Oracle) a examiné un générateur de nombres aléatoires couramment utilisé et a produit une preuve complète et vérifiée par machine que le système est effectivement sécurisé. Les méthodes conventionnelles telles que les tests exhaustifs ne peuvent pas dire si un générateur de nombres aléatoires est sécurisé.

Commentant le travail, Eugène Spafford, un leader de la sécurité et de l'assurance de l'information à l'Université Purdue, dit que la recherche est une avancée significative. "Comme beaucoup d'autres recherches, cela peut ne pas s'appliquer directement à votre vie et à la mienne en ce moment, mais cela crée un ensemble de résultats qui pourraient [conduire à] des résultats très importants à l'avenir."