Technische Zusammenfassung: Agentische Interpretation für LLM-basierte Programmanalyse

1. Problemstellung

Large Language Models (LLMs) bieten einzigartige Fähigkeiten für die Programmanalyse, indem sie auf Informationen jenseits des Quellcodes zugreifen, wie Dokumentation, Sicherheitswarnungen, metadaten spezifischer Versionen und informelle API-Verträge. Die Abhängigkeit von LLMs für eine „One-Shot"-Analyse des gesamten Programms ist jedoch aus drei Hauptgründen inhärent brüchig:

1. Kontextsensitivität: Empirische Studien zeigen, dass die Modellleistung mit zunehmender Kontextlänge und Aufgabenkomplexität nachlässt und die Ergebnisse stark von der Reihenfolge der Informationen im Prompt abhängen. Kritische Beweise (z. B. eine spezifische Sicherheitswarnung) können zwar bereitgestellt, aber nicht zuverlässig genutzt werden.
2. Fehlender persistenter Zustand: Monolithische LLM-Antworten verfügen über keinen persistenten Zustand, um zu verfolgen, welche spezifischen Behauptungen unterstützt, widerlegt oder offen gelassen wurden. Dies erschwert den Umgang mit sich selbst widersprechenden Schlussfolgerungen oder Schlussfolgerungen, die ihre eigenen Ergebnisse nicht stützen.
3. Fehlen einer Abhängigkeitsstruktur: Eine Single-Shot-Antwort bietet keinen Mechanismus für Feedback. Wenn spätere Erkenntnisse zeigen, dass eine frühere Frage falsch eingegrenzt war oder dass eine vorgelagerte Komponente unter einer anderen Hypothese erneut untersucht werden muss, kann eine unstrukturierte Antwort diese iterative Verfeinerung nicht unterstützen.

Folglich besteht ein Bedarf an einem Rahmenwerk, das die Lücke zwischen ad-hoc LLM-Prompts und vollständig spezifizierter statischer Analyse überbrückt, speziell für beweisdurchdringende Programmanalysen, bei denen die relevanten Fakten nicht vollständig im Quellcode oder in formalen Spezifikationen enthalten sind.

2. Methodik: Agentische Interpretation

Die Arbeit schlägt Agentische Interpretation vor, ein Rahmenwerk, das die Disziplin der gitterbasierten statischen Analyse auf LLM-gesteuertes Schlussfolgern anwendet. Die Methodik zerlegt übergeordnete Analyseziele in lokalisierte Behauptungen, die an Programmpunkte und Komponentengrenzen gebunden sind, und verwaltet deren Entwicklung durch ein Gitter endlicher Höhe und einen Worklist-Algorithmus.

2.1 Kernkomponenten

• Bewertungsgraph ($G^*$): Eine Erweiterung eines aus dem Programm abgeleiteten Graphen ($G_{prog}$), der Folgendes umfasst:
  • Hilfsknoten: Knoten, die interkomponentale Interaktionen oder Ziele darstellen, die nicht einem einzelnen Programmpunkt entsprechen.
  • Kontextkanten: Vorwärtsgerichtete Kanten, die sicherstellen, dass bei der Bewertung einer Behauptung am Knoten $n$ der aktuelle Bewertungsstatus und die Beweise aus den Vorgängerknoten empfangen werden.
  • Feedback-Kanten: Rückwärtsgerichtete Kanten, die eine Neubewertung vorgelagerter Knoten auslösen, wenn sich eine nachgelagerte Bewertung ändert (z. B. löst eine widerlegte Kompositionsbehauptung eine gezielte Suche in einer undurchsichtigen Komponente aus).
• Bewertungsbereich (Gitter): Ein Join-Halb-Gitter endlicher Höhe ($A$), das den evidentiellen Status einer Behauptung zusammenfasst.
  • Die Arbeit illustriert dies mit dem AGraded-Gitter: $\{ \perp, w, s \} \times \{ \perp, w, s \}$, wobei die erste Koordinate stützende Beweise und die zweite widerlegende Beweise darstellt. Die Werte reichen von fehlend ($\perp$) über schwach ($w$) bis stark ($s$).
  • Das Gitter ist ein epistemischer Bereich über Beweiszustände, kein abstrakter Bereich über konkrete Programmzustände. Es erfasst, ob eine Behauptung unterstützt oder widerlegt wurde, und die Stärke dieser Beweise.
• Worklist-Harness: Eine Kontrollschleife, die den Analysezustand verwaltet.
  • Kontextualisierung: Für einen Knoten $n$ konstruiert die Harness einen Prompt-Kontext ($\Gamma_n$) unter Verwendung von Quellcode, dem übergeordneten Ziel und den aktuellen Bewertungen der Vorgängerknoten.
  • Knotentransformatoren: Der LLM-Agent führt zwei Operationen durch:
    1. Bewertung: Bewertet bestehende Behauptungen im Kontext und gibt eine aktualisierte Bewertung sowie Beweisaufzeichnungen zurück.
    2. Generierung: Schlägt neue, relevante Behauptungen basierend auf dem Kontext vor.
  • Propagation: Wenn die Join-Operation der neuen Bewertung mit der alten Bewertung zu einer strikten Erhöhung der Gitterordnung führt, werden die erweiterten Nachfolger des Knotens zur Neubewertung in die Warteschlange aufgenommen.

2.2 Der Analyseprozess

Der Prozess wird anhand einer Sicherheitsprüfung eines Programms mit undurchsichtigen Drittanbieter-Komponenten (ein JSON-Parser und ein Signaturverifizierer) veranschaulicht.

1. Initialisierung: Die Worklist wird mit allen Programm- und Hilfsknoten gesät.
2. Iterative Verfeinerung:
   • Phase I: Initiale unabhängige Bewertung der Komponenten (z. B. Überprüfung der Dokumentation für Parser und Verifizierer).
   • Phase II: Zusammensetzung von Beweisen. Das Rahmenwerk bewertet interkomponentale Behauptungen (z. B. „Stellen die Komponenten gemeinsam Sicherheit sicher?"). Wenn eine Kompositionsbehauptung schwach widerlegt wird, lösen Feedback-Kanten eine erneute Untersuchung vorgelagerter Komponenten aus.
   • Phase III: Feedback-gesteuerte Verfeinerung. Der Kontext aus der widerlegten Komposition (z. B. „der Prozessor führt keine Validierung durch") leitet den LLM an, eine gezielte Suche nach spezifischen Schwachstellen (z. B. Prototype Pollution) durchzuführen, anstatt eine breite Überprüfung.
   • Phase IV: Stabilisierung. Die verstärkten Beweise aus vorgelagerten Bereichen propagieren vorwärts und führen zu einer starken Widerlegung des globalen Ziels. Die Worklist leert sich, wenn keine weiteren strikten Erhöhungen der Bewertung auftreten.

3. Hauptbeiträge

Die Arbeit leistet drei primäre Beiträge:

1. Rahmenwerk-Vorschlag: Sie führt Agentische Interpretation als strukturierten Ansatz für beweisdurchdringende Programmanalysen ein und identifiziert ein geeignetes Problemgebiet, in dem LLMs notwendig, aber direktes Prompting unzureichend sind.
2. Formales Modell: Sie formalisiert das Kernmodell und definiert den Bewertungsgraphen, den Bewertungsbereich, Knotentransformatoren und den Worklist-Algorithmus.
3. Charakterisierung des Designraums: Sie erkundet den Designraum, einschließlich:
   • Bewertungsgitter: Diskussion von Kompromissen zwischen groben Gittern (z. B. Vorhandensein/Abwesenheit) und fein granulierten Gittern (z. B. Stärke, Vertrauensbasis). Sie führt AStratified ein, einen Bereich, der die Beweiskraft und die Vertrauensbasis (z. B. „nur Modell" vs. „geprüft") separat verfolgt.
   • Behauptungsmanagement: Behandlung der Kanonisierung, Granularität und Reichweite von Behauptungen.
   • Abfragedesign: Unterscheidung zwischen Bewertungsabfragen (Unterstützung/Widerlegung) und generativen Abfragen (Vorschlag neuer Behauptungen).
   • Terminierung: Beweis, dass der Algorithmus für Gitter endlicher Höhe mit begrenzter Behauptungsgenerierung terminiert, selbst bei nicht-deterministischen LLM-Antworten, sofern Aktualisierungen monoton sind (via Join).

4. Ergebnisse und Einschränkungen

• Ergebnisse: Die Arbeit liefert ein durchgerechnetes Beispiel (eine Sicherheitsprüfung eines Handlers mit undurchsichtigen Komponenten), das zeigt, wie das Rahmenwerk ein Ziel zerlegt, Feedback-Schleifen zur Verfeinerung der Suche nutzt und sich auf eine endgültige Bewertung stabilisiert. Es wird gezeigt, wie das Rahmenwerk erkennen kann, dass ein globales Sicherheitsziel verletzt wird, indem schwache Beweise aus mehreren Quellen zu einer starken Widerlegung kombiniert werden.
• Einschränkungen:
  • Die Arbeit beschreibt laufende Arbeiten. Sie enthält keine praktische Implementierung oder experimentelle Auswertung.
  • Das Rahmenwerk garantiert Terminierung und Beschränktheit, garantiert jedoch keine Korrektheit im traditionellen Sinne (d. h., es beweist nicht, dass die Schlussfolgerungen des LLM korrekt sind). Es macht die evidentielle Rolle des LLM explizit und überprüfbar.
  • Das Rahmenwerk kann einen Agenten, der Beweise konsistent falsch einschätzt, nicht korrigieren; es macht solche Fehler lediglich sichtbar.
  • Der Terminierungsbeweis beruht auf der Annahme, dass Behauptungen niemals widerrufen werden und Bewertungen nur via Join erhöht werden. Mechanismen für die Überarbeitung von Überzeugungen (Absenkung von Bewertungen) werden als zukünftige Arbeit diskutiert, die eine begrenzte Ersetzung oder epochale Neuberechnung erfordert.

5. Bedeutung

Die Bedeutung dieser Arbeit liegt in ihrem Versuch, strukturelle Disziplin in die LLM-basierte Schlussfolgerung bei der Programmanalyse zu bringen. Durch die Abkehr vom „Generate-and-Check"-Paradigma (das einen formalen Verifizierer für die Ausgabe des LLM erfordert) und dem „Heuristisches Orakel"-Paradigma (bei dem der LLM die Korrektheit nicht beeinflussen kann), zielt die Agentische Interpretation auf einen Mittelweg ab.

Sie ist bedeutsam für beweisdurchdringende Analysen, bei denen:

• Die relevanten Fakten nicht formalisierbar sind (z. B. informelle API-Verträge, Sicherheitswarnungen).
• Ein vollständiger Verifizierer nicht existiert.
• Die Analyse Informationen aus diversen, nicht-code-basierten Quellen synthetisieren muss.

Das Rahmenwerk verwandelt den LLM von einem Black-Box-Generator in eine begrenzte, überprüfbare Komponente eines größeren Analysesystems. Es stellt sicher, dass die Analyse auf kontrollierte und prinzipielle Weise fortschreitet und ermöglicht die Trennung von Belangen: Der LLM liefert Beweise, und die gitterbasierte Harness stellt sicher, dass die Analyse begrenzt und nachvollziehbar ist. Dieser Ansatz zielt darauf ab, zukünftige Diskussionen über die Entwicklung formal fundierter Techniken für Agentensysteme in der Programmanalyse zu inspirieren.