Google DeepMind a utilis\u00e9 AlphaProof Code pour v\u00e9rifier formellement certaines propri\u00e9t\u00e9s de s\u00e9curit\u00e9 de libsignal, la biblioth\u00e8que qui impl\u00e9mente le protocole de chiffrement de Signal. L\u2019\u00e9tude porte notamment sur le m\u00e9canisme qui renouvelle les cl\u00e9s au fil d\u2019une conversation. Une preuve formelle permet d\u2019\u00e9tablir qu\u2019une propri\u00e9t\u00e9 d\u00e9finie \u00e0 l\u2019avance tient pour le code \u00e9tudi\u00e9, sous les hypoth\u00e8ses retenues.<\/p>\n
L\u2019\u00e9quipe a fait travailler environ 80 agents IA sur les preuves. Les chercheurs ont d\u00e9fini et relu les propri\u00e9t\u00e9s \u00e0 v\u00e9rifier. Les agents ont produit plus de six millions de lignes dans Lean, un langage dot\u00e9 d\u2019un syst\u00e8me capable de v\u00e9rifier m\u00e9caniquement les preuves. L\u2019int\u00e9r\u00eat de la m\u00e9thode tient au fait qu\u2019elle s\u2019applique \u00e0 une impl\u00e9mentation du protocole, avec ses d\u00e9tails de code.<\/p>\n
Le p\u00e9rim\u00e8tre \u00e9tudi\u00e9 concerne les \u00e9changes \u00e0 deux dans une impl\u00e9mentation cibl\u00e9e sur architecture AArch64. La preuve repose aussi sur des hypoth\u00e8ses concernant les primitives cryptographiques utilis\u00e9es. Les conversations de groupe et la s\u00e9curit\u00e9 globale de l\u2019application restent en dehors de ce p\u00e9rim\u00e8tre.<\/p>\n
Pour \u00e9valuer la m\u00e9thode, les chercheurs ont aussi r\u00e9introduit deux anciens d\u00e9fauts corrig\u00e9s et test\u00e9 leur effet sur les garanties formalis\u00e9es. Le travail illustre le r\u00f4le qui reste aux sp\u00e9cialistes quand la production des preuves s\u2019acc\u00e9l\u00e8re : choisir les propri\u00e9t\u00e9s \u00e0 v\u00e9rifier et examiner les hypoth\u00e8ses qui d\u00e9limitent leur port\u00e9e.<\/p>\n