AlphaProof Code : Google DeepMind prouve la sûreté de libsignal

Démontrer plutôt que tester

Les tests et les audits peuvent établir qu'aucune faille n'a été trouvée, pas qu'il n'en existe aucune. La vérification formelle démontre au contraire, comme un théorème, que le code ne peut pas enfreindre certaines propriétés. Elle est réputée très coûteuse : celle du noyau seL4, achevée en 2009, a exigé l'équivalent de vingt ans de travail pour une personne.

Ici, des experts humains ont défini ce qu'il fallait prouver, à partir de travaux académiques sur Signal. Les agents, propulsés par Gemini 4 Carbon, ont rédigé environ 6,5 millions de lignes de démonstration en langage Lean, dont le vérificateur contrôle chaque étape automatiquement. Selon les chercheurs, aucun n'a écrit lui-même une ligne de preuve.

L'enjeu central est le « ratchet », le mécanisme qui renouvelle en continu les clés. Les preuves établissent qu'un attaquant qui volerait les clés stockées sur un téléphone ne pourrait pas lire les messages antérieurs, chaque clé étant dérivée de la précédente puis effacée. La conversation redevient sûre dès que les deux interlocuteurs échangent de nouveaux messages, et nul ne peut usurper l'identité de l'un d'eux. Pour valider la méthode, l'équipe a réintroduit deux anciens bugs corrigés depuis : le système a montré que ces versions n'offraient plus les garanties attendues.

Des limites assumées

Le directeur technique de Signal, Ehren Kret, a salué « une avancée majeure ». Google signale toutefois que la preuve ne couvre que les conversations à deux, suppose que les briques cryptographiques de base fonctionnent parfaitement sans les vérifier, et porte sur une version de test sous Linux, pas sur les applications mobiles.

Les auteurs en tirent une leçon : maintenant que les preuves deviennent bon marché, la question difficile est de savoir quoi prouver.