💻 computer science

Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

Die Arbeit stellt Gordian vor, ein hybrides Framework für die symbolische Ausführung, das LLMs gezielt einsetzt, um durch Generierung von Ghost-Code solver-feindliche Codefragmente zu entschärfen und dabei die Präzision von SMT-Lösern zu erhalten, was in Tests zu einer signifikant höheren Abdeckung und einer drastischen Reduktion des LLM-Token-Verbrauchs führt.

Ursprüngliche Autoren: Dimitrios Stamatios Bouras, Sergey Mechtaev

Veröffentlicht 2026-03-23

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Dimitrios Stamatios Bouras, Sergey Mechtaev

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stell dir vor, du bist ein Detektiv, der versuchen soll, ein riesiges, komplexes Schloss zu knacken. Das Schloss ist ein Computerprogramm, und dein Ziel ist es, herauszufinden, wie man es so bedient, dass es eine versteckte „Falle" (einen Fehler oder eine spezielle Funktion) auslöst.

In der Welt der Software-Sicherheit gibt es einen sehr klugen, aber manchmal überforderten Assistenten namens Symbolische Ausführung. Dieser Assistent probiert nicht einfach zufällig Tasten, sondern denkt logisch: „Wenn ich hier eine 5 eingebe, passiert X; wenn ich eine 10 eingebe, passiert Y." Er versucht, den gesamten Weg durch das Programm im Kopf zu simulieren.

Das Problem:
Manchmal stößt dieser Assistent auf „Logik-Bomben". Das sind Teile des Programms, die so kompliziert sind (z. B. mit schwerer Mathematik, trigonometrischen Funktionen oder riesigen, verwobenen Datenstrukturen), dass der Assistent einfach nicht weiterkommt. Er steht vor einer verschlossenen Tür und weiß nicht, welchen Schlüssel er braucht, weil die Berechnungen zu schwer für ihn sind.

Frühere Versuche, dieses Problem zu lösen, haben einen riesigen, sehr kreativen KI-Chatbot (einen „Large Language Model" oder LLM) als neuen Detektiv eingesetzt, der den alten Assistenten komplett ersetzt hat. Aber dieser neue Detektiv ist zwar kreativ, aber vergesslich. Er kann nicht gut über den gesamten Weg nachdenken. Wenn das Schloss 100 Schritte entfernt ist und jeder Schritt eine Bedingung hat, vergisst der KI-Detektiv oft, was am Anfang passiert ist, und scheitert.

Die Lösung: Gordian
Die Autoren dieses Papers haben eine brillante Idee namens Gordian entwickelt. Sie sagen: „Warum müssen wir uns entscheiden? Wir brauchen beide!"

Stell dir vor, der alte Assistent (der SMT-Solver) ist ein Präzisions-Ingenieur. Er ist extrem genau, aber bei komplizierten mathematischen Rätseln blockiert er. Der KI-Chatbot ist ein kreativer Architekt, der gut darin ist, neue Ideen zu entwickeln, aber schlecht darin, die Details über lange Distanzen zu behalten.

Gordian ist wie ein Bauleiter, der beide zusammenbringt. Anstatt den Ingenieur durch den Architekten zu ersetzen, nutzt Gordian den Architekten nur dann, wenn der Ingenieur vor einer unüberwindbaren Mauer steht.

Wie funktioniert das? Mit „Geister-Code" (Ghost Code)

Der Bauleiter (Gordian) lässt den Architekten (die KI) nicht das ganze Schloss bauen, sondern nur kleine, hilfreiche Werkzeuge, die er dem Ingenieur gibt. Diese Werkzeuge nennt man „Geister-Code". Sie sind unsichtbar für das eigentliche Programm, helfen aber dem Ingenieur beim Denken.

Es gibt drei Arten von Werkzeugen, die der Architekt baut:

Der Rückwärts-Denker (Inversion):
- Das Problem: Der Ingenieur steht vor einer Formel wie Ergebnis = sin(x) * cos(x). Er weiß das Ergebnis, aber er weiß nicht, welches x dazu führt. Das ist wie zu versuchen, einen Kuchen zu backen, indem man nur den fertigen Kuchen betrachtet und versucht, die Zutaten zu erraten.
- Die Lösung: Der Architekt baut einen kleinen „Rückwärts-Rechner". Er sagt dem Ingenieur: „Wenn du das Ergebnis hast, hier ist eine Anleitung, wie du schrittweise zurückrechnest, um das x zu finden." Der Ingenieur kann dann seinen Weg zurückverfolgen und die richtige Tür finden.
Der vereinfachte Ersatz (Surrogate Models):
- Das Problem: Manchmal ist ein Teil des Programms so komplex (z. B. eine geheime Verschlüsselung), dass der Ingenieur sie gar nicht verstehen kann.
- Die Lösung: Der Architekt baut einen „Stellvertreter". Er sagt: „Vergiss die komplizierte Verschlüsselung. Stell dir stattdessen vor, dieser Teil ist nur eine einfache Addition. Das Verhalten ist fast das Gleiche, aber für deinen Verstand viel einfacher zu berechnen." Der Ingenieur kann weiterarbeiten, ohne sich im Dschungel zu verirren.
Der Kartenzeichner für den Wald (Semantic Heap Partitioning):
- Das Problem: In Programmen mit vielen Zeigern (Datenstrukturen) gibt es unendlich viele Möglichkeiten, wie die Daten im Speicher angeordnet sein könnten. Der Ingenieur versucht, jeden einzelnen Pfad durch diesen Wald zu gehen, und wird wahnsinnig (Path Explosion).
- Die Lösung: Der Architekt sagt: „Wir müssen nicht jeden einzelnen Baum im Wald untersuchen. Wir wissen, dass es nur drei wichtige Arten von Wegen gibt: einen geraden Weg, einen Ring und einen Sackgassen-Weg." Er zeichnet dem Ingenieur nur diese drei Karten. Der Ingenieur muss nur noch diese drei Pfade prüfen, anstatt den ganzen Wald zu durchsuchen.

Das Ergebnis
Am Ende prüft der Bauleiter (Gordian), ob die Lösungen des Architekten wirklich funktionieren, indem er sie im echten Programm testet. So wird sichergestellt, dass die KI keine Halluzinationen (falsche Ideen) liefert.

Warum ist das so toll?

Effizienz: Der alte Assistent (Ingenieur) macht den schweren, logischen Teil. Die KI (Architekt) hilft nur bei den Stellen, wo es klemmt.
Kosten: Da die KI nur selten angerufen wird, spart man enorm viel Rechenzeit und Geld (Token-Kosten).
Erfolg: In Tests hat Gordian deutlich mehr „Fehler" und „Fallen" gefunden als alle anderen Methoden, sowohl als der reine Ingenieur als auch als der reine KI-Detektiv.

Zusammenfassung in einem Satz:
Gordian ist wie ein Team aus einem strengen Mathematiker und einem kreativen Künstler, bei dem der Künstler nur dann eingreift, wenn der Mathematiker vor einem ungelösten Rätsel steht, um ihm eine kleine Hilfe zu geben, damit sie gemeinsam das ganze Schloss knacken können.

Titel:

Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code
(Entschärfung von Logikbomben in der symbolischen Ausführung durch von LLMs generierten Ghost-Code)

1. Problemstellung

Die symbolische Ausführung (Symbolic Execution) ist eine leistungsstarke Technik zur Programmanalyse, die jedoch an fundamentalen Grenzen stößt:

Solver-feindlicher Code: Komplexe numerische Berechnungen (z. B. nichtlineare Arithmetik, trigonometrische Funktionen) oder unentscheidbare Theorien führen zu SMT-Constraints, die von Solvern (wie Z3 oder STP) nicht oder nur extrem langsam gelöst werden können.
Heap-Konfigurations-Explosion: Bei Programmen mit dynamischen Datenstrukturen (z. B. verknüpfte Listen, Bäume) führt die Vielzahl möglicher Aliasing-Beziehungen und Heap-Formen zu einer exponentiellen Pfadexplosion.
Grenzen reiner LLM-Ansätze: Neuere Ansätze, die Large Language Models (LLMs) nutzen, um SMT-Solver komplett zu ersetzen (z. B. ConcoLLMic), scheitern oft an realen Codebasen. LLMs haben Schwierigkeiten, globale Konsistenz über viele interagierende Funktionen hinweg zu gewährleisten und lange Abhängigkeitsketten korrekt zu modellieren.

Das Ziel ist es, die Präzision und globale reasoning-Fähigkeit von SMT-Solvern mit der Domänenkenntnis und Generierungsfähigkeit von LLMs zu kombinieren, ohne die Zuverlässigkeit der symbolischen Ausführung zu opfern.

2. Methodik: Gordian

Das Paper stellt Gordian vor, ein hybrides Framework, das SMT-basierte symbolische Ausführung (implementiert auf Basis von KLEE) mit LLMs integriert. Der Kernansatz besteht darin, LLMs nicht als Ersatz für Solver zu verwenden, sondern selektiv zur Generierung von Ghost-Code (Hilfscode, der die Semantik des Programms nicht verändert, aber die Analyse erleichtert).

Gordian identifiziert schwierige Code-Fragmente und generiert drei Arten von Ghost-Code, je nach Kontext:

A. Inversion schwieriger Fragmente (Fragment Inversion)

Ziel: Überwindung von Solver-feindlichen Operationen (z. B. sin(x), cos(x)).
Mechanismus: Ein LLM wird aufgefordert, eine inverse Funktion $f^{-1}$ zu generieren, die aus den Zielwerten (Suffix-Constraints) die Eingabewerte (Prefix-Constraints) rekonstruiert.
Bidirektionale Constraint-Propagation:
1. Der Solver löst die Constraints nach dem schwierigen Fragment (Suffix), um Kandidatenwerte für die Ausgabe zu erhalten.
2. Die generierte inverse Funktion führt diese Werte konkret zurück, um einen Eingabewert zu schätzen.
3. Ein Optimierungs-Solver findet den Eingabewert, der die Vorwärts-Constraints (Prefix) erfüllt und dem inversen Ergebnis am nächsten kommt.
4. Dies ermöglicht es, Pfade zu durchlaufen, die für den Solver allein unzugänglich wären.

B. Surrogat-Modelle (Surrogate Models)

Ziel: Ersetzung von komplexen, solver-unfreundlichen Code-Fragmenten durch vereinfachte, solver-freundliche Äquivalente.
Mechanismus: Das LLM generiert einen „Surrogate"-Code, der das relevante Verhalten (z. B. Verzweigungen, Ausgaben) beibehält, aber in eine für den SMT-Solver leicht lösbare Theorie (z. B. lineare Arithmetik statt Bitvektoren oder Floating-Point) übersetzt.
Validierung: Da dies eine Approximation ist, werden alle generierten Testeingaben am Ende am Originalprogramm validiert, um die Korrektheit (Soundness) zu gewährleisten.

C. Semantische Partitionierung des Heaps (Semantic Heap Partitioning)

Ziel: Bekämpfung der Pfadexplosion bei dynamischen Datenstrukturen.
Mechanismus: Das LLM analysiert den Kontext und generiert Ghost-Code, der den Heap auf eine kleine Menge semantisch bedeutender Topologien (z. B. „Ring", „gebrochene Kette", „korrekte Liste") einschränkt.
Vorteil: Statt alle möglichen Heap-Konfigurationen symbolisch zu explorieren, wird der Heap durch einen symbolischen Selektor in repräsentative, strukturell sinnvolle Formen unterteilt. Dies reduziert den Suchraum drastisch, während die Dateninhalte (Values) weiterhin symbolisch bleiben.

3. Schlüsselbeiträge

Hybrider Ansatz: Eine neue Architektur, die LLMs gezielt zur Generierung von Solver-Hilfen (Ghost-Code) nutzt, anstatt den Solver zu ersetzen. Dies bewahrt die globale Konsistenz und Präzision.
Drei Ghost-Code-Varianten: Entwicklung und Integration von Inversions-Algorithmen, Surrogat-Modellen und semantischen Heap-Partitionen, jeweils mit spezifischen Prompt-Templates und Integrationsalgorithmen.
Soundness durch Validierung: Der Ansatz garantiert, dass keine falschen Ergebnisse durch Halluzinationen des LLM entstehen, da alle Ergebnisse am Originalprogramm validiert werden.
Umfassende Evaluation: Evaluation auf synthetischen Benchmarks (LogicBombs), einer realen mathematischen Bibliothek (FDLibM) und strukturierten Eingabe-Programmen (libexpat, jq, bc).

4. Ergebnisse

Die Evaluation zeigt signifikante Verbesserungen gegenüber traditionellen symbolischen Ausführungswerkzeugen (KLEE mit STP/Z3) und rein LLM-basierten Ansätzen (ConcoLLMic, Cottontail):

Abdeckung (Coverage):
- LogicBombs: Gordian steigerte die Abdeckung um 52–84 % gegenüber traditionellen Methoden und um 86–419 % gegenüber LLM-basierten Techniken. Es löste bis zu 94,3 % der Logikbomben.
- FDLibM (Mathematik-Bibliothek): Im Vergleich zu ConcoLLMic eine Verbesserung von durchschnittlich 183,5 %. Gordian erreichte eine durchschnittliche Abdeckung von ~91 %, während KLEE bei ~63 % und ConcoLLMic bei ~37 % lag.
- Strukturierte Eingaben: Auf Programmen wie jq und bc erreichte Gordian bis zu 108 % mehr Abdeckung als KLEE und deckte 9,7-mal mehr Zeilen ab als ConcoLLMic.
Effizienz (Token-Kosten):
- Gordian ist extrem token-effizient, da das LLM nur für die Generierung des Ghost-Code und nicht für die gesamte Pfadexploration aufgerufen wird.
- Reduktion des Token-Verbrauchs um 90–96 % im Vergleich zu ConcoLLMic und Cottontail.
Skalierbarkeit: Gordian skaliert effektiv auf reale, komplexe Codebasen, bei denen reine Solver-Ansätze scheitern und reine LLM-Ansätze zu teuer oder inkonsistent sind.

5. Bedeutung und Fazit

Das Paper demonstriert, dass die Kombination von symbolischer Ausführung und LLMs durch eine hybride, ghost-code-basierte Strategie den „Sweet Spot" für die Analyse komplexer Software findet.

Praktische Relevanz: Die Methode macht symbolische Ausführung für reale Anwendungen (Mathematik-Bibliotheken, Parser, strukturierte Eingaben) praktikabel, die bisher aufgrund von Solver-Schwächen oder Pfadexplosion unzugänglich waren.
Paradigmenwechsel: Statt LLMs als „Blackbox"-Solver zu verwenden, werden sie als intelligente Assistenten integriert, die spezifische, lokalisierte Probleme lösen, während der SMT-Solver die globale Konsistenz sicherstellt.
Zukunftsaussichten: Die Arbeit legt den Grundstein für weiterführende Integrationen, bei denen LLM-Modelle und Inversen direkt in den Symbolic-Execution-Engine integriert und zwischengespeichert werden könnten, um eine sich selbst verbessernde Analyseumgebung zu schaffen.

Zusammenfassend bietet Gordian einen robusten Weg, um die „Logikbomben" (Solver-Hindernisse) in der Softwareanalyse zu entschärfen, ohne die mathematische Präzision der symbolischen Ausführung aufzugeben.