Google DeepMind affirme avoir vérifié formellement, grâce à l’IA, des éléments du code de chiffrement de Signal. L’équipe dit avoir mené l’opération en un mois et la présente comme la première vérification formelle d’un protocole cryptographique largement déployé, au niveau de l’implémentation. Le périmètre reste partiel, sans projet de produit grand public, mais les chercheurs évoquent des ouvertures vers d’autres systèmes critiques.
DeepMind revendique une première mondiale et précise le périmètre
Les chercheurs de Google DeepMind affirment avoir utilisé l’IA pour vérifier formellement, pour la première fois, un protocole cryptographique largement déployé à ce niveau. Ils précisent qu’il s’agit également de la première vérification formelle de l’implémentation d’un tel protocole, quelle que soit la méthode employée. L’équipe indique avoir mené ce travail en un mois, alors que des experts auraient normalement besoin de plusieurs années. DeepMind souligne que seule une partie du code de Signal a été vérifiée et considère ce résultat comme une étape vers une infrastructure de sécurité renforcée, dans un contexte où l’IA transforme la cybersécurité. Aucun lancement de produit grand public n’est prévu à ce stade. Les chercheurs se disent ouverts à publier leur code en open source pour soutenir d’autres initiatives de vérification formelle, et estiment que la vérification de la cryptographie de base de Signal pourrait servir de fondation pour sécuriser d’autres systèmes essentiels, comme les firmwares de dispositifs médicaux ou les logiciels de réseaux électriques.
Une méthode hybride avec AlphaProof Code et Gemini Carbon
Les chercheurs ont utilisé AlphaProof Code et se sont appuyés sur des vérifications antérieures réalisées par la Signal Foundation. La tâche a été divisée en deux volets : des humains ont collaboré avec des agents pour définir les propriétés à démontrer, puis plusieurs agents, fondés sur Gemini Carbon, ont conduit les preuves. Ces agents ont également audité les résultats et signalé les zones à revoir par des humains, ce qui ne concernait que 1 % de la base de code, selon les chercheurs. Pour tester la capacité de l’approche à distinguer le code correct du code défectueux, deux bogues de Signal déjà corrigés ont été soumis à AlphaProof Code, qui a produit des preuves correctes.
Vous codez avec l’IA ?
Outils, agents et nouveautés dev IA décryptés, chaque soir en 5 min. Gratuit.
Inclus dès l'inscription : notre sélection des meilleurs guides & comparatifs IA.
Choisissez votre rythme
Gratuit · Pas de spam · Désabonnement en 1 clic
Ce que cela change pour Signal et les messageries chiffrées
Des parties du code de chiffrement de Signal ont été vérifiées formellement, et des preuves mathématiques ont établi que certains composants fonctionnent comme prévu, sans erreurs, selon l’équipe. Les chercheurs estiment que cette preuve automatique appliquée au protocole de base de Signal renforce leur confiance dans le respect des garanties de confidentialité du code. WhatsApp et Google Messages utilisent le même chiffrement, ce qui étend la portée de ces résultats à d’autres messageries chiffrées.
La vérification formelle à l’épreuve de l’IA et de la cybersécurité
Le développement de preuves formelles est historiquement difficile et long, ce qui a souvent limité leur application aux logiciels en production. AlphaProof Code est présenté comme une avancée vers des vérifications de sécurité plus robustes, alors que la création manuelle de ces preuves reste très chronophage. L’IA est décrite comme un facteur ambivalent pour la cybersécurité : elle représente à la fois un risque majeur et un outil puissant. L’année 2026 a été marquée par de nombreux incidents de sécurité liés à l’IA, souvent impliquant des agents, tandis que des entreprises comme Anthropic, Google et OpenAI développent des modèles dédiés à la cybersécurité, dont Claude Mythos d’Anthropic. Plus largement, des avancées récentes attribuées à l’IA dans les mathématiques et la capacité de calcul à grande échelle laissent entrevoir une accélération de tâches autrefois très manuelles. Cette dynamique est jugée rassurante au regard des vulnérabilités récemment découvertes par des systèmes d’IA dans des logiciels, alors que de nombreuses communications reposent sur la cryptographie de Signal.
