A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

Das Paper stellt Preguss vor, ein modulares Framework, das durch die Kombination von statischer Analyse und LLM-gestützter Spezifikationssynthese die automatisierte Verifikation von Programmen mit über 1000 Zeilen Code ermöglicht und dabei den menschlichen Aufwand um 80,6 % bis 88,9 % reduziert.

Das Wesentliche

Hier ist eine einfache Erklärung der Forschungspapier „A Tale of 1001 LoC" (Eine Geschichte von 1001 Zeilen Code), angepasst für ein allgemeines Publikum, mit ein paar kreativen Vergleichen.

Das große Problem: Der riesige Bauplan

Stellen Sie sich vor, Sie haben einen riesigen, komplexen Bauplan für ein Hochhaus (ein Computerprogramm). Dieser Plan ist so lang, dass er sich über Tausende von Seiten erstreckt (über 1000 Zeilen Code).

Ihre Aufgabe ist es, als Sicherheitsinspektor zu garantieren, dass das Gebäude sicher ist. Sie wollen sicherstellen, dass keine Türe zufällig aufspringt, kein Wasserrohr platzt und niemand stolpert (das nennt man „Laufzeitfehler" oder Runtime Errors).

Das Problem: Wenn Sie versuchen, den gesamten Plan auf einmal zu lesen, um alle Fehler zu finden, wird Ihr Gehirn (oder ein Computer) überlastet. Es ist zu viel Information auf einmal.

Die alten Methoden: Der müde Inspektor

Bisher gab es zwei Ansätze:

1. Der strenge Prüfer (Statische Analyse): Ein Computerprogramm schaut sich den Plan an und markiert jede potenzielle Gefahr. Das Problem: Es ist so vorsichtig, dass es auch Dinge als gefährlich markiert, die gar keine sind (z. B. „Achtung, hier könnte theoretisch ein Loch sein", obwohl es fest ist). Das nennt man „falsche Alarme". Menschen müssen dann stundenlang prüfen, ob diese Alarme echt sind.
2. Der KI-Assistent (Große Sprachmodelle): Man hat versucht, eine künstliche Intelligenz (KI) zu bitten, die Sicherheitsregeln zu schreiben. Aber die KI war oft verwirrt, weil der Plan zu lang war, oder sie schrieb Regeln, die zwar klangen, aber nicht genau passten.

Die neue Lösung: Preguss – Der clevere Bauleiter

Die Forscher haben Preguss entwickelt. Man kann sich Preguss wie einen sehr cleveren Bauleiter vorstellen, der zwei Dinge perfekt kombiniert: einen strengen Prüfer und eine KI.

Preguss arbeitet in zwei Schritten, ähnlich wie beim Lösen eines riesigen Puzzles:

Schritt 1: Das Puzzle teilen (Teilen)

Statt das ganze riesige Puzzle auf einmal zu lösen, schaut sich Preguss zuerst an, wo der strenge Prüfer Alarme geschlagen hat.

• Die Analogie: Stellen Sie sich vor, der Prüfer sagt: „Hier an der Treppe könnte es rutschig sein!" und „Hier am Fenster könnte der Rahmen locker sein!".
• Preguss nimmt diese spezifischen Alarme und baut darum herum kleine, überschaubare Arbeitsgruppen (die sogenannten „Verifizierungseinheiten"). Es ignoriert den Rest des Gebäudes, der gerade sicher aussieht. So wird die Aufgabe für die KI viel kleiner und handhabbar.

Schritt 2: Die KI ins Spiel bringen (Erobern)

Jetzt kommt die KI ins Spiel, aber sie bekommt keine Aufgabe mehr, das ganze Haus zu verstehen.

• Die Analogie: Preguss sagt zur KI: „Du musst nur wissen, wie die Treppe beschaffen sein muss, damit sie nicht rutscht, und wie das Fenster montiert sein muss."
• Die KI schreibt dann genau die richtigen Sicherheitsregeln (Spezifikationen) für diesen kleinen Bereich.
• Der Clou: Preguss ist schlau genug zu erkennen, dass die Treppe von der KI im ersten Stock beeinflusst wird. Also schickt es die KI auch zum ersten Stock, um dort die Regeln zu schreiben, damit die Treppe unten sicher ist. Es verbindet also die verschiedenen Etagen (Funktionen) des Gebäudes.

Warum ist das so genial?

1. Keine Überforderung: Weil Preguss das Problem in kleine Häppchen zerlegt, kann die KI sich auf das Wesentliche konzentrieren. Sie muss nicht den ganzen 1000-Seiten-Plan lesen, sondern nur die relevanten 5 Seiten für den aktuellen Alarm.
2. Falsche Alarme entlarven: Oft sagt der strenge Prüfer „Hier ist eine Gefahr!", aber eigentlich ist alles in Ordnung. Preguss nutzt die KI, um zu beweisen: „Nein, hier ist es sicher, weil wir diese Regel haben." So spart man sich das manuelle Durchsuchen von Hunderten von falschen Alarmen.
3. Echte Gefahren finden: In einem echten Test mit einem Satelliten-Steuerungssystem (ein sehr komplexes Programm) hat Preguss nicht nur die Sicherheit bestätigt, sondern 6 echte, versteckte Fehler gefunden, die sonst niemand bemerkt hätte. Das ist wie ein Detektiv, der nicht nur den Plan prüft, sondern auch einen versteckten Riss in der Wand findet.

Das Ergebnis

Mit Preguss konnten die Forscher Programme mit über 1000 Zeilen Code fast vollständig automatisch auf Sicherheit prüfen.

• Der menschliche Aufwand sank um 80% bis 89%. Das bedeutet: Statt dass ein Experte wochenlang den Plan durchforsten muss, reicht es, wenn er sich die wenigen Punkte ansieht, die Preguss nicht selbst lösen konnte.
• Es ist der erste Schritt, um riesige, komplexe Software-Systeme (wie die in Autos, Flugzeugen oder Satelliten) sicher und automatisch zu überprüfen.

Zusammenfassend: Preguss ist wie ein intelligenter Assistent, der den riesigen Berg an Arbeit in kleine, machbare Hügel zerlegt, die KI genau dort hinschickt, wo sie gebraucht wird, und so sicherstellt, dass das große Gebäude sicher steht – ohne dass ein Mensch jede einzelne Schraube von Hand nachziehen muss.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs" auf Deutsch:

1. Problemstellung

Die vollständige automatische Verifikation großer Software- und Hardwaresysteme gilt als „Heiliger Gral" der formalen Methoden. Ein zentrales Hindernis ist die Spezifikationssynthese: Deduktive Verifizierer (wie Frama-C/Wp) benötigen formale Spezifikationen (Vorbedingungen, Nachbedingungen, Schleifeninvarianten), um die Korrektheit eines Programms zu beweisen. Das manuelle Erstellen dieser Spezifikationen für große Programme ist extrem aufwendig und fehleranfällig.

Zwar haben Large Language Models (LLMs) gezeigt, dass sie Spezifikationen generieren können, stoßen jedoch bei großen, realen Programmen (oft >1000 Zeilen Code) an Grenzen:

• Kontextbeschränkungen: LLMs können oft nicht den gesamten Programmcode in einem Durchgang verarbeiten.
• Interprozedurale Komplexität: Die Synthese von Spezifikationen, die über Funktionsgrenzen hinweg wirken (z. B. Nachbedingungen von Hilfsfunktionen, die Vorbedingungen der aufrufenden Funktion erfüllen), ist für bestehende LLM-Ansätze schwierig.
• Falsche Spezifikationen: LLMs neigen dazu, übermäßig restriktive Vorbedingungen zu generieren, die zu falschen Alarmen führen, oder unzureichende Spezifikationen, die echte Laufzeitfehler (RTEs) nicht abdecken.

Das Ziel ist es, die Laufzeitfehler-Freiheit (RTE-freeness) – also das Fehlen von undefiniertem Verhalten wie Division durch Null, Pufferüberläufen oder Nullzeiger-Dereferenzierung – für große C-Programme automatisiert zu verifizieren.

2. Methodik: Das Preguss-Framework

Die Autoren stellen Preguss vor, ein modulares, feinabgestuftes Framework, das statische Analyse und deduktive Verifikation durch eine „Teile-und-Herrsche"-Strategie (Divide-and-Conquer) synergistisch verbindet. Der Prozess gliedert sich in zwei Phasen:

Phase 1: Potential-RTE-gesteuerte Konstruktion und Priorisierung von Verifikationseinheiten (Divide)

• Statische Analyse: Zuerst wird das Programm mit einem abstrakt-interpretationsbasierten Analyser (z. B. Frama-C/Eva oder Frama-C/Rte) analysiert. Dieser generiert Assertions (Behauptungen) an potenziellen Stellen von Laufzeitfehlern (RTEs).
• Verifikationseinheiten (V-Units): Anstatt das gesamte Programm auf einmal zu verifizieren, wird das Problem in handhabbare Einheiten zerlegt. Jede V-Unit besteht aus:
  • Einer Guard-Assertion (eine RTE-Assertion oder eine Vorbedingung an einer Aufrufstelle).
  • Einem minimierten Programmkontext, der nur die aufrufende Funktion (Host) und ihre aufgerufenen Funktionen (Callees) enthält.
• Priorisierung: Die V-Units werden in einer Warteschlange sortiert. Die Sortierung erfolgt bottom-up entlang des Aufrufgraphen: Zuerst werden Funktionen verifiziert, die keine weiteren Funktionen aufrufen (oder deren Verträge bereits bekannt sind), bevor zu deren Aufrufern übergegangen wird. Dies verhindert, dass der Kontext für das LLM unnötig groß wird.

Phase 2: Feinabgestufte Synthese interprozeduraler Spezifikationen (Conquer)

Für jede V-Unit in der Warteschlange wird ein iterativer Prozess gestartet, der ein LLM und einen deduktiven Verifizierer (Frama-C/Wp) abwechselnd nutzt:

1. Verifizierungsversuch: Der Verifizierer prüft, ob die aktuelle Guard-Assertion unter den bereits bekannten Spezifikationen gilt.
2. Feedback-Loop: Falls die Verifikation scheitert (Status: unknown), nutzt Preguss die Beweisverpflichtungen (Proof Obligations) und Fehlermeldungen des Verifizierers als Feedback für das LLM.
3. Spezifikationssynthese: Das LLM generiert gezielt neue Spezifikationen basierend auf dem Kontext:
   • Für die Host-Funktion: Generierung von Vorbedingungen (Preconditions) und Schleifeninvarianten.
   • Für die Callee-Funktionen: Generierung von Nachbedingungen (Postconditions).
   • Wichtig: Das System verhindert bewusst die Generierung von Vorbedingungen für Callee-Funktionen in diesem Schritt, um übermäßig restriktive Annahmen zu vermeiden.
4. Validierung und Korrektur: Generierte Spezifikationen werden auf syntaktische Korrektheit und semantische Erfüllbarkeit geprüft. Fehlerhafte Kandidaten werden verworfen oder korrigiert.
5. Iteration: Der Prozess wiederholt sich, bis die Assertion bewiesen ist oder eine maximale Iterationszahl erreicht ist.

Soundness und Terminierung

• Soundness: Wenn Preguss eine Verifikation als erfolgreich meldet, ist das Programm garantiert RTE-frei unter den angenommenen Hypothesen.
• Terminierung: Durch die statische Konstruktion der Warteschlange und die Beschränkung der Iterationen garantiert das System, dass der Prozess endet.

3. Hauptbeiträge

1. Konzept der Potential-RTE-gesteuerten Synthese: Die Autoren formalisieren die Idee, statische Analyse-Alarme (RTE-Assertions) als Leitfaden für LLMs zu nutzen, um gezielt notwendige Spezifikationen zu erzeugen, anstatt blind zu synthetisieren.
2. Das Preguss-Framework: Ein modulares System, das als erste automatisierte Methode nachweislich RTE-Freiheit für reale Programme mit über 1.000 Zeilen Code (LoC) mit minimalem menschlichem Aufwand nachweisen kann.
3. Open-Source-Datensatz: Erstellung eines Datensatzes aus realen C-Programmen, die mit von Preguss generierten und von Experten verfeinerten Spezifikationen annotiert sind.
4. Implementierung und Evaluation: Eine vollständige Implementierung und umfangreiche Evaluierung, die zeigt, dass Preguss den State-of-the-Art (z. B. AutoSpec) deutlich übertrifft.

4. Ergebnisse

Die Evaluation umfasste den Benchmark Frama-C-Problems sowie vier reale Großprojekte (Contiki, X509-parser, SAMCODE, Atomthreads) mit bis zu 1.451 Zeilen Code.

• Vergleich mit State-of-the-Art: Auf dem Frama-C-Problems-Benchmark erreichte Preguss eine Erfolgsrate von 79,7 % (46 von 51 Programmen), während AutoSpec nur bei 32,7 % erfolgreich war. Preguss ist zudem deutlich schneller (durchschnittlich 4x schneller) und benötigt weniger LLM-Token pro erfolgreichem Beweis, da es gezielter arbeitet.
• Skalierbarkeit: Preguss konnte RTE-Freiheit für Programme mit über 1.000 Zeilen Code (z. B. SAMCODE mit 1.280 LoC) hochautomatisiert verifizieren.
• Reduktion des menschlichen Aufwands: Der menschliche Aufwand zur Verifikation wurde um 80,6 % bis 88,9 % reduziert (gemessen an der Anzahl der manuell anzupassenden Spezifikationen).
• Entdeckung echter Fehler: In dem nicht-öffentlichen Satellitensteuerungssystem SAMCODE identifizierte Preguss 6 bestätigte echte Laufzeitfehler (uninitialisierte Zugriffe), die zuvor unbekannt waren. Dies demonstriert die Fähigkeit des Systems, nicht nur falsche Alarme zu entfernen, sondern echte Bugs zu finden.

5. Bedeutung und Fazit

Das Paper zeigt einen vielversprechenden Weg zur automatisierten Verifikation großer Softwaresysteme auf. Durch die Kombination von statischer Analyse (zur Identifikation von Problemstellen) und deduktiver Verifikation (unterstützt durch LLMs) gelingt es, die Skalierbarkeit von LLMs in der formalen Verifikation zu überwinden.

• Praktische Relevanz: Die Reduktion des manuellen Aufwands macht formale Verifikation für industrielle Anwendungen (wie Raumfahrtsteuerung oder IoT-Betriebssysteme) realistischer.
• Methodischer Fortschritt: Die „Teile-und-Herrsche"-Strategie mit kontextbewusster Spezifikationssynthese adressiert effektiv die Limitierungen von LLMs bezüglich Kontextlänge und komplexer Aufrufhierarchien.
• Zukunftsaussichten: Obwohl das System noch Herausforderungen bei komplexen Datenstrukturen (z. B. verkettete Listen) und externen Bibliotheken hat, legt es den Grundstein für vollständig automatisierte Verifikationspipelines in der Industrie.

Zusammenfassend beweist Preguss, dass die Integration von LLMs in formale Verifikationswerkzeuge, wenn sie durch statische Analyse geleitet und feinabgestuft gesteuert werden, eine transformative Wirkung auf die Zuverlässigkeit großer Softwareprojekte haben kann.