Le chiffrement de Signal validé par une preuve IA de 6,5 millions de lignes

Le code de chiffrement de Signal peut désormais se prévaloir d’une chose que presque aucun logiciel largement utilisé ne possède : une preuve mathématique qu’il tient ses promesses. Une équipe d’agents IA a passé au crible libsignal, la bibliothèque qui fait fonctionner le protocole Signal, et démontré que ses conversations individuelles restent secrètes, permettent de vérifier l’identité de son interlocuteur et écartent de nouveau un attaquant après le vol d’une clé. Les chercheurs n’ont découvert aucune nouvelle faille.

Cette avancée dépasse largement le cercle des utilisateurs de Signal. Son protocole est la norme mondiale pour la messagerie chiffrée de bout en bout, et des variantes protègent les conversations sur WhatsApp, Messenger et Google Messages. Vérifier à ce niveau de détail du code réellement déployé était jusqu’ici si lent que presque personne ne s’y risquait : l’une des plus grandes réussites du domaine, la vérification formelle d’un noyau de système d’exploitation, a demandé vingt années-personnes. Ici, il a fallu quatre semaines.

L’outil, conçu par Google DeepMind, s’appelle AlphaProof Code. Des experts humains et des modèles d’IA ont d’abord traduit les objectifs de sécurité de Signal en énoncés formels dans Lean, un langage de programmation conçu pour les preuves mathématiques, puis une personne a vérifié chacun d’eux. Des équipes de 40 à 80 agents, propulsées par Gemini Carbon, ont ensuite rédigé les preuves, en travaillant pendant 24 à 72 heures d’affilée sur une seule machine. Le résultat représente environ 6,5 millions de lignes de Lean.

Personne n’a besoin de faire confiance à ces millions de lignes. Le noyau de Lean vérifie chaque étape et rejette toute preuve invalide : peu importe donc le modèle qui l’a rédigée ou le nombre d’erreurs qu’il a commises en chemin. En revanche, il faut bien faire confiance à un élément bien plus restreint : environ 26 000 lignes de spécifications et à un modèle du fonctionnement d’un processeur ARM lorsqu’il exécute du code.

Les preuves portent sur les éléments de Signal qui protègent une conversation : l’échange de clés PQXDH, qui établit une conversation, et le Triple Ratchet, qui renouvelle la clé à chaque message, y compris la couche post-quantique conçue pour résister aux futurs ordinateurs quantiques. Concrètement, cela signifie que le vol des clés actuellement stockées sur un téléphone ne donne pas accès aux anciens messages, et que le voleur perd à nouveau l’accès dès que les deux interlocuteurs échangent de nouvelles clés.

Pour montrer que le système sait distinguer le bon code du mauvais, les chercheurs ont réintroduit deux anciennes failles de libsignal, déjà corrigées. Dans un cas, la bibliothèque conservait une copie d’une clé secrète qu’elle aurait dû supprimer. Pour les deux failles, AlphaProof Code a produit une preuve vérifiée par machine démontrant que la version contenant le bug n’était pas sécurisée.

Les limites sont réelles. La preuve ne couvre que les conversations individuelles, et DeepMind indique que la messagerie de groupe fera l’objet de travaux ultérieurs. Elle s’applique à libsignal version 0.105.4, compilée avec le compilateur Rust standard pour ARM Linux au sein d’un petit programme de test, et non aux applications Signal complètes pour iPhone, Android ou ordinateur. Les composants cryptographiques de bas niveau sont présumés sûrs, mais ne sont pas prouvés comme tels. Une erreur dans les spécifications approuvées par des humains affaiblirait la garantie, et WhatsApp ainsi que les autres applications utilisent leurs propres versions du protocole : le résultat ne s’applique donc pas automatiquement à leurs logiciels. Google a également refusé de dire à Wired combien l’analyse avait coûté ou s’il comptait la proposer comme service payant.

Signal a salué le résultat. « À mesure que les menaces de sécurité liées à l’IA se multiplient, la vérification rigoureuse de l’implémentation du protocole Signal renforce encore notre confiance dans les garanties de confidentialité de notre code », a déclaré Ehren Kret, directeur technique de Signal, dans un communiqué. Swarat Chaudhuri, chercheur chez DeepMind, s’est montré plus prudent : il a expliqué à Wired qu’« il reste beaucoup de chemin à parcourir » avant que la méthode puisse s’étendre « à tous les logiciels du monde ».

Pour les utilisateurs de Signal, rien à installer ni aucun réglage à modifier. La preuve porte sur du code déjà présent dans l’application.

DeepMind a publié ces travaux le 10 novembre, accompagnés d’un article technique, et mis en libre accès les spécifications et les preuves sur GitHub. L’entreprise présente le projet Signal comme une étape importante vers un grand défi de vérification formelle lancé en avril. Elle cite les micrologiciels d’appareils médicaux et les logiciels des réseaux électriques parmi les systèmes qu’elle souhaite vérifier ensuite.

Chaudhuri a également fixé une limite à la part du travail qui devrait revenir aux machines. « Nous ne voulons pas de ce genre de monde où tout se fait au feeling avec l’IA, où l’IA définit les objectifs et produit les preuves », a-t-il déclaré à Wired. Ce sont toujours les humains qui décident de ce qui est sécurisé ; l’IA ne fait que le prouver.

Étiquettes: cybersécurité, Google DeepMind, AlphaProof Code, chiffrement de bout en bout, libsignal, Signal