Verification Modulo Tested Library Contracts

1. Problématique et Contexte

La vérification formelle complète de grands programmes logiciels reste un défi majeur. Bien que les techniques de synthèse d'invariants inductifs et de contrats existent, elles ne parviennent pas à passer à l'échelle (scalabilité) pour des bases de code complexes, notamment lorsqu'elles impliquent l'utilisation de bibliothèques externes massives. L'annotation manuelle de ces bibliothèques avec des contrats formels forts est souvent trop coûteuse, voire impossible.

Les auteurs proposent une approche pragmatique : relâcher les garanties de vérification formelle pour les bibliothèques afin de permettre une automatisation complète et scalable pour les programmes clients qui les utilisent.

Le problème central (VMTLC) :
Étant donné un programme client $C$ utilisant une bibliothèque $L$, l'objectif est de synthétiser un ensemble de contrats formels $\Pi$ pour les méthodes de $L$ tels que :

1. Le client $C$ est prouvé formellement correct en supposant que les contrats $\Pi$ sont vrais.
2. Les contrats $\Pi$ passent un test exhaustif généré par un moteur de test déterministe (qui teste la bibliothèque contre ces contrats), sans trouver de violation.

L'idée clé est de remplacer la preuve formelle de la bibliothèque par une validation par test intensive, tout en conservant la preuve formelle du client.

2. Contributions Clés

Le papier introduit plusieurs concepts et mécanismes techniques novateurs :

A. Contrats Contextuels (Contextual Contracts)

Contrairement aux contrats modulaires classiques qui doivent être vrais dans tous les états possibles et pour toutes les entrées, les contrats contextuels ne sont valables que dans le contexte spécifique du programme client.

• Avantage : Ils sont souvent plus simples à inférer et plus forts (plus restrictifs) car ils exploitent les préconditions implicites imposées par le client (ex: le client n'appelle jamais la bibliothèque avec des entrées négatives).
• Exemple : Si un client n'insère que des entiers positifs dans une structure de données, un contrat contextuel pour une méthode de suppression peut garantir que la valeur renvoyée est positive, ce qui serait faux pour un contrat modulaire général.

B. Cadre d'Apprentissage Guidé par les Contre-exemples (CEGS)

Les auteurs proposent un cadre itératif combinant :

• Un solveur de Clauses de Horn Contraintes (CHC) capable de généraliser (pour éviter le surapprentissage).
• Un moteur de test (fuzzer) qui valide les contrats synthétisés.
• Un mécanisme d'apprentissage ICE (Implication, Contre-exemple, Exemple) qui intègre les résultats du test comme des « exemples positifs » pour guider le solveur.

C. Utilisation des LLMs dans l'Apprentissage

Le cadre est agnostique quant à l'algorithme d'apprentissage. Les auteurs montrent comment intégrer des Grands Modèles de Langage (LLM) comme composant d'apprentissage ICE. Le LLM propose des contrats et des invariants basés sur la documentation et le code, et est corrigé itérativement par les contre-exemples fournis par le vérificateur et le testeur.

3. Méthodologie et Algorithme

La solution est implémentée dans un outil nommé Dualis. Le processus fonctionne en boucle de synthèse guidée par les contre-exemples :

1. Génération de Conditions de Vérification (VC) : Le programme client est converti en un système de Clauses de Horn Contraintes (CHC). Ces CHC contiennent des « trous » (predicats inconnus) pour les invariants du client et les contrats de la bibliothèque.
2. Synthèse Initiale : Un solveur CHC généralisant (basé sur l'apprentissage ICE, par exemple HornICE ou un LLM) tente de trouver des prédicats qui rendent les CHC valides.
3. Validation par Test :
   • Mode Modulaire : Le testeur génère des tests pour chaque méthode de la bibliothèque indépendamment pour vérifier si elle viole le contrat synthétisé.
   • Mode Contextuel : Le testeur exécute le programme client complet avec différentes entrées pour vérifier si les appels aux méthodes de la bibliothèque respectent les contrats contextuels.
4. Boucle d'Apprentissage :
   • Si le test échoue (violation trouvée), le cas de test est converti en un exemple positif (un cas que le contrat doit couvrir).
   • Ces exemples sont ajoutés à l'ensemble d'apprentissage du solveur ICE.
   • Le solveur ré-itère pour trouver de nouveaux contrats qui satisfont à la fois les CHC (vérification du client) et les nouveaux exemples positifs (résistance aux tests).
5. Terminaison : La boucle s'arrête lorsque le client est prouvé correct ET que le testeur ne trouve aucune violation pour les contrats synthétisés.

Rôle des LLMs : Ils peuvent être utilisés pour proposer des formules atomiques de base ou des contrats entiers. Le système combine ensuite ces propositions avec des solveurs symboliques pour garantir la correction logique et éviter les contre-exemples.

4. Résultats de l'Évaluation

Les auteurs ont évalué leur approche sur une suite de 43 benchmarks C++ utilisant des bibliothèques de structures de données open-source (Folly, Abseil, Android, SV-COMP). Ces benchmarks sont trop complexes pour les outils d'automatisation actuels (comme SeaHorn), qui échouent sur la plupart d'entre eux.

Résultats principaux :

• Efficacité : L'approche VMTLC a réussi à vérifier la majorité des benchmarks.
  • Avec un apprentissage basé sur LLM, 38/43 contrats modulaires et 41/43 contrats contextuels ont été synthétisés avec succès.
  • Les approches purement symboliques (HornICE) ont eu moins de succès en raison de limitations dans la grammaire des prédicats, mais ont été améliorées par l'hybridation avec les LLM.
• Contrats Contextuels vs Modulaires : Les contrats contextuels sont systématiquement plus simples, plus petits et plus rapides à synthétiser que les contrats modulaires. Ils permettent de résoudre plus de problèmes car ils n'ont pas besoin de couvrir des états inaccessibles au client.
• Validité : Une vérification manuelle et automatique a confirmé que tous les contrats synthétisés étaient corrects.
• Robustesse : L'outil a été testé sur des programmes mutés (incorrects). Bien que les contrats contextuels puissent parfois accepter des programmes incorrects (si le bug est dans un chemin de test très rare), l'approche globale rejette la plupart des programmes erronés que le testeur seul ne pourrait pas détecter.

5. Signification et Conclusion

Ce travail représente une avancée significative dans le domaine de la vérification logicielle en proposant un nouveau point de compromis dans l'espace de conception :

• Scalabilité : En abandonnant la vérification formelle complète des bibliothèques (remplacée par un test rigoureux), on permet la vérification formelle de programmes clients complexes utilisant de grandes bibliothèques.
• Pragmatisme : L'approche reconnaît que la vérification formelle totale est souvent hors de portée, mais que la combinaison de la preuve formelle (pour le client) et du test (pour la bibliothèque) offre un niveau de confiance élevé et pratique.
• Innovation Technique : L'intégration réussie des LLMs dans un cadre d'apprentissage ICE pour la synthèse de contrats et d'invariants ouvre la voie à de nouvelles méthodes hybrides combinant l'intuition des modèles de langage et la rigueur des solveurs formels.

En résumé, Dualis démontre qu'il est possible d'automatiser la vérification de programmes utilisant de grandes bibliothèques en synthétisant des contrats adaptés (modulaires ou contextuels) qui sont validés par une boucle de test et de preuve conjointe.