Google DeepMind affirme avoir franchi une étape majeure dans la vérification formelle des logiciels. Son nouveau cadre multi-agent AlphaProof Code a produit des preuves mathématiques portant sur le code cryptographique central de Signal, jusqu’à l’implémentation exécutée sur les appareils.
La vérification formelle consiste à démontrer mathématiquement qu’un programme respecte des propriétés précises. Cette méthode fournit un niveau d’assurance très élevé, mais elle demande habituellement des années de travail à des spécialistes. DeepMind indique avoir achevé son étude en quatre semaines avec une équipe mêlant experts humains et agents IA.
Six millions de lignes de preuves en Lean
AlphaProof Code organise le travail comme une équipe de recherche. Des humains définissent les objectifs de sécurité et contrôlent leur traduction en spécifications mathématiques. Plusieurs agents alimentés par Gemini Carbon produisent ensuite les preuves dans Lean, un langage dont le noyau vérifie mécaniquement chaque étape.
Selon DeepMind, le système a généré plus de six millions de lignes de Lean. Les agents ont également audité le résultat et signalé environ 1 % de la base de code pour un examen humain approfondi. Le reste pouvait être contrôlé automatiquement par le vérificateur de preuves.
L’équipe ne s’est pas limitée à la description théorique du protocole Signal. Elle a cherché à relier les garanties cryptographiques au code compilé réellement déployé. Cette distinction est importante : des vulnérabilités peuvent apparaître entre une conception correcte et sa mise en œuvre logicielle.
Deux anciens bugs réintroduits pour tester la méthode
Les chercheurs ont aussi réintroduit dans un environnement isolé deux failles réelles déjà corrigées. AlphaProof Code a alors produit des preuves vérifiées montrant que les versions modifiées ne satisfaisaient plus les garanties attendues. Ce test doit montrer que le système ne se contente pas de valider automatiquement n’importe quelle implémentation.
DeepMind présente ce travail comme la première vérification formelle de cette profondeur appliquée au code d’un protocole cryptographique largement déployé. Signal protège les conversations de l’application éponyme, mais sa technologie est aussi utilisée dans d’autres services, dont Google Messages.
Un outil d’IA encadré par des experts
Le résultat ne signifie pas que l’IA a certifié seule l’intégralité de Signal. Les humains ont choisi les propriétés à prouver, relu les spécifications et examiné les zones signalées. Les preuves ne couvrent que les garanties explicitement formulées. Elles ne peuvent pas exclure un problème situé en dehors de ce périmètre.
La nouveauté réside dans l’échelle et la vitesse du travail automatisé. Si la méthode se généralise, elle pourrait rendre la vérification formelle plus accessible pour les logiciels critiques, comme les systèmes médicaux, les réseaux électriques ou les infrastructures publiques.
DeepMind a publié les artefacts de vérification et le papier technique afin qu’ils puissent être examinés. Le laboratoire envisage de combiner cette approche avec ses agents de correction de code, notamment CodeMender. L’objectif est de faire travailler détection, réparation et preuve mathématique dans une même chaîne défensive.
Sources : annonce et résultats de Google DeepMind ; The Register.
