Des chercheurs de Google DeepMind ont montré qu’un système d’IA pouvait démontrer mathématiquement d’importantes propriétés de sécurité du protocole de messagerie Signal. L’équipe a utilisé un nouveau cadre appelé AlphaProof Code pour vérifier formellement plusieurs garanties cryptographiques. Le travail a pris environ quatre semaines et s’inscrivait dans un projet de recherche, et non dans le développement d’un produit commercial. Aucun nouveau bug n’a été découvert dans les parties examinées, et l’IA a correctement repéré d’anciennes failles déjà corrigées lorsqu’elle a été testée sur des versions précédentes du protocole.
La vérification formelle consiste à utiliser les mathématiques pour s’assurer qu’un logiciel se comporte exactement comme prévu, sans laisser de place à des vulnérabilités cachées. Jusqu’ici, ce processus exigeait généralement que des spécialistes rédigent des spécifications détaillées, les traduisent en formules, puis construisent la preuve — un travail fastidieux qui pouvait prendre des mois. En confiant une grande partie du travail à une IA agentique (capable de définir et de poursuivre ses propres sous-objectifs), DeepMind a ramené le délai à quelques semaines. Les chercheurs précisent que l’IA avait toujours besoin d’une supervision humaine à des étapes clés, mais qu’elle pouvait proposer des preuves et les corriger elle-même.
Ehren Kret, directeur technique de Signal, a fait remarquer que les travaux de vérification précédents ne portaient que sur de petits fragments de code. L’approche de DeepMind, a-t-il déclaré, permet d’élargir « considérablement » le champ des éléments vérifiables. L’équipe publie la spécification et la preuve qu’elle a élaborées afin que d’autres groupes puissent s’en servir. Malgré ces résultats prometteurs, DeepMind prévient que l’application de cette méthode à des applications entières ou à des chaînes d’approvisionnement logicielles complètes reste un défi. Le coût de cette vérification assistée par l’IA n’a pas été communiqué.
Pourquoi c’est important
Si l’IA peut démontrer de manière fiable la sécurité des protocoles cryptographiques, les utilisateurs de Signal, Google Messages, WhatsApp et d’applications similaires pourraient avoir davantage confiance dans la confidentialité de leurs messages. Pour les entreprises qui dépendent des communications chiffrées — banques, établissements de santé et journalistes — cette technologie pourrait un jour fournir des garanties vérifiables juridiquement que leurs logiciels ne comportent aucune faille critique.
Pourquoi c'est important
Pour le grand public, cette annonce signifie que le chiffrement qui protège les conversations bénéficie désormais d’une vérification mathématique supplémentaire, ce qui réduit le risque de bugs cachés. Pour les entreprises qui doivent prouver leur conformité aux règles de protection de la vie privée, la vérification assistée par l’IA pourrait devenir un nouveau moyen de démontrer la sécurité de leurs logiciels sans longs audits manuels.
