Natural Language based Specification and Verification

Technische Samenvatting: Specificatie en Verificatie op Basis van Natuurlijke Taal (NLForge)

Probleemstelling
Schendingen van geheugenveiligheid in C- en C++-programma's—zoals ongeldige dereferenties, gebruik na vrijgave (use-after-free) en toegang buiten de grenzen—blijven een primaire bron van softwarekwetsbaarheden. Deze fouten vloeien vaak voort uit complexe interprocedurale interacties die allocatie, deallocatie, initialisatie en aliasing omvatten, en waar traditionele statische analysetools moeite mee hebben om op schaal verificatie uit te voeren. Hoewel Large Language Models (LLMs) sterke capaciteiten hebben aangetoond bij het identificeren van bugs, staan ze voor aanzienlijke uitdagingen bij het voorkomen van de introductie van nieuwe kwetsbaarheden via formele verificatie. Bestaande verificatiepijplijnen vereisen doorgaans specificaties in rigide formele talen (bijvoorbeeld loop-invarianten, pre-/post-condities), wat leidt tot een hoge last voor annotatie. Eerdere pogingen om LLMs te gebruiken voor het synthetiseren van deze formele specificaties hebben beperkt succes getoond. Bovendien geven recente benchmarks aan dat de prestaties van LLMs sterk dalen bij de overstap van verificatie van een enkele functie naar compositional, multi-functioneel redeneren, grotendeels vanwege beperkingen in het contextvenster en de moeilijkheid om globale semantische consistentie te handhaven.

Methodologie: NLForge
De auteurs stellen NLForge voor, een compositional verificatiekader dat LLMs benut om specificaties in natuurlijke taal te genereren en daarover te redeneren, in plaats van rigide formele artefacten. Het systeem werkt op een bottom-up analyse van de aanroepgraaf van het programma, waarbij eerst de callee wordt geanalyseerd.

1. Pijplijnarchitectuur:

   • Preprocessing: Het systeem haalt functiedefinities, handtekeningen en aanroepplaatsen uit C/C++-code om een aanroepgraaf te construeren. Onopgeloste aanroepen worden afgehandeld via externe stubs.
   • Bottom-Up Analyse: Het kader voert een reeks analysepasses uit over de aanroepgraaf in topologische volgorde (verwerking van callees voor callers).
   • Samenvattingen in Natuurlijke Taal: In plaats van formele logica te genereren, produceert de LLM gestructureerde samenvattingen in natuurlijke taal (gecodeerd als getypeerde JSON met beschrijvingen in natuurlijke taal) voor specifieke eigenschappen:
     • Allocatie/Vrijgave/Initialisatie: Samenvatten van heap-objectcreatie, effecten van deallocatie en initialisatie van uitgangsparameters.
     • Contracten voor Geheugenveiligheid: Afleiden van precondities (bijvoorbeeld niet-nul, niet-vrijgegeven, buffergrootte) en postcondities.
     • Samenvattingen voor Lekken en Integers: Het bijhouden van onopgeloste verplichtingen en risico's op integer-overflow.
   • Compositional Controle: In de laatste verificatiepass analyseert de LLM een functie met behulp van de eigen afgeleide precondities en de samenvattingen in natuurlijke taal van zijn callees. Het model fungeert als een redeneeragent die een latente uitvoeringstoestand handhaaft, waarbij het veiligheidsvereisten controleert tegenover contracten van callees zonder de volledige implementatie van de callee in te lijnen.

2. Ontwerprationale:
   Deze aanpak wordt gemotiveerd door de observatie dat LLMs, getraind op code en documentatie, samenvattingen in natuurlijke taal consistenter kunnen genereren, interpreteren en verfijnen dan rigide formele notaties. Dit ontwerp beoogt het verificatieprobleem te decomponeren in herbruikbare semantische samenvattingen, waardoor het model kan redeneren over een functie onder expliciet gestelde aannames over zijn callees, in plaats van elke keer de ruwe broncode opnieuw te analyseren voor elke caller.

Belangrijkste Bijdragen

• Compositional Kader: Een bottom-up interprocedurale verificatiekader voor C/C++ dat LLMs gebruikt om eigenschappen van geheugenveiligheid af te leiden en te verifiëren.
• Intermediaire Representatie in Natuurlijke Taal: De introductie van semantische samenvattingen in natuurlijke taal als intermediaire representatie voor verificatie, in tegenstelling tot eerdere werken die zich richten op het genereren van formele specificaties voor externe symbolische checkers.
• Gestaffelde Analysepijplijn: Een decompositie van redeneren over geheugenveiligheid in herbruikbare samenvattingen (allocatie, deallocatie, initialisatie en verplichtingen aan de kant van de caller) die in volgende fasen teruggevoerd worden naar de LLM.
• Empirische Evaluatie: Een vergelijkende studie van compositional redeneren versus een niet-compositional baseline voor het prompten van het hele programma, uitgevoerd op SV-COMP 2026-benchmarks.

Resultaten
De auteurs hebben NLForge geëvalueerd op een subset van de geheugenveiligheidsbenchmarks van SV-COMP 2026 met vier LLM-ruggengraten (Claude Sonnet-4.6, GPT-5.4, Gemini-3.1-flash-lite en Qwen3.5-27B-UD-Q4) en deze vergeleken met traditionele verifiers (CPAchecker, Symbiotic, Ultimate Automizer).

• RQ1 (LLMs als Verifiers): LLM-gebaseerde analyse toont een hoge recall en dekking, waarbij de meeste true positives worden geïdentificeerd (bijvoorbeeld behaalde Sonnet-4.6 een recall van 99,8% op valid-memsafety). Ze produceren echter aanzienlijk meer false positives dan traditionele tools en kunnen nog niet als standalone, sound verifiers fungeren. Traditionele tools geven vaak "Onbekend" (UNK) terug voor moeilijke gevallen om false positives te vermijden, terwijl LLMs definitieve antwoorden geven met hogere foutpercentages.
• RQ2 (Compositional Verificatie): De compositional aanpak presteert aanzienlijk beter dan de niet-compositional baseline, met name op complexe benchmarks voor real-world controleflow en datastructuren.
  • Compositional runs verhoogden het aantal True Positives van 3.390 naar 3.476 en verlaagden het aantal False Negatives van 301 naar 216 over alle modellen heen.
  • De verbetering was het meest uitgesproken voor kleinere modellen (bijvoorbeeld zag Qwen3.5-27B-Q4 het aantal False Negatives dalen van 218 naar 97) en op benchmarks die sterk interproceduraal redeneren vereisen.
  • De winsten waren minder consistent op synthetische, gelokaliseerde Juliet-tests, waar niet-compositional modellen lokale patronen direct konden benutten.

Betekenis en Claims
Het artikel pleit voor een verschuiving in hoe LLMs worden ingezet bij verificatie: van het behandelen van ze uitsluitend als generators van formele artefacten voor externe engines, naar het gebruik van ze als redeneeragenten over gestructureerde, herbruikbare samenvattingen in natuurlijke taal.

• Praktijktoepasbaarheid: Natuurlijke taal dient als een praktische intermediaire specificatielaag die compositional verificatie mogelijk maakt, met name voor taken waarbij prompten voor het hele programma de redeneerbudget of het contextvenster van het model overschrijdt.
• Beperkingen: De auteurs erkennen dat de informaliteit van natuurlijke taal leidt tot kalibratieproblemen (hogere false positives) en dat de aanpak gevoelig is voor de kwaliteit van gegenereerde samenvattingen; fouten in samenvattingen kunnen zich voortplanten en versterken.
• Toekomstperspectief: Het werk suggereert dat LLMs, hoewel ze nog geen vervanging zijn voor sound formele verificatie, een veelbelovende richting bieden voor schaalbare, bug-vindende verificatie. Toekomstig werk moet zich richten op het verbeteren van kalibratie, het combineren van samenvattingen met symbolische checks, en het robuuster hanteren van complexe functies zoals indirecte aanroepen en heap-invarianten.

De studie concludeert dat de vraag niet zozeer is of LLMs geheugenveiligheid kunnen verifiëren, maar onder welke representaties en decomposities ze betrouwbaarder worden, met de nadruk dat natuurlijke taal de kloof effectief kan overbruggen tussen de modulaire structuur van programma's en de redeneercapaciteiten van LLMs.