💻 computer science

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL

Diese Arbeit präsentiert einen mechanisierten Isabelle/HOL-Beweis, der sowohl Sicherheits- als auch Lebendigkeitsgarantien für die domänenübergreifende Erhaltung des regulatorischen Zustands unter Byzantinischen Fehlern etabliert, indem ein wiederverwendbares Framework aus sieben generischen Locales verwendet wird, die gegen ein umfassendes Modell globaler Finanzregulierungsanforderungen instanziiert sind.

Ursprüngliche Autoren: Jinwook Kim

Veröffentlicht 2026-06-01

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Jinwook Kim

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich eine Welt vor, in der digitale Vermögenswerte (wie tokenisierte Aktien oder Immobilien) frei zwischen verschiedenen „Nachbarschaften“ (Blockchains) und „Papier-Hauptbüchern“ (Off-Chain-Systemen) bewegt werden können. Das Problem ist: Wenn ein Richter in Nachbarschaft A einen Vermögenswert einfriert, muss diese Einfrierung auch in Nachbarschaft B, Nachbarschaft C und im Papier-Hauptbuch sofort und perfekt erfolgen. Wenn dies nicht geschieht, könnten Akteure „Regulierungsarbitrage“ betreiben, indem sie Vermögenswerte an Orten verstecken, an denen die Regeln nicht durchgesetzt werden.

Dieses Paper ist ein mathematischer Beweis, dass ein spezifisches System für die Bewegung dieser Vermögenswerte sowohl sicher (es macht niemals Fehler) als auch lebendig (es bleibt niemals stecken) ist, selbst wenn einige Teilnehmer versuchen, es zu sabotieren.

Hier ist die Aufschlüsselung unter Verwendung einfacher Analogien:

1. Das Ziel: Der „perfekte Staffellauf“

Betrachten Sie das System als einen Staffellauf, bei dem der Staffelstab ein „regulatorischer Status“ (wie „Eingefroren“ oder „Aktiv“) ist.

Die Herausforderung: Wenn ein Läufer (eine Blockchain) die Farbe des Staffelstabs ändert, muss jeder andere Läufer im Team sofort dieselbe Farbe sehen.
Das Risiko: Wenn ein Läufer lügt, vergisst oder stecken bleibt, könnte das gesamte Rennen stoppen oder der Staffelstab könnte gleichzeitig zwei verschiedene Farben haben.

2. Die zwei großen Erfolge (Sicherheit und Lebendigkeit)

Die Autoren haben zwei Dinge über ihr System bewiesen:

A. Sicherheit: Der „unzerbrechliche Spiegel“

Was es bedeutet: Wenn das System funktioniert, ist das Ergebnis immer konsistent. Wenn Kette A „Einfrieren“ sagt, muss Kette B auch „Einfrieren“ sagen. Es gibt keine Mehrdeutigkeit.
Die Analogie: Stellen Sie sich einen Satz magischer Spiegel vor. Wenn Sie einen roten Ball vor Spiegel A halten, zeigen Spiegel B, Spiegel C und das Papierprotokoll alle einen roten Ball. Sie zeigen niemals einen blauen Ball, und sie widersprechen sich nie.
Der Beweis: Die Autoren haben eine „Landkarte“ (genannt Locale) erstellt, die beweist, dass dieses Spiegeln perfekt geschieht, selbst wenn die Ketten unterschiedliche Sprachen sprechen (unterschiedliche technische Vokabulare) oder wenn der Vermögenswert zwischen einer Blockchain und einem Papier-Datenbank-System wechselt. Sie haben bewiesen, dass das Endergebnis immer dasselbe Bild ergibt, egal wie man die Reihenfolge der Operationen vertauscht.

B. Lebendigkeit: Der „Anti-Steckbleiben-Mechanismus“

Was es bedeutet: Das System friert niemals ein, selbst wenn einige Teilnehmer „Byzantinisch“ sind (ein schicker Begriff für bösartige oder defekte Knoten, die lügen, Nachrichten verzögern oder den Zugriff auf Vermögenswerte verweigern).
Die Analogie: Stellen Sie sich eine Gruppe von Menschen vor, die versuchen, einen schweren Kasten durch einen engen Flur zu reichen.
- Das Problem: Ein böser Akteur könnte den Kasten greifen und sich weigern, ihn loszulassen, wodurch er alle anderen blockiert.
- Die Lösung: Das System hat einen eingebauten „Timeout“ (wie eine federbelastete Falltür). Wenn jemand den Kasten zu lange hält, wird der Kasten automatisch aus seinen Händen gerissen und an die nächste Person weitergereicht.
- Der Beweis: Sie haben mathematisch bewiesen, dass selbst wenn bis zu einem Drittel der Menschen versucht, den Flur zu blockieren, der Kasten immer irgendwann durchkommen wird. Kein Vermögenswert wird jemals dauerhaft gesperrt sein.

3. Der „Zaubertrick“: Die Kombination der beiden

Normalerweise setzen Sicherheitsbeweise voraus, dass alle ehrlich sind. Lebendigkeitsbeweise setzen voraus, dass einige Leute schlecht sind.

Der Trick des Papers: Sie haben die beiden kombiniert. Sie haben gezeigt, dass der „Anti-Steckbleiben-Mechanismus“ (Lebendigkeit) so stark ist, dass er die „Ehrliche-Menschen“-Annahme erfordert, die für den „Unzerbrechlichen Spiegel“ (Sicherheit) notwendig ist.
Das Ergebnis: Man muss niemandem vertrauen. Selbst mit bösen Akteuren ist das System garantiert sowohl konsistent als auch in Bewegung.

4. Das Werkzeugset: „Lego-Steine“ für die Mathematik

Die Autoren haben dieses System nicht nur für eine bestimmte Blockchain gebaut. Sie haben 7 wiederverwendbare „Lego-Steine“ (genannt Locales in Isabelle/HOL) entwickelt.

Wie es funktioniert: Diese Steine sind generisch. Man kann sie an jedes beliebige System (eine Bank, eine Lieferkette, ein Spiel) anstecken, um sofort dieselben Sicherheits- und Lebendigkeitsgarantien zu erhalten.
Reale Tests: Sie haben die Steine nicht nur im Karton gelassen. Sie haben sie an drei sehr unterschiedlichen, realen Szenarien getestet, um ihre Funktionsweise zu beweisen:
1. Unterschiedliche Sprachen: Eine Kette, die nur „Einfrieren“ spricht, gegenüber einer Kette, die „Einfrieren“ und „Unfreezen“ spricht.
2. Unterschiedliche Welten: Eine Blockchain gegenüber einem komplexen Off-Chain-Rechtsdokument (DAML).
3. Die Konsens-Engine: Der spezifische Abstimmungsmechanismus, der entscheidet, wer als Nächstes an der Reihe ist.

5. Was dies NICHT ist

Um die Grenzen des Papers klarzustellen:

Es prüft nicht, ob ein spezifischer Richter tatsächlich das rechtliche Recht hat, einen Vermögenswert einzufrieren. Es prüft nur, dass wenn ein Einfrieren angeordnet wird, dies überall korrekt geschieht.
Es beweist nicht, dass der Computercode (Rust/Solidity) fehlerfrei ist; es beweist, dass das mathematische Modell des Systems fundiert ist.
Es behandelt nicht das Chaos eines Netzwerks, das während des Betriebs ständig neue Ketten hinzufügt oder entfernt (das ist zukünftige Arbeit).

Zusammenfassung

Dieses Paper ist ein mathematisches Zertifikat des Vertrauens. Es besagt: „Wir haben ein System gebaut, in dem regulatorische Regeln (wie das Einfrieren von Vermögenswerten) perfekt über verschiedene Welten hinweg durchgesetzt werden. Selbst wenn einige Teilnehmer versuchen, es zu brechen, verfügt das System über einen selbstkorrigierenden Mechanismus, der sicherstellt, dass die Regeln befolgt werden und das System niemals stecken bleibt.“

Dies haben sie erreicht, indem sie 3.215 Zeilen Code in einem Beweisassistenten (Isabelle/HOL) geschrieben haben, den ein Computer Schritt für Schritt überprüfte, um sicherzustellen, dass es keine logischen Lücken gibt.

Technisches Resümee: Sicherheit und Liveness von domänenübergreifender Zustandspräservation unter Byzantine Faults

1. Problemstellung

Die Arbeit adressiert die kritische Herausforderung, die Konsistenz regulatorischer Compliance-Zustände für tokenisierte Assets über heterogene Blockchain-Netzwerke und Off-Chain-Ledger hinweg zu garantieren. Ohne formale Garantien wird regulatorische Arbitrage strukturell möglich; beispielsweise muss eine Einfrieranordnung (Freeze Order), die in einer Jurisdiktion erlassen wurde, unmittelbar und deterministisch in allen verbundenen Domänen reflektiert werden.

Das Problem wird in zwei Dimensionen zerlegt:

Sicherheit (Safety): Sicherstellung, dass im Falle einer Synchronisation der resultierende Zustand über alle Domänen hinweg konsistent ist und eine strukturelle Erhaltung gewährleistet ist.
Liveness: Sicherstellung, dass der Synchronisationsprozess in einer dezentralen Umgebung, die Byzantine Nodes (böswillige Akteure) enthält, tatsächlich voranschreitet und Deadlocks oder Starvation vermeidet.

Vorherige Arbeiten haben nicht beide Eigenschaften gleichzeitig in einem einzigen Framework formal verifiziert, noch haben sie regulatorische spezifische Konsens-Eigenschaften (wie Prioritätsdeterminismus und Asset-Deadlock-Freiheit) mittels Isabelle/HOL verifiziert.

2. Methodik

Die Autoren verwenden einen mechanisierten Beweisansatz unter Verwendung von Isabelle/HOL. Die Entwicklung besteht aus 3.215 Zeilen Code über vier Theorie-Dateien, die ohne sorry oder oops (unbewiesene Annahmen) gebaut wurden.

2.1 System- und Bedrohungsmodelle

Systemmodell: Das System umfasst eine endliche Menge von Domänen (Chains/Ledger), die eine Zustandsautomatenstruktur teilen. Die Synchronisation wird als atomare Operation modelliert, die Verifizierung, Validierung, Sperrerwerb (Lock Acquisition), Zustandsaktualisierung und Sperrenfreigabe umfasst.
Bedrohungsmodell:
- Eigenschaft 1 (Safety): Nimmt initial ehrliche Knoten und zuverlässige Kanäle an.
- Eigenschaft 2 (Liveness): Lockert die Annahme ehrlicher Knoten auf, um bis zu $f < n/3$ Byzantine Nodes zuzulassen. Byzantine Nodes können Sperrenfreigaben zurückhalten oder bösartig agieren.
- Kombiniert: Eigenschaft 2 entlässt die Annahme ehrlicher Knoten aus Eigenschaft 1, was eine bedingungslose Garantie ergibt.

2.2 Modell der regulatorischen Zustandsübergänge

Das formale Modell basiert auf dem Regulatory Compliance Protocol (RCP) Framework, welches 31 Anforderungen aus 15 globalen Finanzbehörden systematisiert.

Zustände: Fünf regulatorische Zustände (ACTIVE, FROZEN, SEIZED, CONFISCATED, RESTRICTED).
Aktionen: Sieben regulatorische Aktionen (FREEZE, SEIZE, CONFISCATE, RESTRICT, UNFREEZE, UNRESTRICT, RELEASE).
Constraints: Das Modell erzwingt spezifische rechtliche Constraints, wie etwa den Ausschluss von "SEIZED → FROZEN" Übergängen (da Seizure eine stärkere rechtliche Einschränkung als Freezing ist) und die terminale Natur des CONFISCATED-Zustands.

2.3 Verifikationsinfrastruktur: Generische Locales

Die Kernmethodik beruht auf der Definition von sieben generischen, domänenunabhängigen Locales in Isabelle/HOL. Diese Locales dienen als wiederverwendbare Verifikationsinfrastruktur. Theorem, die innerhalb dieser Locales bewiesen werden, werden durch das Interpretationsmechanismus von Isabelle automatisch von jeder konkreten Domäne geerbt, die sie instanziiert.

Safety Locales (4):
1. state_machine: Definiert endliche Zustände, Aktionen und deterministische Übergänge.
2. state_preservation: Etabliert eine Natürlichkeitsbedingung, bei der die Synchronisation mit Zustandsübergängen kommutiert (Homomorphismus).
3. symmetric_state_preservation: Fügt inverse Abbildungen hinzu, um eine bidirektionale Roundtrip-Erhaltung zu garantieren.
4. multi_domain_preservation: Generalisiert die Konsistenz auf eine beliebige endliche Menge von Domänen ( $N$ -Domänen-Konsistenz) und stellt die Isolation pro Asset sicher.
Liveness Locales (3):
1. priority_system: Garantiert die deterministische Auswahl von Aktionen über injektive Prioritäten.
2. deadlock_free_locking: Stellt sicher, dass keine Ressource unendlich lange gesperrt bleibt, mittels Timeout-basierter erzwungener Freigabe.
3. fair_leader_system: Garantiert Starvation-Freiheit unter periodischer Planung eines ehrlichen Leaders.

3. Zentrale Beiträge

3.1 Mechanisierter Sicherheitsbeweis (Eigenschaft 1)

Die Arbeit erweitert das Merkle-Funktor-Muster (zuvor beschränkt auf unidirektionale Datenintegrität in einer einzelnen Domäne) auf ein domänenübergreifendes, bidirektionales und Multi-Domänen-Framework.

Bidirektionaler Roundtrip: Beweist, dass Zustandsübergänge in beiden Richtungen zwischen den Domänen getreu reflektiert werden.
N-Domänen-Konsistenz: Beweist, dass nach einer Synchronisation auf einer Domäne alle verbundenen Domänen denselben resultierenden Zustand erreichen.
Per-Asset-Isolation: Beweist, dass eine Synchronisation auf einem Asset den Zustand anderer Assets nicht beeinflusst.
Konkrete Instanziierungen: Die Autoren liefern konkrete Zeugen, um sicherzustellen, dass die Locales nicht vakuum-erfüllt sind:
- Escalation Instance: Eine heterogene-Aktions-Instanz, bei der eine Chain nur Eskalationsaktionen (FREEZE, SEIZE, etc.) unterstützt, während die andere den vollen Satz unterstützt, was die strukturelle Erhaltung über unterschiedliche Vokabularien hinweg beweist.
- Layer-Crossing Instance: Eine bidirektionale Brücke zwischen einem On-Chain reg_state Enum und einem Off-Chain DAML Permission Record, die Injektivität und Informationsverlustfreiheit beweist.

3.2 Mechanisierter Liveness-Beweis (Eigenschaft 2)

Dies ist die erste Verwendung von Isabelle/HOL allein zur Verifizierung der BFT-Konsens-Liveness in einem Blockchain-Kontext.

Determinismus: Konfliktierende regulatorische Aktionen werden über eine totale Ordnung von Prioritäts-Keys (Autoritätslevel, Zeitstempel, Schweregrad, Node-ID) aufgelöst.
Deadlock-Freiheit: Beweist, dass selbst wenn Byzantine Nodes Sperrenfreigaben zurückhalten, der Timeout-Mechanismus sicherstellt, dass die Sperre innerhalb einer gebundenen Zeit abläuft.
Starvation-Freiheit: Beweist, dass unter einer Fairness-Grenze (die garantiert, dass innerhalb von $k$ Epochen ein ehrlicher Leader vorhanden ist) alle ausstehenden Anfragen schließlich verarbeitet werden.

3.3 Assumption Discharge (Kombinierte Garantie)

Die Arbeit demonstriert ein Assume-Guarantee-Reasoning-Muster. Eigenschaft 2 entlässt die "Honest-Node"-Annahme, die für Eigenschaft 1 erforderlich war. Durch den Beweis, dass das System auch bei Byzantine Faults ( $f < n/3$ ) live und deterministisch bleibt, wird die bedingte Sicherheitsgarantie zu einer bedingungslosen Garantie erhoben: Die domänenübergreifende Zustandspräservation gilt auch in Gegenwart von Byzantine Nodes.

4. Ergebnisse und Artefakte

Beweis-Artefakte: Die Entwicklung umfasst acht konkrete Locale-Interpretationen (die alle sieben generischen Locales abdecken) neben einer parametrischen Multi-Domänen-Instanziierung.
Regulatorisches Modell: Das Modell deckt 31 regulatorische Anforderungen ab, die auf 5 Zustände und 7 Aktionen abgebildet sind.
Verfügbarkeit: Alle Artefakte sind öffentlich auf GitHub verfügbar und wurden dem Archive of Formal Proofs (AFP) zur Überprüfung eingereicht.
Design-Leitfaden: Die Beweise liefern spezifische Parameterbeschränkungen für die Implementierung (z. B. $n \ge 3f + 1$ , positive Timeouts, Fairness-Grenzen), die direkt in eine mathematische Design-Rationale für dezentrale Sequencer übersetzt werden können.

5. Signifikanz und Ansprüche

Die Arbeit beansprucht Signifikanz in drei primären Bereichen:

Neuheit in der formalen Verifikation: Es ist die erste Arbeit, die sowohl Sicherheit als auch Liveness simultan für domänenübergreifende regulatorische Zustandsübergänge formal verifiziert. Es ist zudem die erste Arbeit, die regulatorische spezifische Konsens-Eigenschaften (Prioritätsdeterminismus, regulatorische Asset-Deadlock-Freiheit) in einem Tool verifiziert.
Methodische Weiterentwicklung: Durch die Nutzung einer Hierarchie generischer Locales stellt die Arbeit eine wiederverwendbare Verifikationsinfrastruktur bereit, die domänenunabhängig ist. Dies ermöglicht es, dieselben Sicherheits- und Liveness-Beweise auf beliebige Domänen (z. B. DeFi, verteilte Datenbanken) anzuwenden, indem lediglich die Locales instanziiert werden.
Überbrückung von Theorie und Praxis: Die Arbeit geht über die abstrakte Konsens-Verifikation (wie Agreement/Validity) hinaus und adresset domänenspezifische regulatorische Constraints. Sie schlägt explizit die Brücke zwischen einem theoretischen Zustandsautomaten und einem regulatorischen Compliance-Modell und liefert einen "Design-Leitfaden" für Implementierungsparameter, die direkt aus den Beweisen abgeleitet sind.

Die Autoren weisen explizit auf Limitationen hin: Das Modell verifiziert keine chainspezifischen Charakteristika (Gas, Blockzeiten), beweist keine formale Verfeinerung (Refinement) auf Rust/Solidity-Code und setzt ein geschlossenes System voraus (dynamische Ankunft von Requests ist zukünftige Arbeit). Das aktuelle Framework etabliert die grundlegenden Locales und Instanzen, hat jedoch noch nicht die kategorientheoretischen Funktor-Gesetze (Identität und Komposition) formalisiert, welche für das Erreichen des vollen "Funktor"-Status reserviert sind.