Code de Signal vérifié par l'IA de DeepMind en quatre semaines

Qu'est-ce que la vérification formelle ?

C'est l'usage des mathématiques, plutôt que de tests, pour démontrer qu'un logiciel se comporte comme voulu. C'est la garantie de sécurité la plus solide qui existe, mais elle est lente et fastidieuse. La plupart des vérifications de protocoles cryptographiques s'arrêtent à la conception. DeepMind dit avoir vérifié l'implémentation réelle, là où se cachent souvent les vrais bogues. Selon l'entreprise, c'est la première vérification formelle de l'implémentation d'un protocole aussi répandu, avec ou sans IA.

Comment fonctionne AlphaProof Code ?

Ce cadre associe plusieurs modèles d'IA et des experts humains. Des chercheurs et des modèles ont traduit les objectifs de sécurité de Signal en spécifications formelles, relues une à une par des humains. Des agents reposant sur Gemini Carbon ont ensuite écrit les preuves : plus de six millions de lignes de Lean, un langage qui permet à un ordinateur de vérifier les preuves automatiquement. Les agents ont audité leur propre travail et signalé environ 1 % du code pour une seconde relecture humaine.

Les preuves portent par exemple sur la protection des messages avant et après la compromission temporaire d'un appareil.

L'IA a-t-elle trouvé des failles ?

Aucune nouvelle vulnérabilité n'a été découverte dans les parties analysées. Pour tester la capacité du système à distinguer le bon code du mauvais, l'équipe a réintroduit deux vrais bogues déjà corrigés dans une version isolée du code. Dans les deux cas, selon DeepMind, le système a produit une preuve vérifiée par machine que cette version n'était pas sûre.

Limites : l'application mobile Signal n'a pas été vérifiée dans son ensemble, et DeepMind s'appuyait sur un travail antérieur de la Signal Foundation. Ehren Kret, directeur technique de Signal, a indiqué que ce travail portait sur des portions plus petites, alors que l'approche de DeepMind permet une extension significative.

Le chercheur Swarat Chaudhuri refuse que l'IA écrive à la fois les objectifs et les preuves, en se notant elle-même. D'où la relecture humaine des spécifications et des passages signalés.

Le passage à l'échelle et son coût restent flous. DeepMind a mené l'analyse gratuitement, comme projet de recherche, sans donner le coût ni parler d'un produit commercial. Ses artefacts de vérification sont publiés en open source, et la méthode pourrait un jour toucher le micrologiciel de dispositifs médicaux ou les logiciels de réseaux électriques.