Combining model checking with simulation-based techniques for protocol verification

Technische Zusammenfassung: Kombination von Model Checking mit simulationsbasierten Techniken zur Protokollverifizierung

Problemstellung
Model Checking ist eine rigorose Technik zur Verifizierung endlicher Zustandsysteme, wird jedoch häufig durch das Zustandsraumexplosionsproblem behindert. Wenn die Systemparameter (z. B. Kanalkapazitäten oder Fenstergrößen) zunehmen, wächst der erreichbare Zustandsraum exponentiell an, was eine erschöpfende Verifizierung unmöglich macht. Diese Arbeit adressiert diese Einschränkung im Kontext von Kommunikationsprotokollen, spezifisch des Alternating Bit Protocol (ABP) und des Sliding Window Protocol (SWP). Während einfachere Abstraktionen wie das Simple Communication Protocol (SCP) direkt verifiziert werden können, führt die Erhöhung der Parameter in ABP und SWP dazu, dass der Zustandsraum die Kapazitäten standardmäßiger Model-Checking-Werkzeuge übersteigt, selbst mit moderner Hardware.

Methodik
Die Autoren schlagen eine hybride Verifizierungsmethodik vor, die Model Checking mit Simulationsrelationen kombiniert, um die Zustandsraumexplosion zu überwinden. Die theoretische Grundlage der Methode basiert auf dem Prinzip, dass, wenn eine konkrete Zustandsmaschine $M$ durch eine abstrakte Zustandsmaschine $M_A$ simuliert wird und $M_A$ eine Invarianteneigenschaft erfüllt, die entsprechende Invariante auch für $M$ gilt.

Die Methodik wird unter Verwendung der Rewriting-Logic-Sprache Maude operationalisiert und umfasst zwei primäre Frameworks:

1. Direkte Simulationsverifizierung:
   Um ein konkretes Protokoll $M$ gegen ein abstraktes Protokoll $M_A$ zu verifizieren:

   • Schritt 1: Durchführung von direktem Model Checking auf der abstrakten Maschine $M_A$, um deren Invarianteneigenschaft zu verifizieren.
   • Schritt 2: Konjektur eines Kandidaten für eine Simulationsrelation $r$ zwischen $M$ und $M_A$. Beweis, dass die Invariante von $M$ logisch aus der Invariante von $M_A$ unter der Annahme von $r$ ableitbar ist, unter Verwendung von statischer Fallunterscheidung (Case Splitting) und Reduktion.
   • Schritt 3: Nachweis, dass $M$ tatsächlich von $M_A$ simuliert wird. Dies beinhaltet die Verifizierung der Simulationsbedingungen (Korrespondenz der Anfangszustände und Erhaltung der Übergänge) für alle Rewrite-Regeln von $M$.
   • Implementierung: Schritt 3 nutzt ein Drei-Befehl-Verfahren in Maude:
     • srew: Um Nachfolgezustände in $M$ unter Verwendung frischer Konstanten zu finden, die beliebige Werte repräsentieren.
     • red: Um zu verifizieren, dass die Simulationsrelation zwischen den konkreten und abstrakten Zuständen hält.
     • search: Um zu bestätigen, dass die abstrakte Maschine in null oder mehreren Schritten einen entsprechenden Zustand erreichen kann.
   • Um trotz der Verwendung von Übersets der erreichbaren Zustände (aufgrund der Unentscheidbarkeit der Erreichbarkeit) die Korrektheit zu gewährleisten, verwenden die Autoren Lemma 1, welches beweist, dass die Verifizierung der Übergangsbedingung über diese Übersets ausreicht, um die Bedingung über die tatsächlichen erreichbaren Zustände zu garantieren.

2. Komposition von Simulationsrelationen:
   Für hochkomplexe Systeme, in denen eine einzelne Abstraktion nicht ausreicht, schlagen die Autoren einen hierarchischen Ansatz vor. Dies beinhaltet das Verketten von Simulationsrelationen (z. B. $SWP \to ABP \to SCP$).

   • Die Invariante des konkretsten Systems wird aus dem intermediären System abgeleitet, welches wiederum aus dem abstraktesten System abgeleitet wird.
   • Dies ermöglicht die Verifizierung von Systemen mit massiven Zustandsräumen durch Nutzung der verifizierten Invarianten einfacherer, geschichteter Abstraktionen.

Wesentliche Beiträge
Die Arbeit präsentiert zwei Hauptbeiträge:

1. Eine Methodik, die Model Checking mit Simulationsrelationen kombiniert, um Systeme zu verifizieren, bei denen direktes Model Checking aufgrund von Zustandsraumexplosion scheitert.
2. Eine Methodik zur Komposition von Simulationsrelationen, die eine hierarchische Verifizierung durch die Verknüpfung mehrerer Schichten von Abstraktionen ermöglicht, um noch größere und komplexere Modelle zu handhaben.

Ergebnisse und Fallstudien
Die Autoren evaluierten ihren Ansatz anhand von drei Protokollen: SCP, ABP und SWP.

• Fallstudie I (ABP):

  • Herausforderung: Direktes Model Checking von ABP mit maxIndex = 64 und maxQueueLength = 32 führte zu einem Timeout (>3.600 Sekunden) aufgrund von Zustandsraumexplosion.
  • Lösung: Die Autoren etablierten eine Simulationsrelation von ABP zum einfacheren SCP.
  • Ergebnis: Der gesamte Verifizierungsprozess (Prüfung von SCP, Ableitung der Invariante und Verifizierung der Simulation) wurde in weniger als 1 Sekunde pro Schritt abgeschlossen. Dies bestätigte, dass ABP seine Invarianteneigenschaft erfüllt, ohne dass eine erschöpfende Zustandsexploration notwendig war.

• Fallstudie II (SWP):

  • Herausforderung: SWP führt Fensterverwaltung und Sequenznummern ein, was einen Zustandsraum schafft, der signifikant größer als der von ABP ist, wodurch eine direkte Verifizierung unmöglich wird.
  • Lösung: Die Autoren nutzten die Komposition von Simulationsrelationen: $SWP \to ABP \to SCP$. Sie verifizierten die Simulation von SWP zu ABP und kombinierten diese mit der zuvor verifizierten ABP-zu-SCP-Relation.
  • Ergebnis: Der hierarchische Ansatz verifizierte erfolgreich die Invarianteneigenschaft von SWP (Sicherstellung, dass Nachrichten in der richtigen Reihenfolge ohne Verlust oder Duplikation empfangen werden) mit Parametern (windowSize = 16, maxQueueLength = 32), die für eine direkte Prüfung nicht machbar gewesen wären.

Bedeutung und Ansprüche
Die Arbeit behauptet, dass dieser Ansatz das Zustandsraumexplosionsproblem effektiv mildert, indem er die Rechenlast von der erschöpfenden Zustandsdurchtrauung hin zur symbolischen Verifizierung auf kleineren, abstrakten Modellen verschiebt. Wesentliche Aspekte der Bedeutung sind:

• Skalierbarkeit: Die Methode ermöglicht die formale Verifizierung von Protokollen mit großen Parametern (z. B. Fenstergrößen und Warteschlangenlängen), die jenseits der Reichweite von direktem Model Checking liegen.
• Wiederverwendbarkeit: Bestehende formale Spezifikationen können als abstrakte Modelle für neue, komplexere Zielmodelle wiederverwendet werden, was den Verifizierungsaufwand erheblich reduziert.
• Automatisierung und Rigorosität: Während die Konstruktion der abstrakten Modelle und Simulationsrelationen manuelles Domänenwissen erfordert, wird die Gültigkeit dieser Relationen mittels standardmäßiger Maude-Befehle semi-automatisch verifiziert. Die Autoren entwickelten ein Support-Tool, um die Fallunterscheidung und Befehlsausführung zu automatisieren und menschliche Fehler zu minimieren.
• Abgrenzung zu bestehender Arbeit: Im Gegensatz zu Counterexample-Guided Abstraction Refinement (CEGAR), das reaktiv ist und Modelle basierend auf spuriösen Gegenbeispielen verfeinert, ist dieser Ansatz proaktiv und nutzt Domänenwissen, um strategische Abstraktionen zu konstruieren. Dies bietet eine verbesserte Transparenz und Interpretierbarkeit, da die Simulationsrelationen eine für Menschen verständliche Abbildung zwischen konkreten und abstrakten Verhaltensweisen aufrechterhalten.

Die Autoren schließen, dass sie durch die Operationalisierung der Simulationstheorie in eine standardisierte Sequenz von Maude-Befehlen die Lücke zwischen abstrakten theoretischen Relationen und ausführbaren Verifizierungs-Workflows geschlossen haben, was einen praktischen und effizienten Weg zur Verifizierung komplexer verteilter Systeme eröffnet.