A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

Ce papier présente Preguss, un cadre modulaire qui combine l'analyse statique et les grands modèles de langage pour générer automatiquement des spécifications formules et vérifier l'absence d'erreurs d'exécution dans de grands programmes, réduisant ainsi l'effort de vérification humaine de 80,6 % à 88,9 %.

L'essentiel

Imaginez que vous essayez de vérifier si un avion est sûr de voler. Vous ne pouvez pas simplement regarder le plan d'ensemble d'un seul coup, car il y a des milliers de pièces, de câbles et de circuits. Si vous faites une erreur de calcul sur un petit boulon, l'avion pourrait tomber.

C'est exactement le problème que rencontrent les informaticiens quand ils essaient de prouver mathématiquement que de grands logiciels (comme ceux qui contrôlent des satellites ou des systèmes bancaires) ne vont pas planter.

Voici l'histoire de Preguss, présenté dans cet article, expliquée simplement.

1. Le Problème : L'usine de détection d'erreurs qui crie "Au feu !" trop souvent

Les logiciels sont écrits en langage humain (le code), mais les ordinateurs ne comprennent que des maths. Pour vérifier un logiciel, on utilise deux types d'outils :

• Les détecteurs automatiques (les "radars") : Ils scannent le code et disent : "Attention, ici, il y a un risque de division par zéro !" ou "Attention, ici, une mémoire pourrait être illisible !".
  • Le problème : Ces radars sont très prudents. Ils crient souvent "Au feu !" alors qu'il n'y a que de la vapeur. Ce sont de fausses alarmes. Pour un logiciel de 1000 lignes, ils peuvent en trouver des centaines. Un humain doit alors vérifier manuellement chacune d'elles pour dire "Non, c'est faux, tout va bien". C'est épuisant et lent.
• Les vérificateurs mathématiques (les "juges") : Ils peuvent prouver avec certitude qu'un code est sûr, mais ils ont besoin d'un guide. Ils ont besoin de règles écrites par un humain (ex: "Cette fonction ne peut recevoir que des nombres positifs"). Sans ces règles, le juge est aveugle.

2. La Solution : Preguss, le chef d'orchestre intelligent

Les chercheurs ont créé Preguss (un acronyme pour Potential Runtime Error-Guided Specification Synthesis). C'est un système qui utilise l'Intelligence Artificielle (les grands modèles de langage, ou LLM) pour combler le fossé entre les radars et les juges.

Voici comment Preguss fonctionne, avec une analogie :

L'Analogie du "Détective et du Traducteur"

Imaginez que vous avez un livre de 1000 pages écrit dans un code secret, et un détective (le radar) qui vous dit : "Il y a un problème potentiel à la page 450 !"

• L'approche ancienne (sans Preguss) : On donne tout le livre à l'IA et on lui dit : "Traduis-moi les règles de sécurité pour tout le livre". L'IA se perd, elle oublie des détails, et elle donne des règles trop vagues ou fausses.
• L'approche Preguss (Diviser pour régner) :
  1. Diviser (Le Chef d'orchestre) : Preguss ne regarde pas tout le livre d'un coup. Il prend la page 450 (l'erreur signalée) et regarde uniquement les 10 lignes autour, plus les fonctions qui appellent cette ligne. Il découpe le problème en petits morceaux gérables, comme des pièces de puzzle.
  2. Conquérir (Le Traducteur IA) : Pour chaque petit morceau, Preguss demande à l'IA : "Voici l'erreur suspecte. Quelle est la règle exacte qui empêcherait cette erreur de se produire ici ?".
     • L'IA agit comme un traducteur : elle transforme l'alerte du détective ("Attention, risque de crash ici") en une règle mathématique précise ("Il faut que la variable X soit supérieure à 0").
  3. Le Bouclier (La Vérification) : Preguss prend cette nouvelle règle et la donne au "Juge" (le vérificateur mathématique). Si le juge dit "C'est bon, la règle prouve qu'il n'y a pas d'erreur", alors le problème est résolu ! Si le juge dit "Je ne suis pas sûr", Preguss demande à l'IA d'affiner sa règle, un peu comme un professeur qui aide un élève à corriger son devoir.

3. Pourquoi c'est révolutionnaire ?

Jusqu'à présent, vérifier un gros logiciel prenait des mois de travail humain. Preguss change la donne de trois façons :

• Il ne se perd pas : En découpant le problème en petits morceaux (comme manger un éléphant bouchée par bouchée), l'IA ne se noie pas dans la quantité d'informations.
• Il vise juste : Au lieu de deviner des règles au hasard, Preguss utilise les alertes précises du détective pour guider l'IA. C'est comme si on disait à l'IA : "Ne cherche pas n'importe quoi, cherche la solution à ce problème précis".
• Il économise du temps humain : Dans les tests, Preguss a réussi à automatiser la vérification de logiciels de plus de 1000 lignes (ce qui est énorme pour ce type de tâche). Il a réduit le travail humain de 80% à 90%. Au lieu de vérifier 100 fausses alarmes, un humain n'en a plus que quelques-unes à vérifier.

4. Un exemple concret : Le vaisseau spatial

Les chercheurs ont testé Preguss sur un logiciel de contrôle d'un vaisseau spatial (1280 lignes de code).

• Le système a trouvé 6 vraies erreurs (des bugs réels) que les développeurs n'avaient pas vus.
• Il a prouvé que le reste du logiciel était sûr, sans que les humains aient à écrire des centaines de règles complexes.

En résumé

Preguss est comme un assistant super-puissant qui aide les ingénieurs à vérifier la sécurité des logiciels. Il prend les alertes confuses des outils automatiques, utilise l'IA pour inventer les règles mathématiques nécessaires, et prouve que le logiciel ne va pas planter.

C'est une étape majeure vers l'objectif ultime : des logiciels aussi sûrs que l'air que nous respirons, vérifiés automatiquement, même pour les systèmes les plus complexes.

Résumé technique

Voici un résumé technique détaillé de l'article « A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs », présentant le framework Preguss.

1. Problématique et Contexte

La vérification formelle automatisée de logiciels et matériels à grande échelle est un objectif majeur, mais difficile à atteindre. Les méthodes traditionnelles de vérification déductive (comme Frama-C/Wp) nécessitent des spécifications formelles (préconditions, postconditions, invariants de boucle) pour prouver l'absence d'erreurs d'exécution (RTE) et la correction fonctionnelle. Cependant, la synthèse de ces spécifications repose encore largement sur l'expertise humaine, ce qui est prohibitif pour des projets dépassant le millier de lignes de code (LoC).

Les récentes tentatives d'utiliser les Grands Modèles de Langage (LLM) pour automatiser cette synthèse se heurtent à deux limites majeures :

1. Limites de contexte : Les LLM peinent à traiter des programmes entiers en une seule fois en raison de la longueur des contextes et de leur difficulté à localiser les informations pertinentes dans de vastes bases de code.
2. Complexité interprocédurale : La vérification de programmes complexes nécessite des spécifications interprocédurales (contrats entre fonctions). Les approches actuelles génèrent souvent des spécifications intraprocedurales isolées ou des contrats interprocéduraux maladroits (par exemple, des préconditions trop restrictives qui génèrent de faux positifs).

L'objectif est donc de développer une méthode capable de générer automatiquement des spécifications formelles de haute qualité pour des programmes réels de grande taille (plus de 1000 LoC), en minimisant l'intervention humaine.

2. Méthodologie : Le Framework Preguss

Preguss (Potential Runtime Error-Guided Specification Synthesis) est un framework modulaire et fin qui combine l'analyse statique et la vérification déductive selon une stratégie « diviser pour régner » en deux phases synergiques.

Phase 1 : Construction et Priorisation des Unités de Vérification (Diviser)

Au lieu de traiter le programme monolithiquement, Preguss le décompose en Unités de Vérification (V-Units) gérables.

• Guidage par les erreurs potentielles (RTE) : Un analyseur statique (basé sur l'interprétation abstraite, ex: Frama-C/Eva) scanne le code pour détecter les risques d'erreurs d'exécution (divisions par zéro, débordements, accès mémoire invalides) et génère des assertions de garde (guard assertions).
• Construction du graphe d'appel : Le framework construit un graphe d'appel du programme.
• Création des V-Units : Chaque assertion de garde devient le cœur d'une V-Unit, encapsulant la fonction hôte et ses fonctions appelées (callee).
• Priorisation : Les V-Units sont organisées dans une file d'attente selon un ordre total :
  • Vérification ascendante (bottom-up) : Les fonctions appelées sont vérifiées avant leurs appelants pour garantir que leurs contrats (postconditions) sont disponibles.
  • Ordre linéaire : Pour les assertions au sein d'une même fonction, l'ordre suit la séquence d'instructions.

Phase 2 : Synthèse Fine des Spécifications Interprocédurales (Conquérir)

Pour chaque V-Unit, un agent LLM génère itérativement les spécifications nécessaires, guidé par les retours du vérificateur déductif.

• Stratégie différenciée :
  • Fonction Hôte : Le LLM génère des préconditions et des invariants de boucle pour la fonction cible, en se basant uniquement sur le contexte local pour éviter les contraintes excessives.
  • Fonctions Appelées (Callees) : Le LLM génère des postconditions pour les fonctions appelées. Il est explicitement interdit de générer des préconditions pour les fonctions appelées afin d'éviter la propagation de contraintes trop fortes (over-constrained) qui pourraient fausser la vérification.
• Boucle de raffinement (Feedback-Driven) :
  1. Le vérificateur (Frama-C/Wp) tente de prouver l'assertion de garde avec les spécifications actuelles.
  2. Si l'échec survient (statut unknown), le vérificateur renvoie des obligations de preuve (proof obligations).
  3. Le LLM analyse ces obligations pour diagnostiquer l'échec et propose de nouvelles spécifications.
  4. Un mécanisme de correction syntaxique et sémantique filtre les spécifications invalides ou non satisfaisables.
• Terminaison : Le processus s'arrête lorsque l'assertion est prouvée (true) ou après un nombre maximal d'itérations. Les assertions non résolues sont classées comme hypothèses nécessitant une revue humaine.

3. Contributions Clés

1. Concept de Synthèse Guidée par les RTE : Introduction d'une nouvelle approche où les alertes d'erreurs d'exécution générées par l'analyse statique servent de cibles précises pour guider le LLM, plutôt que de demander une synthèse aveugle de spécifications.
2. Framework Preguss : Le premier méthode automatisée capable de prouver l'absence d'erreurs d'exécution (RTE-freeness) sur des programmes réels de plus de 1000 LoC avec un effort humain marginal.
3. Jeu de Données Open Source : Création d'un ensemble de données contenant des programmes C réels annotés avec des spécifications générées par Preguss et validées par des experts.
4. Preuve de Scalabilité : Démonstration que l'approche diviser-conquérir permet de surmonter les limites de contexte des LLM et de gérer les hiérarchies d'appels complexes.

4. Résultats Expérimentaux

Les évaluations ont été menées sur des benchmarks standards (Frama-C-Problems) et quatre projets réels (Contiki, X509-parser, SAMCODE, Atomthreads).

• Performance vs. État de l'art : Sur le benchmark Frama-C-Problems, Preguss a réussi à vérifier 79,7 % des programmes (46 sur 51), surpassant largement AutoSpec (32,7 %) et AutoSpecRte (41,8 %).
• Échelle et Efficacité : Pour les projets réels (>1000 LoC), Preguss a atteint un taux de réussite moyen de 78,1 % à 94,7 % pour les unités de vérification.
• Réduction de l'effort humain : L'outil a permis de réduire l'effort de vérification humaine de 80,6 % à 88,9 % en termes de nombre de spécifications nécessitant une intervention manuelle.
• Détection de Bugs Réels : Dans le système de contrôle spatial SAMCODE (1280 LoC), Preguss a aidé à identifier 6 RTE réels (accès à des variables non initialisées) qui ont ensuite été confirmés par les développeurs.
• Coût : Bien que le coût d'inférence LLM soit plus élevé que les approches baselines (en raison du raffinement itératif), il reste marginal par rapport au temps d'expertise humaine économisé.

5. Signification et Impact

Cet article marque une avancée significative vers l'automatisation de la vérification formelle de logiciels critiques à grande échelle.

• Synergie Analyse/Vérification : Il démontre que l'intégration étroite entre l'analyse statique (pour la détection de risques) et la vérification déductive (pour la preuve) est supérieure à l'utilisation isolée des LLM.
• Pragmatisme : En se concentrant sur la preuve de l'absence d'erreurs d'exécution (RTE) plutôt que sur la spécification fonctionnelle complète, l'approche contourne la difficulté de modéliser le comportement exact de programmes complexes, tout en garantissant la sécurité.
• Faisabilité Industrielle : La capacité à traiter des milliers de lignes de code avec une intervention humaine réduite rend la vérification formelle accessible pour des projets industriels réels, comme les systèmes embarqués et spatiaux.

En résumé, Preguss transforme la vérification formelle d'une tâche manuelle fastidieuse en un processus semi-automatisé efficace, capable de gérer la complexité des systèmes modernes grâce à une architecture intelligente de décomposition de problèmes et de raffinement guidé par les preuves.