VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

Le papier présente VeriStruct, un cadre novateur qui étend la vérification automatique assistée par l'IA aux modules de structures de données complexes en Verus en orchestrant la génération de spécifications et en corrigeant les erreurs de syntaxe, réussissant ainsi à vérifier 99,2 % des fonctions sur un ensemble de test de onze modules Rust.

L'essentiel

Imaginez que vous construisez une ville entière avec des robots. Ces robots sont incroyablement rapides et créatifs : ils peuvent écrire le code informatique qui fait fonctionner les feux de circulation, les systèmes bancaires ou les applications de messagerie. C'est ce qu'on appelle l'IA générative.

Mais il y a un gros problème : ces robots sont comme des enfants brillants mais distraits. Ils construisent des gratte-ciels magnifiques, mais ils oublient parfois de vérifier si les fondations sont solides. Un petit défaut dans le code peut transformer un pont sécurisé en un pont qui s'effondre au premier vent.

C'est là qu'intervient VeriStruct, le sujet de l'article que vous avez lu. Voici comment cela fonctionne, expliqué simplement avec des analogies.

1. Le Problème : Le Robot qui oublie les règles

Dans le monde de l'informatique, pour prouver qu'un logiciel est sûr, on utilise des mathématiques rigoureuses (c'est la "vérification formelle"). C'est comme avoir un inspecteur du bâtiment qui vérifie chaque vis et chaque poutre avant d'autoriser l'ouverture d'un immeuble.

Le problème, c'est que pour que l'inspecteur travaille, il faut lui fournir un manuel d'instructions très précis (des "annotations"). Écrire ce manuel à la main est long, difficile et ennuyeux pour les humains.

Récemment, on a essayé de demander à l'IA (les robots) d'écrire ce manuel pour nous. Mais l'IA fait souvent des erreurs :

• Elle utilise un langage que l'inspecteur ne comprend pas.
• Elle oublie des règles cruciales pour des objets complexes (comme une "file d'attente" ou un "arbre" de données).
• Elle invente des règles qui semblent logiques mais qui sont mathématiquement fausses.

2. La Solution : VeriStruct, l'Architecte Chef de Chantier

VeriStruct n'est pas juste un robot qui écrit du code. C'est un système intelligent qui aide l'IA à devenir un architecte fiable. Il fonctionne comme un chef de chantier expérimenté qui supervise un apprenti (l'IA).

Voici les trois étapes clés de son travail, illustrées par une analogie de construction :

Étape A : Le Planificateur (Le Chef d'Orchestre)

Avant même de commencer à construire, VeriStruct demande à l'IA : "De quoi avons-nous besoin pour ce bâtiment ?"

• Si on construit un simple mur, il faut juste des briques.
• Si on construit un Ring Buffer (une sorte de roue de vélo où l'on stocke des données), il faut des choses plus complexes : une vue mathématique (comment la roue tourne), des règles de sécurité (ne pas dépasser la capacité), et des preuves que tout fonctionne ensemble.
• VeriStruct dit à l'IA : "Oublie les briques simples, concentre-toi sur la vue mathématique et les règles de sécurité." Cela évite de perdre du temps à demander à l'IA de faire des choses inutiles.

Étape B : La Génération avec Guides (L'Apprenti Guidé)

L'IA commence à écrire les règles. Mais comme elle ne connaît pas parfaitement le langage spécial de l'inspecteur (Verus), VeriStruct lui donne un livre de règles (des "guides de syntaxe") directement dans sa conversation.

• Au lieu de laisser l'IA deviner, on lui dit : "Pour décrire cette roue, imagine-la comme une liste de nombres, pas comme un tas de métal."
• Cela aide l'IA à créer une abstraction mathématique claire, comme si on dessinait un plan simplifié du bâtiment plutôt que de lister chaque grain de sable.

Étape C : Le Service de Réparation (Le Mécanicien de Précision)

C'est la partie la plus géniale. Souvent, l'IA fait une erreur. Par exemple, elle utilise une fonction qui modifie la réalité (comme ouvrir une porte) dans une règle qui doit rester théorique (comme dire "si la porte était fermée"). L'inspecteur (le vérificateur) crie : "Erreur !"

Au lieu de tout jeter, VeriStruct agit comme un mécanicien de Formule 1 :

1. Il écoute le bruit du moteur (le message d'erreur).
2. Il identifie le problème précis (ex: "Tu as utilisé une fonction interdite ici").
3. Il envoie un module de réparation spécialisé pour corriger exactement ce problème.
4. Il réessaie.

Ce cycle se répète jusqu'à ce que tout soit parfait. C'est comme si l'IA essayait, se trompait, recevait une correction ciblée, et recommençait jusqu'à ce que le bâtiment soit solide.

3. Les Résultats : Une Ville Sans Accidents

Les chercheurs ont testé VeriStruct sur 11 structures de données complexes (des files d'attente, des arbres, des verrous de sécurité, etc.).

• Sans VeriStruct (juste l'IA seule) : L'IA réussit à peine 4 fois sur 11. Elle se perd dans les détails.
• Avec VeriStruct : Le système réussit 10 fois sur 11. Il a vérifié 99,2 % de toutes les fonctions avec succès.

C'est comme passer d'un chantier où la moitié des bâtiments s'effondrent à un chantier où presque tout est parfaitement sécurisé, le tout avec beaucoup moins d'intervention humaine.

En Résumé

VeriStruct est un cadre de travail qui transforme l'IA d'un "rédacteur créatif mais imprévisible" en un "ingénieur rigoureux".

• Il planifie ce qui est nécessaire.
• Il guide l'IA avec des règles claires.
• Il répare les erreurs pas à pas.

Grâce à cela, nous pouvons espérer un futur où le logiciel généré par l'IA est non seulement rapide à produire, mais aussi mathématiquement prouvé comme étant sûr, sans avoir besoin d'une armée de mathématiciens pour vérifier chaque ligne de code. C'est un pas géant vers une infrastructure numérique plus fiable.

Résumé technique

1. Problématique

L'essor des systèmes d'intelligence artificielle générative pose un double défi pour l'infrastructure logicielle critique : d'une part, ils facilitent la découverte de vulnérabilités par des acteurs malveillants ; d'autre part, le code généré ou assisté par l'IA introduit de nouveaux risques de bugs et de failles de sécurité. La vérification de programme formelle (program verification) est la méthode mathématique pour garantir l'absence de ces défauts, mais son adoption pratique est limitée par le coût humain élevé requis pour écrire des annotations logiques complexes (préconditions, postconditions, invariants, preuves auxiliaires).

Bien que des travaux récents aient démontré l'efficacité des grands modèles de langage (LLM) pour vérifier des fonctions isolées (algorithmes de base), la vérification de modules de structures de données reste un défi majeur. Contrairement aux fonctions simples, les structures de données nécessitent :

1. Des abstractions mathématiques (Views) pour raisonner sur l'état logique.
2. Des invariants de type (Type Invariants) qui doivent être préservés par toutes les opérations.
3. Une vérification conjointe de multiples méthodes sous un invariant partagé.

De plus, les LLMs peinent à maîtriser la syntaxe spécifique et la sémantique de vérification du langage Verus (une extension de Rust pour la vérification formelle), générant souvent des erreurs de syntaxe ou des appels à des fonctions exécutables dans des contextes de spécification interdits.

2. Méthodologie : Le Framework VeriStruct

Les auteurs proposent VeriStruct, un framework automatisé qui orchestre la génération et la réparation d'annotations de vérification pour des modules de structures de données en Rust/Verus. Le workflow s'articule autour d'un pipeline en deux étapes principales, piloté par un module de planification.

A. Entrées et Sorties

• Entrée : Le code source Rust de la structure de données (sans annotations) et une suite de tests unitaires illustrant le comportement attendu.
• Sortie : Une version annotée du code, vérifiée formellement par le compilateur Verus.

B. Étape 1 : Génération des Annotations (GenAnnos)

Cette étape utilise un module Planificateur (Planner) pour déterminer quels composants de vérification sont nécessaires pour une tâche donnée, évitant ainsi des générations inutiles. Le planificateur orchestre quatre modules spécialisés, invoqués séquentiellement selon le plan :

1. Module View : Génère une abstraction mathématique (trait View) qui mappe la structure de données concrète vers un objet logique (ex: séquences, ensembles) pour faciliter le raisonnement.
2. Module Invariant de Type : Génère les invariants logiques que toute instance de la structure doit satisfaire (ex: bornes des indices, capacité positive).
3. Module Spécification : Génère les fonctions de spécification, les préconditions (requires) et les postconditions (ensures).
4. Module Preuve : Génère les blocs de preuve (proof blocks) et les invariants de boucle nécessaires.

Stratégie d'amélioration : Pour chaque module, le système génère plusieurs échantillons (sampling) et sélectionne celui qui maximise le nombre de fonctions vérifiées. Un module de raffinement des Views est également intégré pour éviter les abstractions triviales (comme un produit cartésien de tous les champs) et encourager des abstractions conceptuelles plus puissantes.

C. Étape 2 : Réparation des Annotations (RepairAnnos)

La génération initiale échoue souvent à cause d'erreurs de syntaxe Verus ou de sémantique. VeriStruct implémente une boucle de réparation itérative :

1. Le code est soumis au vérificateur Verus.
2. Si des erreurs sont détectées, elles sont analysées via un appariement de motifs (regex) pour identifier la classe d'erreur.
3. Un module de réparation dédié est invoqué pour corriger spécifiquement cette erreur (ex: remplacer un appel à une fonction exécutable par une fonction de spécification, corriger les problèmes de mutabilité Rust, ou renforcer les postconditions suite à un échec de test).
4. Le processus se répète jusqu'à succès ou épuisement du budget d'itérations.

3. Contributions Clés

1. Nouveau Workflow pour les Structures de Données : Extension de la vérification assistée par IA au-delà des fonctions uniques vers des modules complets nécessitant des abstractions, des invariants de type et une vérification conjointe.
2. Implémentation VeriStruct : Un outil fonctionnel intégrant un planificateur, des modules de génération spécialisés et un système de réparation itératif.
3. Guidage Syntaxique et Sémantique : Intégration de directives syntaxiques Verus dans les prompts et création de modules de réparation spécifiques pour corriger les erreurs de sémantique de vérification (ex: confusion entre fonctions spec et exécutables).
4. Évaluation Rigoureuse : Validation sur 11 benchmarks réels de structures de données Rust.

4. Résultats Expérimentaux

L'évaluation a été menée sur 11 modules de structures de données (Ring Buffer, Treemap, Bitmap, RwLock, etc.), totalisant 129 fonctions à vérifier.

• Performance de VeriStruct :
  • Succès sur 10 des 11 benchmarks.
  • Vérification réussie de 128 fonctions sur 129 (99,2 %).
  • Réduction significative de l'effort manuel d'annotation.
• Comparaison avec les Baselines :
  • Une approche de base (LLM simple itératif sans workflow structuré) n'a réussi que 4 benchmarks et 52 fonctions.
  • Claude Code (agent IA autonome avec accès aux outils) a vérifié 102 fonctions sur 8 benchmarks, restant inférieur à VeriStruct tout en consommant plus de tokens.
• Efficacité : VeriStruct atteint des résultats supérieurs avec un coût en tokens comparable ou inférieur aux agents autonomes, grâce à sa structure modulaire et son planificateur.

5. Signification et Perspectives

Ce travail représente une avancée majeure vers l'automatisation de la vérification formelle à grande échelle. En démontrant que les LLMs peuvent gérer la complexité des structures de données (abstractions mathématiques et invariants) lorsqu'ils sont guidés par un workflow structuré, VeriStruct réduit la barrière à l'entrée pour l'adoption de la vérification formelle dans l'industrie logicielle (notamment avec Rust).

Perspectives futures :

• Intégration de la Génération Augmentée par Récupération (RAG) pour extraire des lemmes utiles des bibliothèques standards.
• Extension à la vérification de structures de données concurrentes complexes via l'algèbre des ressources.
• Utilisation de l'Apprentissage par Renforcement (RL) pour optimiser la recherche de spécifications et de preuves.
• Automatisation complète de la génération des tests unitaires pour éliminer la dépendance aux tests fournis manuellement.

En résumé, VeriStruct transforme la vérification de programmes d'une tâche artisanale et coûteuse en un processus semi-automatisé robuste, capable de produire des bibliothèques de code vérifié réutilisables.