NESA: Relational Neuro-Symbolic Static Program Analysis

1. Problemstellung

Die statische Programmanalyse ist ein wesentlicher Bestandteil der Softwareentwicklung für Optimierung, Fehlererkennung und Debugging. Trotz erheblicher Fortschritte in Präzision und Skalierbarkeit wird sie in der Praxis oft nicht genutzt. Das Papier identifiziert zwei Hauptbarrieren:

• Abhängigkeit von der Kompilierung: Herkömmliche Analysetools benötigen oft Intermediate Representations (IR), die nur nach einer erfolgreichen Kompilierung des Quellcodes verfügbar sind. Dies macht sie in Entwicklungsumgebungen unbrauchbar, wo Code oft unvollständig ist. Zudem erschweren Inkompatibilitäten zwischen Build-Systemen, Compilern und IR-Versionen die Integration.
• Mangelnde Anpassungsfähigkeit (Customization): Die Anpassung bestehender Tools an spezifische Entwickleranforderungen erfordert tiefes Wissen über Compiler-Infrastrukturen und IRs. Dies stellt eine hohe Einstiegshürde dar.

Große Sprachmodelle (LLMs) bieten zwar die Möglichkeit, Code semantisch zu verstehen und Analysen ohne Kompilierung durchzuführen, leiden jedoch unter dem Problem von Halluzinationen (falsche Aussagen), was zu unzuverlässigen Ergebnissen führt.

2. Methodik: NESA (Neuro-Symbolic Static Program Analysis)

NESA ist ein kompositioneller, neuro-symbolischer Ansatz, der die Stärken von LLMs mit deterministischen Parser-basierten Analysen kombiniert, um Halluzinationen zu minimieren und eine kompilierungsfreie, anpassbare Analyse zu ermöglichen.

Kernkonzepte:

• Analyse-Richtsprache (Analysis Policy Language):

  • Die Benutzer definieren die Analyse als eine Menge von Regeln in einer eingeschränkten Form von Datalog.
  • Diese Sprache erlaubt die Zerlegung komplexer Analyseprobleme in kleinere Teilprobleme.
  • Es werden zwei Arten von Relationen unterschieden:
    1. Symbolische Relationen: Erfassen syntaktische Eigenschaften (z. B. Variablenamen, Zeilennummern, Kontrollfluss), die deterministisch durch einen Parser (z. B. Tree-sitter) extrahiert werden können.
    2. Neuronale Relationen: Erfassen semantische Eigenschaften (z. B. Datenabhängigkeiten, Taint-Flows), die für LLMs definiert werden müssen.
  • Intensionale Relationen: Das gewünschte Endergebnis (z. B. ein Programm-Slice oder ein gefundener Bug), das aus den anderen Relationen abgeleitet wird.

• Neuronale Relationsspezifikationen:

  • Benutzer definieren semantische Eigenschaften durch natürliche Sprache und Few-Shot-Beispiele (Chain-of-Thought).
  • Dies ermöglicht eine deklarative Anpassung ohne Kenntnis von Compiler-Interna.

• Auswertungsverfahren (Evaluation Procedure):

  • NESA verwendet einen Worklist-Algorithmus, um die Datalog-Regeln bis zu einem Fixpunkt auszuwerten.
  • Lazy Prompting (Träges Prompting): Das Ausfüllen neuronaler Relationen durch LLMs wird verzögert, bis die zugehörigen symbolischen Relationen bereits gefüllt sind. Dies schränkt den Suchraum für das LLM ein (z. B. nur spezifische Ausdrücke betrachten statt des gesamten Programms), was Halluzinationen drastisch reduziert.
  • Incremental Prompting (Inkrementelles Prompting): Um Token-Kosten und Zeit zu sparen, werden nur neue Tupel generiert, die noch nicht in der Relation vorhanden sind. Redundante Anfragen werden vermieden.
  • Constraint Neural Constructors: Je nachdem, welche Terme (Variablen) bereits durch symbolische Relationen „gebunden" (bounded) sind, wählt NESA automatisch den am besten geeigneten Constructor (z. B. 2-arity statt 0-arity), um die Wahrscheinlichkeit von Halluzinationen zu minimieren.

3. Schlüsselbeiträge

1. Neuro-Symbolischer Rahmen: Ein neuer Ansatz, der LLMs für semantische Analyse und Parser für syntaktische Analyse kombiniert, um eine kompilierungsfreie und anpassbare statische Analyse zu ermöglichen.
2. Datalog-basierte Policy-Sprache: Eine Sprache, die es Benutzern erlaubt, komplexe Analysen durch Zerlegung in symbolische und neuronale Teilprobleme zu definieren.
3. Strategien zur Reduktion von Halluzinationen: Einführung von Lazy Prompting und Incremental Prompting sowie Constrained Neural Constructors, die die Genauigkeit von LLMs in der Programmieranalyse signifikant steigern.
4. Umfassende Evaluation: Demonstration der Überlegenheit gegenüber reinen LLM-Ansätzen und bestehenden State-of-the-Art-Tools in verschiedenen Szenarien.

4. Ergebnisse

Die Evaluation umfasste Programm-Slicing und die Erkennung von sechs verschiedenen Fehlertypen (APT, XSS, DBZ, NPD, RE, UOWH) sowie reale Anwendungen.

• Leistung (Präzision und Recall):

  • Programm-Slicing: NESA erreichte 91,50 % Präzision und 84,61 % Recall (F1-Score 0,88), was den State-of-the-Art-Slicer NS-Slicer (F1 0,82) und reine LLM-Ansätze deutlich übertrifft.
  • Bug-Erkennung (Juliet Test Suite): Hohe Präzision und Recall bei XSS (98,95 % / 94,00 %) und APT (94,74 % / 90,00 %). Auch bei schwierigeren Fällen wie DBZ (Divide-by-Zero) und NPD (Null Pointer) zeigte NESA robuste Ergebnisse, wo reine LLM-Ansätze oft versagten.
  • TaintBench (Reale Malware): Bei der Erkennung von Taint-Schwachstellen in Android-Malware erreichte NESA eine Präzision von 66,27 % und einen Recall von 78,57 % (F1 0,72). Dies übertraf einen industriellen Ansatz um 0,20 Punkte im F1-Score.
  • Reale Bugs: NESA entdeckte 13 echte Speicherleck-Bugs in den Projekten h3 (Uber) und dynamips, die alle von den Entwicklern bestätigt und behoben wurden.

• Effizienz und Kosten:

  • Obwohl NESA pro Fall mehr Token verbraucht als einfache Prompting-Ansätze, ist es effizienter pro erkanntem Fehler (Cost-Recall-Ratio).
  • Die Anpassung ist sehr leichtgewichtig: Eine typische Analyse-Policy besteht aus ca. 11 Regeln und einer Prompt-Datei von nur ~43 Zeilen.

• Vergleich mit Baselines:

  • NESA übertraf sowohl reine LLM-Ansätze (GPT-3.5, GPT-4, Claude) als auch nicht-prompting-basierte Tools (wie Pinpoint) in der Gesamtleistung, insbesondere bei der Anpassungsfähigkeit und der Vermeidung von False Positives durch kontextuelle Einschränkungen.

5. Bedeutung und Ausblick

NESA adressiert die kritischen Lücken der aktuellen statischen Analyse: die Abhängigkeit von der Kompilierung und die mangelnde Anpassbarkeit. Durch die Kombination von symbolischer Strenge (Parser) und semantischer Flexibilität (LLMs) bietet NESA einen neuen Paradigmenwechsel.

• Praktische Relevanz: Die Fähigkeit, Bugs in unvollständigem Code zu finden und Analysen ohne tiefe Compiler-Expertise zu definieren, macht statische Analyse für breitere Entwicklerkreise zugänglich.
• Zukunft: Das Papier schlägt vor, LLMs durch Fine-Tuning mit statischen Fakten zu verbessern und kleinere, spezialisierte Modelle für neuronale Relationen zu verwenden, um die Skalierbarkeit für sehr große Codebasen zu erhöhen.

Zusammenfassend demonstriert NESA, dass neuro-symbolische Ansätze die Zuverlässigkeit von LLMs in der Softwareanalyse signifikant steigern und gleichzeitig die Usability revolutionieren können.