Les LLM automatisent la vérification formelle de bibliothèques open source à grande échelle

Les développeurs logiciels ont longtemps souffert du coût élevé de la vérification formelle, une méthode qui prouve mathématiquement que le code est exempt de bugs spécifiques. Une récente collaboration entre une équipe de recherche en IA et Theorem montre que les grands modèles de langage peuvent désormais automatiser ce processus à grande échelle. En utilisant Claude pour analyser des binaires compilés, l'équipe a réussi à prouver des propriétés de sécurité pour plus de 100 bibliothèques open source réelles, marquant un changement significatif dans la manière dont la correction logicielle peut être garantie.

Ce qui s'est passé

Le projet s'est concentré sur l'application de la vérification formelle aux logiciels de production au niveau du code d'assemblage, ciblant spécifiquement l'architecture RISC-V. L'équipe a sélectionné 123 bibliothèques open source issues de l'initiative OSS-Fuzz de Google, qui contient déjà des milliers de points d'entrée rédigés par des développeurs, conçus pour planter lorsque des bugs sont détectés. Au lieu de s'appuyer sur des tests par force brute, l'équipe a demandé à Claude de prouver que ces programmes ne planteraient jamais pour toute entrée inférieure à 64 Mo, en supposant un binaire statique mono-thread fonctionnant sous Linux.

Sur une période de quelques semaines, Claude a généré des preuves pour 239 points d'entrée à travers ces bibliothèques. Les preuves résultantes totalisaient environ 180 millions de lignes de code Rocq, avec des preuves individuelles atteignant en moyenne environ 600 000 lignes. Durant ce processus, le modèle n'a pas seulement généré les preuves, mais a également identifié et corrigé des bugs qui persistaient malgré des billions de tests précédents. Cet effort représente la première application à grande échelle de l'IA pour vérifier formellement des logiciels de production au niveau de l'assemblage.

Pour rendre ces résultats accessibles, l'équipe publie un sous-ensemble des preuves ainsi que les sémantiques RISC-V et système d'exploitation utilisées dans l'analyse. Theorem propose également d'exécuter cette chaîne de vérification pour d'autres projets open source et a publié une compétence (skill) Claude pour aider les développeurs à commencer à vérifier leur propre code. Cette approche fait passer la vérification formelle d'une pratique de niche réservée aux systèmes critiques comme l'avionique à un outil plus largement applicable au développement logiciel général.

Comment cela fonctionne

La vérification formelle nécessite de traduire le code en un modèle mathématique et de prouver qu'il adhère à un ensemble de règles de sécurité. Le défi principal a toujours été de définir ce que signifie « correct » pour des logiciels complexes. Dans ce projet, l'équipe a contourné le besoin de spécifications manuelles en convertissant les tests de fuzzing existants en spécifications formelles. Les tests de fuzzing génèrent des entrées aléatoires pour trouver des plantages, mais ils ne peuvent garantir que chaque chemin est testé. La nouvelle méthode définit la spécification comme « cette suite de tests réussit toujours », appliquée aux instructions RISC-V compilées plutôt qu'au code source.

Claude opère en analysant les artefacts exécutables et les sémantiques formelles du jeu d'instructions RISC-V et du comportement des processus Linux fournies par Theorem. Le modèle génère des preuves massives démontrant qu'aucune erreur de sécurité mémoire ou échec d'assertion ne peut se produire dans les conditions définies. Ces preuves sont ensuite validées par le vérificateur de preuves Rocq, un noyau de confiance qui garantit la validité de la logique mathématique. Parce que le vérificateur valide la preuve automatiquement, les développeurs n'ont pas besoin de revoir manuellement les millions de lignes de code générées, ne faisant confiance qu'aux modèles sous-jacents et au vérificateur lui-même.

Détails clés

• Le projet a vérifié 239 points d'entrée à travers 123 bibliothèques open source issues de l'initiative OSS-Fuzz.
• Claude a généré environ 180 millions de lignes de code de preuve Rocq, avec des preuves typiques atteignant 600 000 lignes.
• La vérification ciblait le code d'assemblage RISC-V, prouvant l'absence de plantages pour les entrées inférieures à 64 Mo sous Linux.
• Le modèle a découvert et corrigé des bugs qui avaient survécu à des billions de tests de fuzzing précédents.
• La confiance est placée dans les modèles formels RISC-V et Linux, les énoncés de théorèmes et le vérificateur de preuves Rocq.
• Theorem publie une compétence Claude pour aider les développeurs à appliquer des flux de travail de vérification similaires à leurs propres projets.

Pourquoi c'est important

Pour les ingénieurs logiciels, ce développement abaisse la barrière d'entrée pour la vérification formelle, qui a historiquement nécessité des années d'efforts spécialisés d'experts. En automatisant la création de preuves, les LLM rendent possible l'application de garanties de sécurité rigoureuses aux bibliothèques et applications quotidiennes. Ce changement permet aux équipes de dépasser la correction réactive de bugs et le fuzzing proactif vers un modèle où les composants critiques sont mathématiquement prouvés sûrs contre des classes entières de vulnérabilités, telles que les erreurs de sécurité mémoire.

La capacité de vérifier des binaires compilés plutôt que simplement le code source est particulièrement significative. Cela signifie que les propriétés de sécurité peuvent être garanties pour les artefacts exécutables réellement déployés en production, tenant compte des comportements du compilateur et des interactions de bas niveau. À mesure que les capacités des modèles s'améliorent et que des sémantiques pour plus d'architectures deviennent disponibles, cette approche pourrait devenir une partie standard du cycle de vie de développement logiciel, réduisant le risque d'exploits dans les dépendances open source largement utilisées.

Ce que vous pouvez faire

• Explorez le sous-ensemble publié des preuves et la sémantique RISC-V pour comprendre la structure de la vérification formelle générée par l'IA.
• Essayez la nouvelle compétence Claude publiée par Theorem pour commencer à expérimenter des flux de travail de vérification sur vos propres bases de code.
• Passez en revue les tests de fuzzing existants de votre projet, car ils peuvent servir de base aux spécifications formelles lors de futurs efforts de vérification.
• Envisagez d'intégrer des étapes de vérification formelle pour les bibliothèques critiques de votre chaîne de dépendances, surtout celles traitant des entrées non fiables.
• Restez informé des développements concernant les sémantiques formelles RISC-V et Linux, car l'élargissement de ces modèles augmentera la portée des logiciels vérifiables.
• Évaluez si les hypothèses de binaires statiques mono-thread s'appliquent à vos projets actuels comme point de départ pour la vérification.