Signal passe au crible de l’IA avec des preuves cryptographiques

Google DeepMind affirme avoir utilisé des agents d’intelligence artificielle pour vérifier formellement des propriétés de sécurité de Signal, en s’attaquant cette fois au code compilé de libsignal plutôt qu’à un simple modèle théorique. L’équipe dit avoir validé le handshake PQXDH et le Triple Ratchet, deux briques centrales du protocole de messagerie, avec des preuves lues par la machine et contrôlées par des humains. L’enjeu est clair : savoir si une IA peut aider à démontrer, de façon rigoureuse, qu’un code de chiffrement fait bien ce qu’il promet. Et ce n’est pas le genre de sujet qu’on règle avec un simple “tout va bien”.

Une preuve sur le code réel, pas seulement sur le papier

Le point le plus intéressant n’est pas l’annonce elle-même, mais le terrain choisi. Les chercheurs disent être allés au-delà d’un modèle abstrait du protocole Signal pour vérifier une implémentation compilée de libsignal, en l’occurrence des crates libsignal v0.105.4 et SPQR v1.6.0, assemblées dans un exécutable Linux AArch64 lié statiquement. Selon leur papier, il s’agit de la première preuve de sécurité au niveau protocolaire pour du code non modifié d’une implémentation cryptographique largement déployée [à vérifier].

Le travail s’appuie sur AlphaProof Code, un cadre multi-agents qui transforme des objectifs de sécurité en spécification mathématique, puis en preuves Lean vérifiées par le noyau du langage. Dans ce montage, les humains choisissent les propriétés à démontrer, lèvent les ambiguïtés et valident les arbitrages, tandis que les agents génèrent le code de preuve. Autrement dit, l’IA ne décide pas seule du sens de la démonstration ; elle exécute une partie de la mécanique. C’est moins glamour qu’un robot qui “comprend” la cryptographie, mais beaucoup plus utile.

Ce que la vérification couvre, et ce qu’elle laisse de côté

La vérification porte sur le code de session un-à-un, avec le handshake PQXDH et le mécanisme Triple Ratchet. Les chercheurs disent avoir formalisé quatre garanties : la forward secrecy, qui protège les anciens messages si l’état courant est compromis ; l’authentification ; la post-compromise security, c’est-à-dire la capacité à retrouver un niveau de sécurité après une compromission ; et la handshake secrecy. Le papier ajoute deux volets d’analyse, l’un symbolique et l’autre computationnel, pour encadrer les hypothèses cryptographiques.

Reste que le résultat ne certifie pas Signal dans son ensemble. Le périmètre exclut la génération de clés, la messagerie de groupe, les effets de bord multi-appareils et les canaux latéraux. Certaines briques cryptographiques restent aussi appuyées sur des contrats de confiance, ainsi que sur les axiomes standards de Lean et les hypothèses du modèle AArch64. Les auteurs précisent donc que la preuve donne une forte assurance sur un scénario précis, pas un blanc-seing général sur toute l’application. À ce stade, le mot “formel” n’efface pas les limites du périmètre.

Une méthode lourde, mais déjà moins héroïque qu’avant

La charge de travail donne une idée de l’ambition. Cinq chercheurs ont travaillé pendant quatre semaines, avec des agents tournant en continu sur leurs stations de travail. Les systèmes auraient produit environ 6,5 millions de lignes de preuve Lean vérifiées par machine, adossées à quelque 26 000 lignes de spécifications et de sémantique AArch64 considérées comme de confiance. Les auteurs disent aussi n’avoir écrit aucune ligne de preuve eux-mêmes ; ils ont plutôt orchestré la production, la revue et l’intégration.

Le gain potentiel est là : la vérification formelle a longtemps ressemblé à un sport d’endurance, réservé à quelques projets très coûteux. Les chercheurs rappellent que la preuve du micro-noyau seL4 a mobilisé 20 années-personnes, tandis que CompCert a demandé six ans de développement. Leurs propres travaux n’annulent pas cet historique, mais ils suggèrent qu’avec des agents, la facture pourrait baisser. Reste à voir si la même méthode tient la route sur d’autres bases de code, car l’IA aime parfois la précision autant qu’un chat aime l’eau.

Pourquoi Signal et pourquoi maintenant

Le choix de Signal n’a rien d’anodin. L’application est devenue une référence de la messagerie chiffrée, et son architecture cryptographique sert de base à des garanties de confidentialité très observées par les défenseurs de la vie privée comme par les chercheurs en sécurité. Dans ce contexte, démontrer formellement une partie de son comportement a une valeur de signalisation industrielle, au sens fort : cela montre ce que des agents peuvent produire quand la cible n’est ni un puzzle académique ni un modèle jouet.

Signal, de son côté, y voit surtout un renforcement de confiance. Son directeur technique, Ehren Kret, estime que le travail “gives us even greater confidence in our code’s privacy guarantees.” Les chercheurs, eux, présentent cette étape comme un test de méthode pour aller plus loin : davantage de routines vérifiées, moins d’hypothèses de confiance, et à terme une couverture plus large des versions de libsignal avant leur publication. Pour l’instant, l’idée n’est pas d’annoncer un déploiement immédiat, mais de montrer qu’un workflow human-in-the-loop peut passer à l’échelle sans perdre le contrôle des hypothèses.