Contexte et objectifs
Des chercheurs de Google DeepMind ont employé une IA dite agentic pour réaliser une vérification formelle du protocole Signal, l’un des standards de chiffrement utilisé par l’application Signal, Google Messages et WhatsApp. L’objectif était double : confirmer, par une preuve mathématique, les garanties cryptographiques essentielles du protocole et démontrer la capacité du nouveau cadre AlphaProof Code à accélérer ce type d’analyse.
Méthodologie et cadre AlphaProof Code
Le projet, mené en quatre semaines, a consisté à traduire les propriétés de sécurité du protocole (authenticité, confidentialité, intégrité) en formules logiques, puis à laisser AlphaProof Code générer automatiquement les preuves. Avant l’ère de l’IA, chaque étape nécessitait plusieurs mois d’efforts humains : rédaction des spécifications, formalisation en logique, construction manuelle de la preuve. L’agentic AI a réduit ce délai à quelques jours, tout en conservant la rigueur mathématique requise.
Résultats et portée de la vérification
Les preuves obtenues n’ont révélé aucune nouvelle vulnérabilité dans les parties du protocole étudiées. En revanche, lorsqu’AlphaProof Code a été appliqué à des versions antérieures de Signal contenant des failles déjà corrigées, l’outil a correctement identifié l’impossibilité de vérifier formellement ces versions, confirmant ainsi sa sensibilité aux défauts connus. Les chercheurs ont publié la spécification du protocole et les preuves associées afin de faciliter d’autres travaux de vérification formelle.
Enjeux et limites
Cette démonstration confirme que l’IA peut assister la vérification formelle, mais la portée reste restreinte : seule une sous‑partie du protocole a été couverte, le code complet de l’application mobile n’a pas été analysé. Les auteurs soulignent qu’une généralisation à l’ensemble du logiciel mondial nécessitera des avancées supplémentaires, tant au niveau de la modélisation que de la scalabilité de l’outil. Par ailleurs, l’efficacité pratique de la vérification assistée par IA pour des bases de code de grande taille demeure à évaluer.
