A Deductive System for Contract Satisfaction Proofs

Dieses Paper stellt ein in Rocq formalisiertes, vollständiges und korrektes deduktives Beweissystem vor, das relative Spurgleichheit und relative Bisimulation nutzt, um die Einhaltung von Hardware-Software-Verträgen zur Vermeidung von Seitenkanalangriffen modular und interaktiv zu verifizieren.

Das Wesentliche

Das große Problem: Der lauschende Nachbarn im Cloud-Server

Stell dir vor, du mietest einen Rechenraum in einer riesigen Cloud. Du hast geheime Daten (wie Passwörter oder Bankdaten), und ein anderer Nutzer hat vielleicht bösartige Absichten. Beide nutzen denselben Computer-Chip (CPU).

Das Problem: Selbst wenn du deine Daten verschlüsselst, hinterlassen deine Berechnungen winzige Spuren im Inneren des Chips – ähnlich wie Fußabdrücke im Sand oder ein warmer Ofen, der verrät, dass gerade gekocht wurde. Diese Spuren nennt man Seitenkanäle. Ein cleverer Angreifer kann diese Spuren beobachten und daraus deine Geheimnisse erraten (bekannt durch Attacken wie "Spectre" oder "Meltdown").

Die Lösung: Der "Vertrag" zwischen Software und Hardware

Um sich zu schützen, brauchen wir eine Art Vertrag zwischen dem Software-Entwickler und dem Hardware-Hersteller.

• Der Vertrag (Contract): Das ist eine vereinfachte Beschreibung dessen, was der Chip theoretisch preisgeben darf. Er sagt: "Wenn du diesen Code ausführst, darfst du nur diese und jene Informationen über die Spur abgeben."
• Die Realität (Hardware): Der echte Chip ist komplex, hat viele Tricks (wie Vorhersagen von Entscheidungen) und ist schwer zu verstehen.

Damit der Vertrag funktioniert, muss bewiesen werden, dass der echte Chip niemals mehr preisgibt als der Vertrag zulässt. Wenn der Vertrag sagt "Ich zeige nur die Adresse", darf der Chip nicht auch noch den Inhalt des Speichers verraten.

Das Problem mit dem Beweis: Der "Pen-and-Paper"-Albtraum

Früher haben Mathematiker versucht, diese Sicherheit auf einem Blatt Papier zu beweisen. Das Problem: Diese Beweise waren so lang und kompliziert (manchmal 25 Seiten voller Formeln!), dass kaum jemand sie wirklich nachvollziehen konnte. Ein kleiner Fehler in der Rechnung könnte bedeuten, dass der Chip doch unsicher ist.

Andere Methoden nutzen Computer, die alles automatisch durchprobieren (Modellprüfung). Das ist gut, aber wenn der Computer einen Fehler macht oder die Suche abbricht, weiß man nicht, ob der Chip sicher ist oder nicht.

Die neue Idee: Ein interaktiver Beweis-Assistent

Die Autoren dieses Papers haben eine neue Methode entwickelt, die wie ein kooperatives Spiel zwischen Mensch und Computer funktioniert. Sie nutzen ein Werkzeug namens "Rocq" (ein Beweis-Assistent), das wie ein sehr strenger, aber hilfsbereiter Tutor agiert.

Statt einen riesigen Beweis auf einmal zu schreiben, bauen sie ihn Schritt für Schritt auf.

Die Metapher: Der "Relative Bisimulation"-Tanz

Stell dir vor, du hast vier Tänzer:

1. Tänzer A & B: Zwei Versionen deines Programms, die auf dem Vertrag laufen (eine mit Geheimnis X, eine mit Geheimnis Y).
2. Tänzer C & D: Zwei Versionen deines Programms, die auf dem echten Chip laufen (ebenfalls mit X und Y).

Das Ziel: Wenn Tänzer A und B (Vertrag) genau dieselben Schritte machen und dieselben Spuren hinterlassen, dann müssen auch Tänzer C und D (Chip) dieselben Spuren hinterlassen.

Die Herausforderung:

• Der Vertrag ist oft "langsam" oder macht Dinge anders als der Chip.
• Der Chip macht vielleicht einen Sprung, während der Vertrag erst noch überlegt.
• Manchmal läuft der Chip schneller, manchmal der Vertrag. Sie sind nicht synchron.

Frühere Methoden verlangten, dass man vorher eine perfekte Choreografie (eine "Simulation") für alle vier Tänzer entwirft. Das ist extrem schwer.

Der neue Trick (Relative Bisimulation):
Die Autoren haben ein System entwickelt, bei dem man die Choreografie während des Tanzes erfinden kann.

• Sie nutzen eine Technik namens "Koinduktion" (ein mathematisches Werkzeug für unendliche Prozesse).
• Man sagt dem Computer: "Ich behaupte, diese vier Tänzer sind sicher verbunden."
• Der Computer fragt: "Okay, was passiert im nächsten Schritt?"
• Man antwortet: "Schauen wir mal. Wenn der Vertrag hier einen Schritt macht, darf der Chip hier einen Schritt machen. Wenn der Chip hier einen Schritt macht, darf der Vertrag warten."
• Der Computer merkt sich diese Regeln (die "Invarianten") und baut sie Schritt für Schritt auf.

Es ist wie beim Lösen eines Labyrinths: Man muss nicht den ganzen Weg auf einmal sehen. Man geht einen Schritt, merkt sich die Regel ("Wenn ich links gehe, muss ich rechts warten"), und baut so den Pfad zur Sicherheit auf.

Warum ist das cool?

1. Modularität: Man kann Teile des Beweises wie Lego-Steine bauen und wiederverwenden.
2. Fehlerresistenz: Da der Beweis-Assistent (Rocq) jede einzelne logische Schlussfolgerung überprüft, kann man sich sicher sein, dass der Beweis stimmt. Keine versteckten Fehler mehr.
3. Flexibilität: Das System erlaubt es, dass der Vertrag und der Chip nicht im exakt gleichen Takt tanzen müssen (asynchron). Das ist in der realen Welt (bei modernen Chips mit Vorhersagen) absolut notwendig.

Zusammenfassung in einem Satz

Die Autoren haben ein neues, interaktives Werkzeug gebaut, das es Ingenieuren erlaubt, Schritt für Schritt und mit Hilfe eines Computers zu beweisen, dass ein Computer-Chip seine Geheimnisse nicht verrät, selbst wenn er komplexe Tricks wie "Vorhersagen" verwendet – ganz ohne endlose, fehleranfällige Papier-Beweise.

Das Ergebnis: Wir können jetzt mit viel mehr Vertrauen sagen: "Ja, dieser Chip hält sich an den Sicherheitsvertrag, und deine Daten sind sicher."

Technische Zusammenfassung

1. Problemstellung und Motivation

Hintergrund:
Bei der Ausführung von Programmen auf geteilter Hardware (z. B. in Cloud-Umgebungen) können geheime Daten über Mikroarchitektur-Komponenten (Caches, Branch-Predictoren, Puffer) an Angreifer geleakt werden. Bekannte Angriffe wie Meltdown und Spectre haben die Dringlichkeit von Verteidigungsmechanismen gegen solche Side-Channel-Attacken unterstrichen.

Hardware-Software-Verträge:
Um Software-Entwicklern die Analyse von Leckagen zu erleichtern, ohne tiefes Wissen über die Mikroarchitektur zu benötigen, wurden „Hardware-Software-Verträge" eingeführt. Diese sind abstrakte Spezifikationen auf Ebene der Instruction Set Architecture (ISA), die das erwartete Leckage-Verhalten eines Prozessors beschreiben.
Ein Vertrag ist korrekt, wenn er das tatsächliche Leckage-Verhalten der Hardware überapproximiert. Dies wird als Vertragserfüllung (Contract Satisfaction) bezeichnet: Wenn der Vertrag für zwei verschiedene Eingaben das gleiche Leckage-Verhalten vorhersagt, müssen auch die tatsächlichen Hardware-Ausführungen ununterscheidbar sein.

Die Herausforderung:
Der Nachweis der Vertragserfüllung ist komplex, da er eine relationale Eigenschaft (ein Hyper-Eigenschaft) darstellt, die vier Ausführungsstränge gleichzeitig betrachtet:

1. Zwei Verträge (Contract Traces) mit unterschiedlichen Eingaben.
2. Zwei Hardware-Ausführungen (Hardware Traces) mit denselben Eingaben.

Bisherige Ansätze basierten auf Modellprüfung (Model Checking) oder manuellen Beweisen („Pen-and-Paper").

• Modellprüfung: Oft automatisiert, aber abhängig von der Korrektheit der Algorithmen und Implementierungen; kann bei komplexen Invarianten scheitern.
• Manuelle Beweise: Sehr fehleranfällig und schwer zu verifizieren (ein Beispiel im Paper erstreckt sich über 25 dichte Seiten).

Das Ziel dieses Papers ist es, einen deduktiven Beweisführer zu entwickeln, der in einem interaktiven Beweisassistenten (Rocq, ehemals Coq) implementiert ist, um diese Beweise formal, modular und schrittweise zu führen.

2. Methodik und Kernkonzepte

Das Paper löst das Problem durch die Einführung eines neuen Beweissystems, das auf relativer Bisimulation basiert.

A. Relative Spurgleichheit (Relative Trace Equality)

Die Vertragserfüllung wird als Spezialfall eines allgemeineren Problems definiert: „Spurgleichheit impliziert Spurgleichheit".
Formal: Wenn die Spuren zweier Vertragsexecutionen gleich sind ($\llbracket P \rrbracket_C(s_1) = \llbracket P \rrbracket_C(s_2)$), dann müssen auch die Spuren der Hardware-Executionen gleich sein ($\llbracket P \rrbracket_H(h_1) = \llbracket P \rrbracket_H(h_2)$).

B. Relative Bisimulation (Relative Bisimilarity)

Um diese Eigenschaft zustandsbasiert (statt spurbasiert) zu beweisen, wird eine 4-stellige Relation eingeführt.

• Lockstep vs. Asynchronität: Ein naiver Ansatz würde alle vier Zustände synchron („lockstep") fortschreiten lassen. Dies ist jedoch unzureichend, da Verträge und Hardware unterschiedlich schnell fortschreiten können (z. B. spekuliert die Hardware, während der Vertrag beide Pfade simuliert, oder umgekehrt).
• Lösung: Das Paper definiert eine relative Bisimulation, die eine Mischung aus koinduktivem und induktivem Denken erlaubt:
  • Hardware-Schritte werden koinduktiv behandelt (Greatest Fixpoint): Man muss zeigen, dass die Leckagen übereinstimmen und die Nachfolgerzustände wieder in der Relation liegen.
  • Vertragsschritte werden induktiv behandelt (Least Fixpoint): Man darf Schritte auf der Vertragsseite überspringen, solange die Leckage-Unterschiede nachgewiesen werden können. Dies erlaubt es, „asynchrone" Sprünge zu modellieren, ohne die Korrektheit zu verlieren.

C. Deduktives System mit Parametrisierter Koinduktion (Parameterized Coinduction)

Um die Beweise in einem Beweisassistenten effizient zu gestalten, nutzen die Autoren das Framework der parametrisierten Koinduktion (Paco).

• Statt eine vollständige Invariante (die Bisimulationsrelation) von vorneherein anzugeben, wird diese inkrementell während des Beweises aufgebaut.
• Das System verwendet Beweis-Quintupel ($R \vdash \dots$), die den aktuellen Beweisstatus und die gesammelte Hypothese ($R$) repräsentieren.
• Regeln: Das System bietet Regeln wie C-Step (Vertragsschritt), H-Step (Hardware-Schritt), Invariant (Hinzufügen neuer Paare zur Hypothese) und Cycle (Abschluss, wenn der aktuelle Zustand in der Hypothese liegt).

D. Up-To-Techniken

Das System integriert Techniken zur Vereinfachung von Beweisen („Up-To"):

• Symmetrie: Vertauschen von Zuständen.
• Transitivität: Ersetzen von Zuständen durch äquivalente, die weniger (oder mehr) Leckage aufweisen, um Beweise zu zerlegen.
• Diese Techniken sind mathematisch als „kompatible Funktionen" formalisiert, die sicher in das koinduktive System integriert werden können.

3. Wichtige Beiträge

1. Formale Definition der relativen Bisimulation: Eine sound und complete Charakterisierung der relativen Spurgleichheit durch eine 4-stellige Relation, die asynchrone Abläufe zwischen zwei Semantiken (Vertrag vs. Hardware) korrekt handhabt.
2. Deduktives Beweissystem: Entwicklung eines deduktiven Systems, das auf parametrisierter Koinduktion basiert. Es ermöglicht einen modularen Beweisstil, bei dem Invarianten schrittweise konstruiert werden, anstatt sie vollständig vorzugeben.
3. Integration von Up-To-Techniken: Erweiterung des Systems um Regeln, die Symmetrie und Transitivität ausnutzen, um Beweise drastisch zu vereinfachen.
4. Formalisierung in Rocq: Das gesamte System wurde im Beweisassistenten Rocq formalisiert und auf seine Soundness und Vollständigkeit überprüft.
5. Fallstudien: Anwendung des Systems auf zwei komplexe Szenarien:
   • Always-Mispredict Contract: Beweis, dass ein Hardware-Modell mit Branch-Spekulation einen Vertrag erfüllt, der immer beide Pfade spekulativ ausführt (Abstraktion von Spectre-artigen Angriffen).
   • Sequential Contract: Beweis für ein Hardware-Modell mit Out-of-Order-Ausführung, das durch einen sequentiellen Vertrag abstrahiert wird.

4. Ergebnisse

• Korrektheit: Das deduktive System wurde mathematisch bewiesen als sound (jeder bewiesene Satz ist wahr) und complete (jeder wahre Satz kann bewiesen werden).
• Praktische Anwendbarkeit: Die Autoren konnten erfolgreich zwei anspruchsvolle Verträge für einfache Hardware-Modelle verifizieren.
  • Im Fall des „Always-Mispredict"-Contracts konnte gezeigt werden, dass die asynchrone Natur des Beweissystems (Überspringen von Vertragsschritten, wenn die Hardware korrekt spekuliert) entscheidend ist, um die Beweise handhabbar zu machen.
  • Die Beweise waren modular und nutzten die „Up-To"-Techniken, um Redundanzen zu eliminieren.
• Vergleich: Im Gegensatz zu Modellprüfung, die oft bei der Suche nach Invarianten scheitert oder nicht terminiert, liefert das deduktive System einen strukturierten, vom Benutzer geführten (aber assistierten) Beweis, der die Intuition hinter der Abstraktion explizit macht.

5. Bedeutung und Ausblick

Bedeutung:
Dieses Paper stellt einen Paradigmenwechsel in der Verifikation von Hardware-Sicherheit dar. Es bietet erstmals ein fundamentales, deduktives Fundament für den Nachweis von Vertragserfüllung, das die Lücke zwischen abstrakten Spezifikationen und konkreten Mikroarchitekturen schließt. Es ermöglicht es, komplexe Sicherheitsgarantien (wie Schutz vor Side-Channel-Angriffen) formal und maschinenüberprüfbar zu beweisen, ohne auf Black-Box-Tests oder unvollständige Modellprüfung angewiesen zu sein.

Zukunftsaussichten:

• Erweiterung auf nicht-deterministische Systeme: Das aktuelle System geht von deterministischer Semantik aus. Die Erweiterung auf Nicht-Determinismus (z. B. durch Quantoren-Alternierung) ist eine offene Herausforderung.
• Verschachtelte Spekulation (Nested Speculation): Die Behandlung von komplexeren Spektren der Spekulation (Stacks vs. Puffer) erfordert noch feinere Invarianten.
• Programlogik: Das Ziel ist es, die Beweise noch abstrakter zu gestalten, ähnlich wie bei Separation Logics, um Beweise für große Programme modularer zu machen, anstatt nur über konkrete Zustandsquadrupel zu reasoning.

Zusammenfassend bietet das Paper ein leistungsfähiges Werkzeug für die formale Verifikation von Hardware-Sicherheit, das die Komplexität relationaler Beweise durch innovative Anwendung der Koinduktion beherrschbar macht.