AlphaProof Code de Google DeepMind vérifie le chiffrement de Signal
Les agents IA ont généré plus de 6,5 millions de lignes de preuves mathématiques en quatre semaines, couvrant la poignée de main PQXDH et le Triple Ratchet.
Google DeepMind a annoncé sur son blog officiel que son système multi-agents de vérification formelle AlphaProof Code a vérifié libsignal, la bibliothèque de chiffrement cœur de Signal. Les agents IA ont produit plus de 6,5 millions de lignes de code de preuve mathématique en quatre semaines.
La vérification a couvert la poignée de main PQXDH et le Triple Ratchet utilisés pour le chiffrement de bout en bout, démontrant que la confidentialité, l'authentification, la confidentialité persistante et la sécurité après compromission tiennent dans le code machine compilé. Certaines propriétés de sécurité supposant des attaques par ordinateur quantique ont été vérifiées dans un modèle mathématique séparé.
Les chercheurs ont réinséré deux bogues Signal déjà corrigés dans le code, et AlphaProof Code a prouvé mathématiquement qu'aucun des deux ne satisfaisait les conditions de sécurité. Ils ont également réduit à environ 1 % du total les zones de code nécessitant une revue humaine supplémentaire.
Google DeepMind a publié en open source sur GitHub les spécifications mathématiques et les preuves utilisées lors de la vérification. Aaron Kretz, CTO de Signal, a déclaré que les agents IA étendaient considérablement la vérification formelle, d'un périmètre limité au code d'implémentation réel.
La vérification s'est limitée au code de chiffrement de la messagerie individuelle compilé dans un environnement d'exécution spécifique, et n'a pas couvert la messagerie de groupe ni l'état multi-appareils.
Contexte
Le protocole Signal, ou les chiffrements qui en dérivent, est utilisé par des messageries comme WhatsApp et Google Messages, protégeant les communications de milliards de personnes dans le monde. Le 6 novembre, Google a annoncé que l'IA avait trouvé deux faiblesses dans le chiffrement RSA et publié un algorithme réduisant jusqu'à 30 fois le coût de factorisation des clés.
En bref
Qu'est-ce qu'AlphaProof Code ?
C'est le système multi-agents de vérification formelle de Google DeepMind, qui a vérifié la bibliothèque de chiffrement libsignal de Signal.
Quelles parties de Signal ont été vérifiées ?
La vérification a couvert la poignée de main PQXDH et le Triple Ratchet pour la messagerie individuelle, mais pas la messagerie de groupe ni l'état multi-appareils.
Les preuves sont-elles disponibles ?
Oui, Google DeepMind a publié en open source sur GitHub les spécifications mathématiques et les preuves utilisées.