Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition

1. Problemstellung

Die formale Verifikation der Sicherheit (Safety) verteilter und nebenläufiger Systeme ist eine herausfordernde Aufgabe. Der Kern dieser Verifikation liegt in der Entwicklung eines induktiven Invariants (einer Aussage über den Systemzustand, die bei allen Übergängen erhalten bleibt).

• Herausforderung: Obwohl es in den letzten Jahren Fortschritte bei der automatisierten Verifikation (z. B. durch IC3/PDR oder syntaktisch geführte Synthese) gab, sind diese Methoden bei komplexen, industriellen Protokollen oft unvorhersehbar.
• Limitierungen: Automatisierte Werkzeuge funktionieren oft nach dem „Alles-oder-Nichts"-Prinzip. Wenn sie scheitern, bieten sie wenig bis keine Anleitung für den menschlichen Verifizierer, wie ein manueller Beweis aufgebaut werden kann.
• Menschliche Interaktion: In der Praxis erfordern große Verifikationsaufgaben menschliche Führung. Bisherige interaktive Ansätze (wie das Ivy-Framework) oder Theorembeweiser (Coq, Isabelle) haben jedoch Nachteile: Ivy fokussiert sich stark auf Entscheidbarkeit und behandelt Invarianten oft als lineare Liste von Lemmas, was bei großen Beweisen unübersichtlich wird. Theorembeweiser haben eine steile Lernkurve und bieten wenig Automatisierung.
• Ziel: Es fehlt ein Framework, das die Komplexität großer induktiver Beweise durch Kompositionalität handhabbar macht, dem Nutzer Feedback zum Beweisfortschritt gibt und eine lokale Analyse von Teilproblemen ermöglicht.

2. Methodik: Induktive Beweiszerlegung (Inductive Proof Decomposition)

Die Autoren stellen eine neue Methodik vor, die auf der schrittweisen Konstruktion eines induktiven Beweisgraphen (Inductive Proof Graph) basiert.

A. Der induktive Beweisgraph

Dies ist eine formale Datenstruktur, die die logischen Abhängigkeiten innerhalb eines induktiven Invariants explizit macht.

• Struktur: Der Graph besteht aus zwei Arten von Knoten:
  1. Lemma-Knoten ($V_L$): Repräsentieren die Teilaussagen (Lemmas), aus denen das Invariant besteht.
  2. Aktion-Knoten ($V_A$): Repräsentieren die logischen Aktionen des Protokolls (die disjunktiven Teile der Übergangsrelation $T = A_1 \lor \dots \lor A_k$).
• Kanten: Eine Kante verbindet ein Lemma mit einem spezifischen Aktion-Knoten, wenn das Lemma als Unterstützung (Support) für die Induktionsbedingung dieses Lemmas bezüglich dieser Aktion dient.
• Arbeitsweise: Der Verifizierer arbeitet rückwärts vom Ziel-Sicherheitsmerkmal (Safety Property) aus. Wenn ein Knoten nicht induktiv ist (d.h. ein Gegenbeispiel zur Induktion, CTI, existiert), wird ein neues Lemma entwickelt, das dieses Gegenbeispiel ausschließt, und der Graph wird erweitert.

B. Lokale Variablen-Slices (Variable Slicing)

Ein zentrales Merkmal der Methode ist die Fähigkeit, die Analyse auf relevante Variablen zu beschränken.

• Prinzip: Für jeden Aktion-Knoten $(L, A)$ wird eine Teilmenge der Systemvariablen berechnet, die für die Gültigkeit dieses Knotens relevant ist.
• Berechnung: Der Slice umfasst Variablen, die im Vorbedingungen der Aktion ($Pre$), in der Definition des Lemmas ($L$) und in den Update-Ausdrücken der von $L$ betroffenen Variablen vorkommen.
• Vorteil: Dies reduziert die Komplexität der zu analysierenden Gegenbeispiele drastisch, da irrelevante Zustandsvariablen ausgeblendet werden. Der Nutzer muss sich nicht mit dem gesamten monolithischen Zustand befassen, sondern nur mit dem lokalen Kontext.

C. Interaktiver Prozess

Der Prozess wird durch das Tool Scimitar unterstützt:

1. Der Nutzer wählt einen nicht bewiesenen Knoten (mit einem CTI).
2. Das Tool zeigt das Gegenbeispiel an, gefiltert durch den lokalen Variablen-Slice.
3. Der Nutzer entwickelt ein neues Lemma, um das Gegenbeispiel zu widerlegen.
4. Das Lemma wird als neuer Knoten eingefügt und mit dem entsprechenden Aktion-Knoten verbunden.
5. Dieser Prozess wiederholt sich, bis alle Knoten „entladen" (discharged) sind, was bedeutet, dass alle induktiven Beweisverpflichtungen erfüllt sind.

3. Wichtige Beiträge

1. Formalisierung induktiver Beweisgraphen: Definition einer neuen Struktur, die die Abhängigkeiten zwischen Lemmas und Protokollaktionen explizit macht und eine kompositionelle Beweisführung ermöglicht.
2. Methodik der induktiven Beweiszerlegung: Ein Ansatz für interaktive Sicherheitsbeweise, der auf der inkrementellen, gegenbeispielgesteuerten Konstruktion des Graphen basiert.
3. Implementierung und Evaluation: Entwicklung des Tools Scimitar (in Python, mit TLA+ als Eingabeformat) und erfolgreiche Anwendung auf mehrere Protokolle, darunter eine hochkomplexe Spezifikation von Raft.
4. Lokale Slicing-Technik: Ein neuartiges Verfahren zur Projektion irrelevanter Variablen, das die Analyse von Gegenbeispielen für den Menschen erheblich erleichtert.

4. Ergebnisse und Evaluation

Die Autoren wendeten ihre Methode auf fünf verteilte Protokolle an, die in TLA+ spezifiziert waren:

• Protokolle: SimpleConsensus, TwoPhase Commit, AbstractRaft, Bakery (Mutual Exclusion) und AsyncRaft.
• AsyncRaft: Dies ist eine industrielle Spezifikation von Raft mit asynchroner Nachrichtenübermittlung und feinkörnigem lokalem Zustand. Es handelte sich um die erste induktive Invarianten-Entwicklung für ein Raft-Modell dieser Komplexität mit diesem Automatisierungsgrad.
• Ergebnisse:
  • Die Beweise für die komplexen Protokolle (insbesondere AsyncRaft) konnten in etwa 3 Person-Wochen entwickelt werden. Zum Vergleich: Ähnliche manuelle Bemühungen für weniger komplexe Invarianten dauern oft 1-2 Person-Monate.
  • Die Beweisgraphen zeigten eine klare, oft baumartige Struktur, die das Verständnis der Protokolllogik förderte.
  • Die Slicing-Technik reduzierte die Anzahl der zu betrachtenden Variablen pro Schritt signifikant (z. B. auf 33–50 % der Gesamtvariablen).
  • Der Graph deckte Induktionszyklen auf, die in monolithischen Beweisen schwer zu erkennen sind (z. B. Wechselwirkungen zwischen lokalem Zustand und Nachrichten im Netzwerk).

5. Bedeutung und Fazit

Das Paper stellt einen Paradigmenwechsel in der interaktiven Verifikation verteilter Systeme dar.

• Kompositionalität: Anstatt einen riesigen, monolithischen Invarianten zu suchen, zerlegt die Methode das Problem in handhabbare, lokalisierte Teilprobleme.
• Mensch-Maschine-Schnittstelle: Es bietet einen strukturierten Weg, wie ein Mensch mit einem automatisierten Solver zusammenarbeiten kann, wenn dieser allein versagt. Der Graph dient als „Landkarte" des Beweises.
• Skalierbarkeit: Die Methode ermöglicht die Verifikation von Protokollen (wie Raft in voller Detailtiefe), die für rein automatische Werkzeuge derzeit noch zu komplex sind.
• Einblick: Die resultierenden Beweisgraphen sind nicht nur für die Verifikation nützlich, sondern bieten auch wertvolle Einblicke in die Struktur und Korrektheit des Protokolls selbst, indem sie Abhängigkeiten und Zyklen sichtbar machen.

Zusammenfassend bietet „Inductive Proof Decomposition" einen robusten, skalierbaren und intuitiven Ansatz, um die Lücke zwischen vollautomatisierter Verifikation (die oft scheitert) und rein manueller Beweisführung (die sehr mühsam ist) zu schließen.