DeepMind affirme avoir fait prouver par l'IA deux fonctions de Signal
Le 10 novembre, Google DeepMind a annoncé que des agents d'IA, guidés par des experts, ont démontré que deux fonctions du code de Signal, l'ouverture d'une conversation chiffrée et le renouvellement des clés, respectent des règles de sécurité fixées à l'avance, selon un travail de recherche publié par l'entreprise.
- Selon DeepMind, les agents ont produit plus de six millions de lignes de preuve en Lean, un langage de programmation qui contrôle automatiquement chaque étape de la preuve. Un humain n'a relu que 1 % du code vérifié, et le travail a duré quatre semaines.
- Pour vérifier que le système distingue un code correct d'un code défectueux, les chercheurs ont remis deux anciennes erreurs de sécurité réelles dans une copie isolée du code de Signal. Dans les deux cas, le système a démontré que cette version n'était pas sûre.
- Selon The Register, la preuve suppose que le chiffrement lui-même est impossible à casser : elle ne garantit donc pas que les messages résistent à toute attaque. L'équipe comptait cinq personnes, et le coût en jetons (unités de calcul facturées) n'est pas communiqué.
© 2026 EXYVIA. Reprise autorisée avec mention « Radar IA EXYVIA » et lien.
Ce que ça change pour une direction
- Si votre entreprise édite des logiciels sensibles (paiement, santé, énergie), repérez les parties du logiciel dont une faille coûterait le plus cher : ce sont les candidats à une preuve de ce type.
- Distinguez « prouvé » de « sans risque » : une preuve couvre seulement les propriétés que des humains ont choisies. Dans un audit ou un appel d'offres, demandez lesquelles.
- DeepMind met ses fichiers de preuve en accès libre : demandez à votre prestataire d'estimer le temps d'experts et le coût de calcul avant d'étendre la méthode à d'autres logiciels.
Sources :