Formal Methods and Real-World Cryptographic Protocols: Advancing the Verification and Testing Frontiers for Specifications and Implementations

Les protocoles cryptographiques sont les garants de nos échanges numériques sécurisés, piliers technologiques de notre société de l’information. L’histoire répétée d’attaques exploitant les erreurs de conception et d’implémentation de ces protocoles n’a de cesse de démontrer leur fragilité. Ce manuscrit aborde un défi central de la sécurité informatique : comment obtenir de meilleures garanties pour les protocoles cryptographiques ?

Premièrement, nous présentons des avancées fondamentales en méthodes formelles, introduisant de nouvelles techniques de modélisation, des algorithmes de vérification et des méthodologies de preuve dans le modèle Dolev-Yao visant à garantir formellement la sécurité des protocoles cryptographiques face à leur modèle d’attaquant. Deuxièmement, nous les mettons en application à grande échelle dans des analyses de sécurité de protocoles largement déployés. Nous détaillons notamment la découverte de vulnérabilités critiques et leur correction dans des protocoles majeurs tels que les standards industriels de la téléphonie mobile (4G et 5G) et des systèmes de contrôle industriels (OPC UA), ainsi que le système de vote électronique français (FLEP) déployé pour les élections législatives. Enfin, nous ciblons l’écart entre la vérification formelle des spécifications de protocoles et la sécurité de leurs implémentations en introduisant une nouvelle approche de test par fuzzing guidée par le modèle formel de Dolev-Yao. Ce nouveau paradigme de test logiciel permet la découverte automatique d’attaques logiques causées par des bugs dans des implémentations de protocoles cryptographiques complexes. Nous démontrons son efficacité, notamment par la détection de plusieurs nouvelles vulnérabilités et de dizaines de bugs dans des implémentations de protocoles parmi les plus testés (TLS et SSH).