DeepMind a vérifié en un mois une partie de la cryptographie de Signal avec l'IA

Vos tests passent, la revue de code ne révèle aucun problème, et pourtant la confiance dans le code critique n'est pas au rendez-vous. Pour la cryptographie, c'est particulièrement gênant : une combinaison rare de conditions peut peser plus lourd que mille exécutions réussies. Selon ZDNET, Google DeepMind a appliqué AlphaProof Code à une partie du code cryptographique de Signal et a terminé la vérification en un mois. L'intérêt pratique réside dans la tentative de réduire le travail manuel de construction des preuves mathématiques.

Précisons d'emblée la portée du résultat : la publication n'indique pas que les chercheurs ont prouvé la sécurité de toute la messagerie. Il s'agit de certaines parties de l'implémentation et de propriétés que l'équipe a choisi de vérifier. Pour un développeur, la différence est essentielle : une preuve répond à une question précise sur le programme, elle ne délivre pas un certificat de fiabilité universel.

Ce que l'on vérifie mathématiquement

Imaginez une fonction qui met à jour l'état cryptographique après le traitement d'un message. Un test classique lui transmet des données choisies et compare le résultat à celui attendu. On peut ajouter des entrées aléatoires, des valeurs limites et de longues séquences d'appels. Mais chaque exécution ne vérifie toujours qu'un scénario précis.

En vérification formelle, on commence par écrire l'exigence exacte sur le comportement de la fonction. On prouve ensuite que le code la respecte dans tous les cas couverts par le modèle défini. Exemple hypothétique : l'opération doit conserver un certain rapport entre l'ancien et le nouvel état. Il s'agit d'une illustration de la méthode, et non de la description d'une propriété précise prouvée par l'équipe de DeepMind.

La partie la plus coûteuse de ce travail commence souvent avant même la preuve. Il faut décider ce que le programme promet exactement, quelles hypothèses sont admissibles et où s'arrête le périmètre vérifié. Si l'exigence est mal formulée ou incomplète, même une preuve correcte ne répondra pas à la vraie question sur la sécurité du produit.

Comment le travail a été réparti entre humains et agents

D'après ZDNET, les chercheurs se sont appuyés sur des travaux antérieurs de la Signal Foundation. Les humains, avec les agents, ont défini les énoncés à démontrer. Plusieurs agents ont ensuite construit les preuves ; par ailleurs, le système a aidé à contrôler le résultat et a signalé les zones nécessitant l'attention d'un humain.

Le média indique qu'environ 1 % de la base de code a été signalé pour une nouvelle vérification manuelle. Ce chiffre doit être lu avec prudence : le texte ne précise pas comment le dénominateur a été défini, ni ce qui était considéré comme une zone vérifiée. Il ne signifie pas que l'IA a confirmé de manière autonome la sécurité des 99 % restants de l'application Signal.

Un autre résultat annoncé concerne le travail sur deux bogues de Signal corrigés auparavant. Ce type de test est utile : l'outil doit distinguer une implémentation correcte d'une implémentation défectueuse. Toutefois, un bref résumé ne suffit pas pour reconstituer l'expérience, comprendre ses conditions et évaluer quelles classes d'erreurs le système sait réellement détecter.

Le délai d'un mois nécessite lui aussi du contexte. ZDNET le compare à un travail qui aurait pu prendre des années à des experts, mais ne cite aucun projet comparable, ni le coût en calcul, ni un décompte détaillé du travail humain. Il est donc trop tôt pour promettre aux équipes la même accélération.

Que faire en tant que développeur et product manager

Si l'approche se confirme sur les éléments disponibles, elle sera particulièrement intéressante pour de petits modules où une erreur coûte cher et dont les exigences peuvent être formulées avec précision. On peut commencer par une seule fonction, en décrivant ses entrées admissibles, les propriétés attendues et ses dépendances. On verra ensuite plus clairement s'il y a matière à vérification formelle et quel résultat l'équipe pourra accepter.

Pour le product manager, il est utile de définir à l'avance les limites de la promesse faite à l'utilisateur. Une propriété prouvée d'un module cryptographique ne dit automatiquement rien sur la protection de l'appareil, l'interface, les sauvegardes ou la justesse des mises à jour. Ces questions appellent leurs propres vérifications.

Selon la publication, DeepMind prévoit d'ouvrir le code d'AlphaProof Code. Pour évaluer l'adéquation de l'outil, il faudra le dépôt lui-même, les spécifications, les preuves vérifiables et la description des limites. Pour l'instant, c'est un exemple instructif d'application de l'IA à un problème d'ingénierie : les agents peuvent aider à préparer des preuves, mais la qualité des exigences et les limites du résultat restent de la responsabilité des humains.