AlphaProof Code : une IA prouve des propriétés du code de Signal
· Rédaction BehindLines
Des chercheurs de Google DeepMind affirment avoir démontré, avec des agents d'intelligence artificielle, plusieurs garanties de sécurité du code réel sur lequel repose le protocole de messagerie Signal. D'après le billet de DeepMind, il s'agirait de la première vérification formelle, à ce niveau de détail et par une IA, d'un protocole cryptographique très répandu ; The Register rapporte que c'est ce que revendiquent les chercheurs.
Une méthode en équipe
Le système s'appelle AlphaProof Code. Selon DeepMind, des experts humains et plusieurs modèles de langage commencent par transformer les objectifs de sécurité de Signal en spécifications mathématiques, que des personnes relisent chacune à leur tour. Des agents écrivent ensuite les preuves en Lean, un langage dont le vérificateur contrôle automatiquement les démonstrations. D'après The Register, les agents ont produit 6,5 millions de lignes de Lean ; DeepMind évoque plus de 6 millions. Ils ont ensuite audité ces preuves et signalé environ 1 % du code pour un second regard humain, ce qui, d'après DeepMind, fait gagner beaucoup de temps.
Ce qui a été prouvé
Les preuves visent le code compilé, et non le seul schéma théorique du protocole, souligne DeepMind. Elles couvrent par exemple la protection des messages avant et après la compromission passagère d'un appareil. The Register mentionne aussi la confidentialité persistante, l'authentification et le secret de l'échange initial de clés. Pour s'assurer que la méthode sait distinguer un code correct d'un code bogué, l'équipe a replacé deux vraies failles, corrigées depuis, dans une version isolée du code de Signal ; chaque fois, le système a fourni une preuve, validée par machine, que cette version n'était pas sûre.
Des limites reconnues
The Register précise que le résultat reste théorique : il part d'une cryptographie supposée parfaite et n'assure pas le secret calculatoire des octets. Selon les auteurs cités par le site, le travail a pris quatre semaines à cinq personnes et consommé « pas mal de jetons ». Ils rappellent que la vérification du micronoyau seL4 a coûté 20 années-personnes et que le compilateur CompCert a demandé six ans de développement.
Ehren Kret, directeur technique de Signal, estime dans le billet de DeepMind que cette approche permet d'étendre nettement le périmètre de la vérification formelle. Swarat Chaudhuri, l'un des chercheurs, déclare à The Register que la prochaine difficulté sera de décider quoi spécifier, davantage que de produire les preuves.
Pourquoi c'est important
DeepMind rappelle que les vulnérabilités réelles se logent souvent dans l'écart entre la conception et la mise en œuvre d'un protocole, un écart que ces preuves cherchent à combler. L'entreprise y voit une base pour sécuriser d'autres systèmes vitaux, comme les micrologiciels de dispositifs médicaux ou les logiciels de réseaux électriques, tout en précisant que le passage à plus grande échelle demande encore des recherches.