Une IA peut-elle démontrer que du code protège réellement les messages ? Avec AlphaProof Code, Google DeepMind annonce avoir franchi un cap : des agents guidés par des chercheurs ont produit des preuves mathématiques reliant des garanties de sécurité de Signal à son code compilé. La première revendiquée concerne ce niveau de vérification d’une implémentation cryptographique largement déployée, pas la sécurité absolue de toute l’application.
L’annonce, publiée le 10 novembre 2026, déplace le débat. Un logiciel de chiffrement ne doit pas seulement reposer sur de bonnes idées : son implémentation doit respecter les propriétés attendues. C’est précisément ce lien qu’il devient possible d’examiner avec davantage de rigueur.
Ce qu’AlphaProof Code a réellement démontré
Le rapport technique de DeepMind porte sur libsignal, la bibliothèque de référence du protocole Signal. Les auteurs étudient sa version 0.105.4, compilée pour AArch64 Linux dans un petit programme en ligne de commande.
Les preuves relient ce binaire à des propriétés cryptographiques, notamment la confidentialité et l’authenticité des messages, la protection des échanges passés et certaines garanties après compromission. Le travail couvre PQXDH, qui établit le secret initial, et son articulation avec le Triple Ratchet, qui fait évoluer les clés au fil de la conversation.
Il faut conserver cette précision : les auteurs ne déclarent pas avoir vérifié toutes les applications Signal, leurs interfaces ou tous les usages possibles.
La « première » est celle d’un lien entre protocole et implémentation
Dans sa présentation de l’avancée, DeepMind revendique la première vérification à cette profondeur d’une implémentation largement utilisée d’un protocole cryptographique. L’intérêt est de dépasser l’analyse du seul schéma théorique pour atteindre le code compilé.
Cette portée doit rester attachée au titre. Les preuves de sécurité de protocoles et la vérification logicielle existaient auparavant. L’actualité porte sur la profondeur et le périmètre du résultat annoncé, avec l’aide de l’IA.
Pourquoi protéger le passé ne suffit pas à protéger le futur
Les spécifications du Double Ratchet publiées par Signal éclairent deux objectifs essentiels. La confidentialité persistante, souvent appelée forward secrecy, vise à préserver les anciens messages même si des clés présentes sont compromises. La sécurité après compromission cherche à rétablir une protection grâce à l’arrivée de nouveaux secrets, sous les conditions du protocole.
Une image permet de saisir la différence : dérober une clé aujourd’hui ne devrait pas ouvrir toutes les portes d’hier. Et une fois l’intrusion terminée, remplacer les secrets doit permettre de refermer les portes à venir. Cette comparaison reste une simplification ; les garanties exactes dépendent du scénario d’attaque et des éléments dérobés.
De son côté, PQXDH est documenté par Signal comme un mécanisme d’établissement de clés intégrant une protection post-quantique. Cela ne permet pas d’étendre automatiquement chaque preuve sur son implémentation à tous les scénarios quantiques.
L’IA écrit les preuves, Lean en contrôle la validité
Le fonctionnement décrit par DeepMind repose sur une collaboration : les humains approuvent les spécifications, des agents produisent les preuves, puis Lean les vérifie. L’équipe rapporte une campagne de quatre semaines et un test supplémentaire : deux anciennes erreurs, déjà corrigées, ont été réintroduites dans des versions isolées du code. Le système a alors produit des preuves montrant la violation des propriétés visées.
Il s’agit d’un contrôle de la pertinence des garanties, pas de l’annonce de deux nouvelles failles dans Signal.
Le texte à prouver compte autant que la démonstration
La distinction est importante pour comprendre l’apport de l’IA. Une démonstration peut être logiquement correcte tout en portant sur une question trop faible. Si une équipe demande seulement de prouver qu’un programme démarre, une preuve parfaite ne dira rien sur la confidentialité des messages.
Notre lecture du travail est donc que l’effort humain se déplace : définir les bonnes propriétés, examiner les hypothèses et décider ce qui doit être inclus devient central. Le contrôle automatique d’une preuve apporte une assurance sur le raisonnement formalisé ; il ne choisit pas à la place des experts les promesses qui méritent d’être vérifiées.
Les limites qui empêchent de parler d’un Signal « incassable »
Le rapport annonce environ 6,5 millions de lignes de preuves Lean, mais conserve un socle de confiance : spécifications, modèle de la machine et contrats de certaines fonctions, dont des primitives cryptographiques. Les résultats concernent des sessions entre deux interlocuteurs ; la messagerie de groupe reste hors du périmètre étudié.
La documentation publique des artefacts détaille d’autres restrictions. Les canaux auxiliaires sont hors du modèle d’attaquant. La preuve computationnelle ne couvre pas les adversaires quantiques ; certaines garanties symboliques abordent une partie de cette question. Les auteurs signalent aussi des limites de leur borne de sécurité pour de multiples longues sessions et des hypothèses d’environnement.
Ces réserves ne rendent pas les preuves inutiles. Elles permettent de savoir à quelle question elles répondent. Il serait trompeur d’en déduire qu’un téléphone compromis, une interface défaillante ou une attaque extérieure au modèle deviennent sans danger.
Une avancée à juger sur ses artefacts, pas sur une promesse
Les preuves et spécifications sont rendues publiques pour permettre leur examen. Leur disponibilité ne signifie pas que toutes ont déjà fait l’objet d’une réplication indépendante ; nous ne revendiquons pas une telle reproduction ici.
Pour la sécurité logicielle, l’enjeu est concret : rapprocher une propriété compréhensible par les experts du programme qui l’exécute. Si cette méthode devient reproductible sur d’autres versions et d’autres bibliothèques, elle pourrait élargir l’usage de la vérification formelle.
Le résultat le plus intéressant n’est donc pas une promesse d’invulnérabilité. C’est la possibilité de demander à l’IA un livrable plus exigeant qu’une explication convaincante : une preuve contrôlable, accompagnée d’un énoncé précis de ce qu’elle garantit.
Références
- Google DeepMind — Introducing AlphaProof Code, 10 novembre 2026.
- Chaudhuri et al. — AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level, rapport technique.
- Google DeepMind — Documentation et artefacts de vérification.
- Signal — The Double Ratchet Algorithm.
- Signal — The PQXDH Key Agreement Protocol.
