AlphaProof Code de DeepMind prouve la sécurité de Signal

Des chercheurs de Google DeepMind ont annoncé une avancée majeure en sécurité logicielle grâce à AlphaProof Code, un framework combinant agents IA et expertise humaine pour vérifier formellement le code du protocole Signal. Cette technologie protège des milliards de conversations privées dans des applications comme Signal et Google Messages. La vérification formelle consiste à prouver mathématiquement qu’un programme respecte des propriétés de sécurité données. Elle est souvent coûteuse et réservée à des équipes d’experts. Ici, l’équipe a fait franchir une étape à cette discipline: pour la première fois, une IA a permis de vérifier à ce niveau de profondeur un protocole cryptographique largement déployé. Il s’agit également de la première fois que l’implémentation réelle d’un tel protocole fait l’objet d’une vérification formelle, que le processus ait recours à l’IA ou non. AlphaProof Code fonctionne comme une équipe de recherche. Des experts humains définissent avec plusieurs modèles les objectifs de sécurité à prouver, puis chaque spécification mathématique est revue par des spécialistes. Des agents pilotés par Gemini Carbon génèrent ensuite des preuves en Lean, un langage qui permet de vérifier automatiquement la correction des programmes. Ces agents ont produit plus de six millions de lignes de Lean. Ils ont également audité les preuves et identifié environ 1 % du code nécessitant un second regard humain, tandis que le système validait automatiquement le reste. L’originalité du travail tient aussi à son niveau de vérification. Les protocoles cryptographiques sont souvent analysés seulement au niveau de leur conception. Les agents de Google DeepMind ont démontré que le code compilé, exécuté sur les appareils, satisfait les propriétés de sécurité voulues, notamment la protection des messages avant et après une compromission temporaire d’un appareil. Cette approche réduit le risque de vulnérabilités situées entre la théorie et l’implémentation. Le projet a abouti en quatre semaines, alors qu’un effort équivalent prendrait historiquement plusieurs années à des équipes spécialisées. Pour valider la méthode, les chercheurs ont réintroduit deux bugs réels, déjà corrigés, dans une copie isolée du code de Signal. Dans les deux cas, le système a prouvé que la version modifiée était désormais non sécurisée. Cette réussite ouvre la voie à une automatisation plus poussée de la vérification du logiciel critique, là où une faille peut exposer simultanément des millions d’utilisateurs. Elle montre que les agents IA peuvent assister l’expertise humaine pour prouver la sûreté de systèmes complexes, sans remplacer les décisions humaines sur les points les plus sensibles.