Natural Language based Specification and Verification

Résumé technique : Spécification et vérification basées sur le langage naturel (NLForge)

Énoncé du problème
Les violations de sécurité de la mémoire dans les programmes C et C++ — telles que les déréférencements invalides, les utilisations après libération et les accès hors limites — restent une source principale de vulnérabilités logicielles. Ces erreurs découlent souvent d'interactions interprocédurales complexes impliquant l'allocation, la libération, l'initialisation et l'aliasage, que les outils d'analyse statique traditionnels peinent à vérifier à grande échelle. Bien que les modèles de langage de grande taille (LLM) aient démontré de fortes capacités à identifier des bugs, ils font face à des défis majeurs pour prévenir l'introduction de nouvelles vulnérabilités par la vérification formelle. Les pipelines de vérification existants nécessitent généralement des spécifications dans des langages formels rigides (par exemple, invariants de boucle, préconditions/postconditions), créant une charge d'annotation élevée. Les tentatives antérieures d'utiliser des LLM pour synthétiser ces spécifications formelles ont montré un succès limité. De plus, des benchmarks récents indiquent que les performances des LLM chutent précipitamment lors du passage de la vérification d'une seule fonction à un raisonnement compositionnel multi-fonctions, principalement en raison des limitations de la fenêtre de contexte et de la difficulté à maintenir une cohérence sémantique globale.

Méthodologie : NLForge
Les auteurs proposent NLForge, un cadre de vérification compositionnel qui exploite les LLM pour générer et raisonner sur des spécifications en langage naturel plutôt que sur des artefacts formels rigides. Le système opère sur une analyse ascendante, priorisant les fonctions appelées (callee-first) du graphe d'appels du programme.

1. Architecture du pipeline :

   • Prétraitement : Le système extrait les définitions de fonctions, les signatures et les sites d'appel du code C/C++ pour construire un graphe d'appels. Les appels non résolus sont gérés via des stubs externes.
   • Analyse ascendante : Le cadre exécute une séquence de passes d'analyse sur le graphe d'appels dans l'ordre topologique (traitant les fonctions appelées avant les fonctions appelantes).
   • Résumés en langage naturel : Au lieu de générer de la logique formelle, le LLM produit des résumés structurés en langage naturel (encodés sous forme de JSON typé avec des descriptions en langage naturel) pour des propriétés spécifiques :
     • Allocation/Libération/Initialisation : Résumé de la création d'objets du tas, des effets de libération et de l'initialisation des paramètres de sortie.
     • Contrats de sécurité mémoire : Inférence de préconditions (par exemple, non-nul, non-libéré, taille du tampon) et de postconditions.
     • Résumés de fuites et d'entiers : Suivi des obligations non résolues et des risques de débordement d'entiers.
   • Vérification compositionnelle : Lors de la passe de vérification finale, le LLM analyse une fonction en utilisant ses propres préconditions inférées et les résumés en langage naturel de ses fonctions appelées. Le modèle agit comme un agent de raisonnement qui maintient un état d'exécution latent, vérifiant les exigences de sécurité par rapport aux contrats des fonctions appelées sans intégrer l'implémentation complète de ces dernières.

2. Raison d'être de la conception :
   Cette approche est motivée par l'observation que les LLM, entraînés sur du code et de la documentation, peuvent générer, interpréter et affiner des résumés en langage naturel de manière plus cohérente que des notations formelles rigides. Cette conception vise à décomposer le problème de vérification en résumés sémantiques réutilisables, permettant au modèle de raisonner sur une fonction sous des hypothèses explicitement énoncées concernant ses fonctions appelées, plutôt que de réanalyser le code source brut pour chaque appelant.

Contributions clés

• Cadre compositionnel : Un cadre de vérification interprocédurale ascendante pour C/C++ utilisant des LLM pour inférer et vérifier des propriétés de sécurité mémoire.
• Représentation intermédiaire en langage naturel : L'introduction de résumés sémantiques en langage naturel comme représentation intermédiaire pour la vérification, contrastant avec les travaux antérieurs axés sur la génération de spécifications formelles pour des vérificateurs symboliques externes.
• Pipeline d'analyse en étapes : Une décomposition du raisonnement sur la sécurité mémoire en résumés réutilisables (allocation, libération, initialisation et obligations côté appelant) qui sont renvoyés au LLM dans les étapes suivantes.
• Évaluation empirique : Une étude comparative du raisonnement compositionnel par rapport à une base de référence de type « whole-program prompting » non compositionnelle sur les benchmarks SV-COMP 2026.

Résultats
Les auteurs ont évalué NLForge sur un sous-ensemble des benchmarks de sécurité mémoire SV-COMP 2026 en utilisant quatre architectures de LLM (Claude Sonnet-4.6, GPT-5.4, Gemini-3.1-flash-lite et Qwen3.5-27B-UD-Q4) et les ont comparés à des vérificateurs traditionnels (CPAchecker, Symbiotic, Ultimate Automizer).

• RQ1 (LLM en tant que vérificateurs) : L'analyse basée sur les LLM démontre un rappel et une couverture élevés, identifiant la plupart des vrais positifs (par exemple, Sonnet-4.6 a atteint un rappel de 99,8 % sur valid-memsafety). Cependant, ils produisent significativement plus de faux positifs que les outils traditionnels et ne peuvent pas encore servir de vérificateurs autonomes et sûrs. Les outils traditionnels renvoient souvent « Inconnu » (UNK) pour les cas difficiles afin d'éviter les faux positifs, tandis que les LLM fournissent des réponses définitives avec des taux d'erreur plus élevés.
• RQ2 (Vérification compositionnelle) : L'approche compositionnelle surpasse nettement la base de référence non compositionnelle, en particulier sur des benchmarks complexes de flux de contrôle et de structures de données du monde réel.
  • Les exécutions compositionnelles ont augmenté les vrais positifs de 3 390 à 3 476 et réduit les faux négatifs de 301 à 216 sur l'ensemble des modèles.
  • L'amélioration a été la plus marquée pour les modèles plus petits (par exemple, Qwen3.5-27B-Q4 a vu ses faux négatifs passer de 218 à 97) et sur les benchmarks nécessitant un fort raisonnement interprocédural.
  • Les gains ont été moins cohérents sur les tests synthétiques et localisés de Juliet, où les modèles non compositionnels pouvaient exploiter directement des motifs locaux.

Signification et affirmations
L'article plaide pour un changement dans la manière dont les LLM sont utilisés en vérification : passer du traitement de ces derniers comme de simples générateurs d'artefacts formels pour des moteurs externes à leur utilisation en tant qu'agents de raisonnement sur des résumés structurés et réutilisables en langage naturel.

• Praticité : Le langage naturel sert de couche de spécification intermédiaire pratique permettant la vérification compositionnelle, en particulier pour les tâches où le « whole-program prompting » dépasse le budget de raisonnement du modèle ou sa fenêtre de contexte.
• Limitations : Les auteurs reconnaissent que l'informalité du langage naturel entraîne des problèmes d'étalonnage (plus de faux positifs) et que l'approche est sensible à la qualité des résumés générés ; les erreurs dans les résumés peuvent se propager et s'amplifier.
• Perspectives futures : Ce travail suggère que, bien que les LLM ne soient pas encore un remplacement pour la vérification formelle sûre, ils offrent une direction prometteuse pour une vérification de détection de bugs évolutive. Les travaux futurs devraient se concentrer sur l'amélioration de l'étalonnage, la combinaison des résumés avec des vérifications symboliques, et la gestion plus robuste de fonctionnalités complexes comme les appels indirects et les invariants de tas.

L'étude conclut que la question n'est pas seulement si les LLM peuvent vérifier la sécurité mémoire, mais sous quelles représentations et décompositions ils deviennent plus fiables, soulignant que le langage naturel peut efficacement combler le fossé entre la structure modulaire des programmes et les capacités de raisonnement des LLM.