Une équipe de chercheurs de Google DeepMind a réussi à démontrer mathématiquement la robustesse du protocole de chiffrement de Signal grâce à l'intelligence artificielle. Cette expérience, baptisée AlphaProof Code, marque une étape inédite dans la vérification formelle de logiciels complexes, traditionnellement jugée trop coûteuse en temps et en ressources humaines.
Une démonstration par la preuve mathématique
Contrairement aux méthodes d'audit classiques qui consistent à tester un logiciel pour détecter des failles, la vérification formelle vise à prouver mathématiquement qu'un code ne peut pas enfreindre ses propriétés de sécurité. Pour ce projet, Google a déployé 80 agents d'IA fonctionnant avec le modèle Gemini 4 Carbon. Ces agents ont généré 6,5 millions de lignes de démonstration dans le langage Lean, validant ainsi le fonctionnement du mécanisme de renouvellement des clés de chiffrement, pilier de la protection des échanges sur Signal.
L'IA au service de la fiabilité logicielle
Le processus a permis de confirmer qu'un attaquant accédant aux clés stockées sur un terminal ne peut pas déchiffrer les messages passés, grâce au système de renouvellement constant des clés. Pour tester la fiabilité de leur méthode, les chercheurs ont réintroduit d'anciennes vulnérabilités corrigées dans le code