Natural Language based Specification and Verification

Technische Zusammenfassung: Natursprachbasierte Spezifikation und Verifikation (NLForge)

Problemstellung
Verletzungen der Speichersicherheit in C- und C++-Programmen – wie ungültige Dereferenzierungen, Use-After-Free und Zugriffe außerhalb der Grenzen – bleiben eine Hauptquelle für Software-Schwachstellen. Diese Fehler resultieren häufig aus komplexen interprozeduralen Interaktionen, die Allokation, Deallokation, Initialisierung und Aliasierung umfassen, welche traditionelle statische Analysewerkzeuge in großem Maßstab nur schwer verifizieren können. Während Large Language Models (LLMs) starke Fähigkeiten beim Identifizieren von Fehlern gezeigt haben, stehen sie vor erheblichen Herausforderungen, die Einführung neuer Schwachstellen durch formale Verifikation zu verhindern. Bestehende Verifikationspipelines erfordern typischerweise Spezifikationen in starren formalen Sprachen (z. B. Schleifeninvarianten, Vor-/Nachbedingungen), was zu einer hohen Annotationslast führt. Frühere Versuche, LLMs zur Synthese dieser formalen Spezifikationen einzusetzen, haben nur begrenzten Erfolg gezeigt. Darüber hinaus deuten aktuelle Benchmarks darauf hin, dass die Leistung von LLMs beim Übergang von der Verifikation einzelner Funktionen zur kompositionellen, mehrfunktionalen Reasoning drastisch einbricht, was hauptsächlich auf Einschränkungen des Kontextfensters und die Schwierigkeit zurückzuführen ist, eine globale semantische Konsistenz aufrechtzuerhalten.

Methodik: NLForge
Die Autoren schlagen NLForge vor, ein kompositionelles Verifikationsframework, das LLMs nutzt, um natursprachliche Spezifikationen zu generieren und darauf zu reasoning, anstatt starrer formaler Artefakte. Das System arbeitet auf einer bottom-up-Analyse des Aufrufgraphen des Programms, beginnend bei den Callee-Funktionen.

1. Pipeline-Architektur:

   • Vorverarbeitung: Das System extrahiert Funktionsdefinitionen, Signaturen und Aufrufstellen aus C/C++-Code, um einen Aufrufgraphen zu konstruieren. Unauflösbare Aufrufe werden über externe Stubs behandelt.
   • Bottom-Up-Analyse: Das Framework führt eine Sequenz von Analyse-Passes über den Aufrufgraphen in topologischer Reihenfolge durch (Verarbeitung von Callee-Funktionen vor den Callern).
   • Natursprachliche Zusammenfassungen: Anstatt formale Logik zu generieren, erstellt das LLM strukturierte natursprachliche Zusammenfassungen (kodiert als typisiertes JSON mit natursprachlichen Beschreibungen) für spezifische Eigenschaften:
     • Allokation/Freigabe/Initialisierung: Zusammenfassung der Erzeugung von Heap-Objekten, Effekte der Freigabe und Initialisierung von Ausgabeparametern.
     • Speichersicherheitsverträge: Ableitung von Vorbedingungen (z. B. nicht-null, nicht-freigegeben, Puffergröße) und Nachbedingungen.
     • Leck- und Ganzzahl-Zusammenfassungen: Verfolgung offener Verpflichtungen und Risiken von Integer-Überläufen.
   • Kompositionelle Prüfung: Im abschließenden Verifikationsschritt analysiert das LLM eine Funktion unter Verwendung ihrer eigenen abgeleiteten Vorbedingungen und der natursprachlichen Zusammenfassungen ihrer Callee-Funktionen. Das Modell fungiert als Reasoning-Agent, der einen latenten Ausführungszustand aufrechterhält und Sicherheitsanforderungen gegen Callee-Verträge prüft, ohne die vollständige Implementierung der Callee-Funktion einzubetten.

2. Designbegründung:
   Dieser Ansatz wird durch die Beobachtung motiviert, dass LLMs, die auf Code und Dokumentation trainiert wurden, natursprachliche Zusammenfassungen konsistenter generieren, interpretieren und verfeinern können als starre formale Notationen. Dieses Design zielt darauf ab, das Verifikationsproblem in wiederverwendbare semantische Zusammenfassungen zu zerlegen, sodass das Modell eine Funktion unter explizit stated Annahmen über ihre Callee-Funktionen reasoning kann, anstatt den rohen Quellcode für jeden Caller erneut zu analysieren.

Hauptbeiträge

• Kompositionelles Framework: Ein bottom-up interprozedurales Verifikationsframework für C/C++, das LLMs zur Inferenz und Verifikation von Speichersicherheitseigenschaften nutzt.
• Natursprachliche Intermediärdarstellung: Die Einführung natursprachlicher semantischer Zusammenfassungen als Intermediärdarstellung für die Verifikation, im Gegensatz zu früheren Arbeiten, die sich auf die Generierung formaler Spezifikationen für externe symbolische Prüfer konzentrieren.
• Stufenweise Analyse-Pipeline: Eine Zerlegung des Speichersicherheits-Reasonings in wiederverwendbare Zusammenfassungen (Allokation, Deallokation, Initialisierung und Caller-seitige Verpflichtungen), die in nachfolgenden Stufen wieder an das LLM zurückgespeist werden.
• Empirische Evaluation: Eine vergleichende Studie über kompositionelles Reasoning versus eine nicht-kompositionelle Whole-Program-Prompting-Baseline auf SV-COMP 2026-Benchmarks.

Ergebnisse
Die Autoren evaluierten NLForge auf einer Teilmenge der SV-COMP 2026-Speichersicherheits-Benchmarks unter Verwendung von vier LLM-Backbones (Claude Sonnet-4.6, GPT-5.4, Gemini-3.1-flash-lite und Qwen3.5-27B-UD-Q4) und verglichen diese mit traditionellen Verifikatoren (CPAchecker, Symbiotic, Ultimate Automizer).

• RQ1 (LLMs als Verifikatoren): Die LLM-basierte Analyse zeigt eine hohe Recall-Rate und Abdeckung und identifiziert die meisten True Positives (z. B. erreichte Sonnet-4.6 einen Recall von 99,8 % bei valid-memsafety). Allerdings produzieren sie signifikant mehr False Positives als traditionelle Werkzeuge und können noch nicht als eigenständige, sounde Verifikatoren dienen. Traditionelle Werkzeuge geben für schwierige Fälle oft „Unknown" (UNK) zurück, um False Positives zu vermeiden, während LLMs definitive Antworten mit höheren Fehlerraten liefern.
• RQ2 (Kompositionelle Verifikation): Der kompositionelle Ansatz übertrifft die nicht-kompositionelle Baseline signifikant, insbesondere bei komplexen Benchmarks für reale Kontrollfluss- und Datenstruktur-Anforderungen.
  • Kompositionelle Runs erhöhten die True Positives von 3.390 auf 3.476 und reduzierten die False Negatives von 301 auf 216 über alle Modelle hinweg.
  • Die Verbesserung war bei kleineren Modellen am ausgeprägtesten (z. B. sanken bei Qwen3.5-27B-Q4 die False Negatives von 218 auf 97) und bei Benchmarks, die starkes interprozedurales Reasoning erfordern.
  • Die Gewinne waren bei synthetischen, lokalisierten Juliet-Tests weniger konsistent, wo nicht-kompositionelle Modelle lokale Muster direkt ausnutzen konnten.

Bedeutung und Behauptungen
Die Arbeit plädiert für einen Wandel in der Nutzung von LLMs in der Verifikation: weg davon, sie ausschließlich als Generatoren formaler Artefakte für externe Engines zu behandeln, hin zu ihrer Nutzung als Reasoning-Agenten über strukturierte, wiederverwendbare natursprachliche Zusammenfassungen.

• Praktikabilität: Natursprache dient als praktische Intermediärspezifikationsschicht, die kompositionelle Verifikation ermöglicht, insbesondere für Aufgaben, bei denen Whole-Program-Prompting das Reasoning-Budget oder das Kontextfenster des Modells übersteigt.
• Einschränkungen: Die Autoren räumen ein, dass die Informalität der Natursprache zu Kalibrierungsproblemen (höhere False Positives) führt und dass der Ansatz empfindlich gegenüber der Qualität der generierten Zusammenfassungen ist; Fehler in Zusammenfassungen können sich fortpflanzen und verstärken.
• Ausblick: Die Arbeit legt nahe, dass LLMs zwar noch keinen Ersatz für sounde formale Verifikation darstellen, aber eine vielversprechende Richtung für skalierbare, fehlersuchende Verifikation bieten. Zukünftige Arbeiten sollten sich auf die Verbesserung der Kalibrierung, die Kombination von Zusammenfassungen mit symbolischen Prüfungen und die robustere Handhabung komplexer Merkmale wie indirekte Aufrufe und Heap-Invarianten konzentrieren.

Die Studie kommt zu dem Schluss, dass die Frage nicht nur ob LLMs Speichersicherheit verifizieren können, sondern unter welchen Repräsentationen und Zerlegungen sie zuverlässiger werden, ist. Dies unterstreicht, dass Natursprache die Lücke zwischen modularer Programmstruktur und LLM-Reasoning-Fähigkeiten effektiv überbrücken kann.