Formale Verifikation von Blockchain-Konsensmechanismen mittels Event-B

Zusammenfassung

Diese Studie präsentiert einen formalen Verifikationsrahmen für Blockchain-Konsensmechanismen und Smart Contracts unter Verwendung der Event-B-Methode. Dieser Ansatz kombiniert Abstraktion von Repräsentation, invariantenbasierte Beweise und zeitliche Modellprüfung mit formellen Prüfungen von Sicherheit, Liveness und Widerstand gegen Double-Spending vor der Bereitstellung.

Zusammenfassung

Diese Studie entwickelt einen formal fundierten Verifikationsrahmen für Blockchain-Konsensmechanismen und Smart-Contract-Verhalten unter Verwendung von Event-B und der Rodin-Plattform. Im Gegensatz zu früheren Ansätzen, die hauptsächlich auf Simulation oder fallbasierter Validierung isolierter Verträge basieren, integriert diese Arbeit Finite State Machine (FSM)-Abstraktion, invariantengesteuerten Beweis, Verfeinerungsmodellierung und zeitliche Logikverifikation, um Proof of Work (PoW), Proof of Stake (PoS) und Mechanismen zur Verhinderung von Doppelausgaben zu analysieren. Solidity Smart Contracts werden in FSMs abstrahiert und als Event-B-Maschinen codiert, was die formale Spezifikation von Zustandsübergängen und Sicherheitsbeschränkungen ermöglicht. Sicherheitseigenschaften – einschließlich Transaktionseinzigartigkeit, Zustandskonsistenz, Durchsetzung von Zugriffskontrollen und invarianter Erhaltung des Hauptbuchs – werden durch automatisch generierte Beweisverpflichtungen in Rodin überprüft. Insgesamt wurden 312 Beweisverpflichtungen generiert, von denen 287 (92 %) automatisch erlassen und 25 interaktiv nachgewiesen wurden, was zu einer vollständigen invarianten Abdeckung führte. Liveness-Eigenschaften wurden in der Computation Tree Logic (CTL) spezifiziert und durch Modellprüfung validiert, wobei die Deadlock-Freiheit und die spätere Auswahl des Validators unter PoS-Bedingungen bestätigt wurden. Die Verhinderung von Doppelausgaben wurde formal mittels zustandskonsistenter Hauptbuchmodellierung durchgesetzt, bei dem Eindeutigkeitsbeschränkungen über alle erreichbaren Zustände hinweg nachgewiesen wurden. Die Konsenslogik auf Protokollebene für PoW und PoS wurde auf drei Abstraktionsebenen verfeinert, wodurch die Blockintegrität und die Korrektheit der Validatoren durch schrittweise Verfeinerung sichergestellt wurden. Die Ergebnisse zeigen, dass maschinell geprüfte Beweise überprüfbare Korrektheitsgarantien über simulationsbasierte Evaluation hinaus bieten und eine rigorose und reproduzierbare Verifikationspipeline etablieren, die die Korrektheitssicherheit und die protokollbasierte Robustheit in Blockchain-Systemen verbessert.

Einleitung

Die Blockchain-Technologie hat sich zu einem verteilten Hauptbuchparadigma entwickelt, das eine dezentrale Buchführung ohne Abhängigkeit von zentralen Behörden ermöglicht. Durch die Replikation von Hauptbuchzuständen über teilnehmende Knoten hinweg und das Erreichen einer Einigung durch Konsensmechanismen bieten Blockchain-Systeme Integrität, Transparenz und Manipulationsresistenz in offenen und gegnerischen Umgebungen. Wie von Yaga et ^al.1 beschrieben, kombiniert die Blockchain-Architektur kryptografische Primitive, verteilte Konsensprotokolle und Peer-to-Peer-Kommunikation, um sicherzustellen, dass validierte Transaktionen rechnerisch unpraktisch zu verändern sind. Kernkonsensmechanismen wie Proof of Work (PoW) und Proof of Stake (PoS) regulieren die Auswahl von Validatoren, die Blockvalidierung und die Synchronisation von Hauptbüchern. Darüber hinaus erweitern Smart Contracts die Blockchain-Fähigkeiten, indem sie programmierbare Logik einbetten, die autonom vordefinierte Regeln ausführt und dezentrale Anwendungen in Bereichen wie Finanzen, Gesundheitswesen und Governance ermöglicht. Da Blockchain-Technologien zunehmend in hochwertigen, sicherheitskritischen Umgebungen eingesetzt werden, ist die Korrektheit von Konsensmechanismen und Smart-Contract-Verhalten unerlässlich geworden, um die betriebliche^{Zuverlässigkeit} aufrechtzuerhalten.

Trotz ihrer dezentralen Natur bleiben Blockchain-Systeme anfällig für logische und protokollbezogene Schwachstellen. Doppelte-Ausgaben-Angriffe können auftreten, wenn Konsistenzbeschränkungen für das Hauptbuch nicht streng durchgesetzt werden. Schwächen auf Konsensebene, wie falsche Validator-Auswahllogik oder fehlerhafte Blockvalidierungsregeln, sowie Smart-Contract-Schwachstellen, einschließlich Re-Entrancy und unsachgemäßer Zugriffskontrolle, haben zu erheblichen finanziellen Verlusten auf bereitgestellten Plattformen geführt. Obwohl empirische Test- und Simulationsrahmen weit verbreitet zur Bewertung des Verhaltens von PoW- und PoS-Protokollen verwendet werden, liefern diese Ansätze nur illustrative Beobachtungen und keine umfassenden Korrektheitsgarantien. Simulationsbasierte Validierung kann die invariante Erhaltung über alle erreichbaren Zustände hinweg nicht nachweisen oder Sicherheits- und Lebenseigenschaften unter jedem Ausführungspfad gewährleisten. Diese Einschränkung unterstreicht die Notwendigkeit mathematisch fundierter Verifikationstechniken, die über die Beobachtungsanalyse hinaus rigoros über Blockchain-Systeme hinaus argumentieren können.

Formale Methoden bieten eine solche Grundlage, indem sie Systemspezifikation und -verifikation durch mathematische Logik ^3,4 ermöglichen. Ereignis-B erweitert dieses Paradigma durch schrittweise Verfeinerung, indem Systeme als abstrakte Zustandsautomaten dargestellt werden, in denen Systemzustände durch Invarianten eingeschränkt sind und Übergänge als bewachte Ereignisse^{modelliert werden 5}. Die Rodin-Plattform generiert automatisch Beweisverpflichtungen und unterstützt deren Ausführung, wodurch maschinell geprüfte Überprüfung der invarianten Erhaltung und der Zustandskonsistenz⁶ möglich ist. Klassische Spezifikationstechniken wie die B-Methode⁷ und Z⁸ zeigen, wie invariantenbasiertes Schließen und formale Verfeinerung die Systemkorrektheit über verschiedene Entwicklungsstufen hinweg sicherstellen können. Diese Methoden wurden häufig in missionskritischen und sicherheitskritischen Systemen eingesetzt, um die Korrektheit vor dem Einsatz^{sicherzustellen.} Weitere Erweiterungen wie UML-B und grafische Verfeinerungsrahmen demonstrieren zudem die Skalierbarkeit von verfeinerungsbasierter Modellierung für komplexe industrielle Systeme 14,15,16,17,18,19. Diese Entwicklungen zeigen, dass verfeinerungsgetriebene formale Modellierung die Systemkomplexität effektiv steuern kann, während starke Korrektheitsgarantien aufrechterhalten werden.

Formale Verifikationsansätze wurden auch für Blockchain-Systeme erforscht. SMT-basierte Vertragsverifikationstechniken überprüfen automatisch Behauptungen innerhalb von Solidity-Programmen und können Gegenbeispiele liefern, wenn logische Verstöße auftreten²⁰. Werkzeuge wie VERISOL verwenden endliche Zustandsabstraktionen für Smart-Contract-Verifikation², während Theorembeweis-Ansätze Verträge in formale Denkrahmen wie F*²¹ übersetzen. Darüber hinaus ermöglichen semantische Formalisierungen der Ethereum-Virtuellen Maschine eine rigorose Argumentation über Ausführungsemantik und Schwachstellenerkennung²². Ebenso wurden Theorembeweise-Umgebungen wie Coq eingesetzt, um konsensbezogene Sicherheitseigenschaften und transaktionale Korrektheit^{zu analysieren 23}. Obwohl diese Ansätze wertvolle Einblicke liefern, konzentrieren sie sich oft unabhängig voneinander auf Vertragsebene oder auf Konsens-Eigenschaften. Systemebene Ledger-Invarianten, Konsenszustandsübergänge und Smart-Contract-Verhalten werden selten in ein einheitliches, auf Verfeinerung basierendes Framework integriert, das die Rückverfolgbarkeit über Spezifikationsschichten und Verifikationsartefakte hinweg gewährleistet. Darüber hinaus legen viele bestehende Ansätze Wert auf Schwachstellenerkennung oder logische Behauptungsprüfung statt auf systematische invariante Erhaltung über mehrere Verfeinerungsstufen.

Die vorliegende Studie schließt diese methodologische Lücke, indem sie einen einheitlichen formalen Verifikationsrahmen vorschlägt, der die Finite State Machine (FSM)-Abstraktion von Solidity-Smart Contracts mit Event-B-Verfeinerungsmodellierung und maschinell geprüfter Proof Obligation Discharge innerhalb der Rodin-Plattform integriert. Anstatt Vertragsverifikation und Konsensmodellierung als getrennte Probleme zu behandeln, spezifiziert das vorgeschlagene Framework formal Protokoll-Level-Zustandsübergänge für PoW und PoS, Ledger-Integritätsbedingungen, Transaktions-Einzigartigkeitsbedingungen und Smart-Contract-Zustandsentwicklung innerhalb eines einzigen strukturierten Modells. Sicherheitseigenschaften – einschließlich invarianter Erhaltung, Transaktionseindeutigkeit, kontrollierter Zustandsübergänge und Konsistenz im Hauptbuch – werden als Ereignis-B-Invarianten ausgedrückt und durch automatisch generierte Beweisverpflichtungen überprüft. Temporale und ausführungsreihenfolgeabhängige Eigenschaften werden mittels Computation Tree Logic spezifiziert und durch Modellprüfung überprüft, um die Korrektheit über statische Invarianten hinaus sicherzustellen. Ein zentraler methodischer Beitrag liegt in der Etablierung expliziter Rückverfolgbarkeit über Abstraktionsschichten hinweg: Soliditätsfunktionen werden in FSM-Übergänge abstrahiert, FSM-Übergänge werden als Ereignis-B-Ereignisse kodiert, und Invarianten zusammen mit zeitlichen Spezifikationen sind direkt mit erfüllten Beweisverpflichtungen und Modellprüfungsergebnissen verknüpft. Diese strukturierte Abbildung stellt sicher, dass jede Korrektheitsbehauptung durch maschinell verifizierte Beweise gestützt wird und unterscheidet nachweisbasierte Garantien klar von simulationsbasierten Beobachtungen.

Der Umfang dieser Arbeit ist bewusst begrenzt, um Präzision und analytische Klarheit zu gewährleisten. Die Modellierung konzentriert sich auf Protokollebene-Zustandsübergänge für Konsensmechanismen, Ledger-Integritätsbeschränkungen, Transaktionseinzigartigkeit und Verhalten des Smart-Contract-Zustands. Netzwerkbezogene Aspekte wie Verzögerungen bei der Nachrichtenverbreitung, byzantinische Adversarialstrategien, Fork-Auflösungsmechanismen und detaillierte Gassemantik der Ethereum Virtual Machine liegen außerhalb der definierten Abstraktionsgrenze. Durch die explizite Definition dieser Modellierungsannahmen stellt der Rahmen sicher, dass Verifizierungsansprüche mit formal verifizierten Beweisen übereinstimmen. Der Rest dieses Artikels stellt die Abstraktionsmethodik, den Event-B-Modellierungs- und Verfeinerungsprozess, die Verfahren für invariante und zeitliche Verifikation sowie die daraus resultierenden Verifikationsergebnisse vor. Indem die Verifizierung von Blockchain-Protokollen und Smart-Contracts auf verfeinertebasierte formale Modellierung und maschinell geprüfte Beweise basiert, stärkt diese Studie die methodische Strenge und verbessert die Korrektheitssicherheit vor der Einführung für dezentrale Hauptbuchsysteme.

Protokoll

Studieninputs
In dieser Studie wurden zwei Solidity-Smart-Contracts als Verifikationseingaben verwendet. Ersteres war ein Simple DAO-ähnlicher Vertrag, der als Fallstudie für die Wiederaufnahme genutzt wurde. Der zweite war ein ausgedünnter Ledger-/State-Transition-Vertrag, der darauf ausgelegt war, Vertragsebenen-Einschränkungen gegen Doppelausgaben zu testen. Der ursprüngliche Solidity-Quellcode diente als Eingabe für die in diesem Protokoll definierten Abstraktions- und Verifikationsprozesse. Der allgemeine Transformationsprozess, der für solche Verträge verwendet wird, ist in Abbildung 1 dargestellt, die die schrittweise Transformation des Solidity-Quellcodes in die FSM-, Event-B- und SMV-Modelle während der Verifikation zeigt.

Modellierungsgrenze
Formale Modellierung konzentriert sich auf die Steuerungsflusslogik von Smart Contracts, einschließlich Funktionsein- und -austrittsverhaltens, interner Ausführung und Vertragszustandsübergängen. Die Sichtbarkeit der Funktionen (öffentlich, extern, intern und privat) wurde zusammen mit dem entsprechenden Call-Stack-Verhalten dargestellt, das für die Re-Entrancy-Analyse relevant ist. Die Arten abstrakter Übergänge (Anruf, Senden, Übertragung) wurden als Operationen für den Transfer von Ethern behandelt.

Vertragsebene-Invarianten wurden definiert, um die Transaktionseinzigartigkeit zu gewährleisten und Doppelausgaben innerhalb der Abstraktionsgrenze zu vermeiden. Um die Anforderungen an die Validierungsauswahl und Blockintegrität darzustellen, wurde die Protokoll-Logik-Abstraktionsschicht anhand der Protokollzustandsübergänge sowohl von Proof of Work als auch von Proof of Stake definiert.

Die Abstraktionsgrenze umfasste keine Netzwerkschicht-Elemente, einschließlich der Planung der zuzusendenden Nachrichten und Verzögerungen durch eine Vielzahl von Hops, Fork-Auflösung, Netzwerkgegner mit byzantinischen Strategien, Ethereum-Virtual-Machine-Semantik und Gas-Semantik, die von Netzwerkknoten kontrolliert wird, Ausnahmepropagation, asynchrone Ausführungen, komplexes Rückfallverhalten und Netzwerk-Finalität. Daher gelten die Ergebnisse der Bestimmung der doppelten Ausgaben nur für Vertragsebene-Invarianten und stellen keine netzwerkebene Vereinbarung über die Endgültigkeit dar.

Werkzeuge und Konfiguration
Die Rodin-Plattform wurde verwendet, um das Event-B-Modell (Version 3.7.0) zu modellieren, zu verfeinern, Beweisverpflichtungen zu erstellen und auszuführen, was es den PP-, ML-, SMT- und Atelier-B-Beweisern ermöglichte, Beweise automatisch und interaktiv auszuführen. nuXmv Version 2.0.0 wurde auf den generierten SMV-Modellen im vollständigen CTL-Explorationsmodus ausgeführt, um CTL-Modellprüfungen durchzuführen.

Alle Verifikationsausführungen wurden in einer kontrollierten Rechenumgebung unter Verwendung von Ubuntu 22.04 LTS, OpenJDK 11 und Python 3.10.12 durchgeführt. Web3 (7.6.0), NetworkX (3.4.2), Matplotlib (3.8.0), Graphviz (0.20.3), NumPy (1.26.4) und Pandas (2.2.2) wurden zur Implementierung von Simulations- und Visualisierungselementen verwendet. Dieses Design garantierte, dass formale Verifikations- und Simulationsergebnisse unter denselben Ausführungsbedingungen reproduziert werden konnten.

Transformations-Workflow
Dieser Verifikationsprozess hatte vier Phasen. Soliditätsverträge wurden zunächst in eine Finite State Machine (FSM-SC)-Darstellung übersetzt. Das FSM-SC-Modell wurde anschließend in Event-B codiert, mit klar festgelegten Invarianten und Verfeinerungsgraden. Die FSM-SC-Abstraktion wurde in nuXmv in ein SMV-Modell übersetzt. Die Verifikationsergebnisse wurden als Statistiken zur Nachweispflichtentlastung und CTL-Modellprüfung angegeben, und Gegenbeispiele wurden als Fälle bereitgestellt.

FSM-Bau
Jeder Vertrag wurde als endliche Zustandsmaschine abstrahiert, definiert als:

Wobei:
S = Menge von Zuständen
S₀ = Anfangszustand
T = Übergangsrelation
V = Sichtbarkeitskartierung
G = Schutzprädikate
A = Aktionen/Zustandsupdates.

Algorithmus 1: FSM-Konstruktion aus Solidity
Eingabe: Soliditäts-Quellcode
Ausgabe: FSM-SC

1) Den abstrakten Syntaxbaum des Solidity-Vertrags analysieren.
2) Erstelle den Anfangszustand S₀ aus der Konstruktordefinition.
3) Für jede Soliditätsfunktion f wird ein eigener Kontrollzustand S_f erstellt und die Sichtbarkeit V(f) ∈ {öffentlich, extern, intern, privat} erfasst.
4) Für jede Aussage innerhalb der Funktion f leiten Sie einen Übergang t ab, indem Sie Guard-Prädikate aus Regore/Assert-Bedingungen und Aktionen aus Zustandsvariablen-Updates extrahieren.
5) Übergang t zu T hinzufügen.
6) Erstelle explizite Übergangstypen für Ether-Transferoperationen (Aufruf, Senden, Übertragung), interne und externe Aufrufe, Delegiertenaufruf, Selbstzerstörung, tx.origin-Nutzung, bedingte Verzweigungen und Schleifenkonstruktionen.
7) FSM-SC = (S, S₀, T, V, G, A) zurückgeben.

Und jede Soliditätsfunktion ist mit einem anderen FSM-Steuerzustand verbunden. Für das Verständnis von Schwachstellen wurden schwachstellenrelevante Ausführungsflüsse, z. B. solche Flows mit externen Aufrufen gefolgt von Balance-Updates, explizit in geordnete Übergänge abstrahiert. Abbildung 2 zeigt ein Beispiel für ein FSM-SC-Diagramm für den SimpleDAO-ähnlichen Vertrag und zeigt, wie Eintrittszustände, externe Aufrufübergänge und Zustandsaktualisierungssequenzen während dieser Konstruktionsphase abstrahiert wurden.

Kodierung von FSM in Event-B
Der FSM-Übergang wurde als Event-B-Konstrukte dargestellt. Alle Übergänge entsprechen Ereignissen von Ereignis B, einschließlich bestimmter Wachen und Aktionen.

Algorithmus 2: FSM-zu-Event-B-Codierung
Eingang: FSM-SC
Ausgabe: Event-B-Maschine und Kontext

1) Definieren Sie STATE_SET und FUNKTION im Vertragskontext.
2) Variablen deklarieren, die den FSM-Kontrollzustand und den Vertragsniveau-Zustand repräsentieren.
3) Jeden FSM-Steuerzustand s ∈ S mit current_state ∈ STATE_SET darstellen.
4) Für jeden Übergang (s → s′, g, a) erstellen Sie ein Ereignis-B-Ereignis E_t mit:
5) WOBEI current_state = s ∧ g
6) DANN current_state := s′ ∥ anwenden(a)
7) Sichtbarkeitsbeschränkungen kodieren mit Guards, die von V(f) abgeleitet sind.
8) Invarianten inv1–inv9 definieren, um Sicherheits- und Konsistenzeigenschaften zu erfassen.
9) INITIALISIERUNG definieren, indem S₀ und Standardwerte zugewiesen werden.

Die Menge der Zustände, der aktuelle Zustand, die Funktionssichtbarkeit, der Aufrufstapel, der Transaktionszeitstempel, der Ether-Transferstatus, die Delegiertenaufruf-Flagge, die Selbstzerstörungsflagge und die Verifikationsbedingung sind einige der Variablen, die im Event-B-Modell erfasst werden. Die Invarianten (inv1-inv9) und die Aktionen der Initialisierungen (akt1-akt6) entsprechen denen der formalen Spezifikation. Abbildung 3 zeigt außerdem grafisch, wie die Schlüsselereignisse, die für Schwachstellen relevant sind, insbesondere re-entrancy-bezogene Übergänge, in der Event-B-Codierung verwaltet werden. Diese Abbildung erklärt, wie die strukturellen Muster des in Abbildung 2 gezeigten FSM-SC-Modells in verifizierbare Event-B-Ereignisse abgebildet werden.

Verfeinerungsstrategie
Es wurden zwei Stufen der Verfeinerung umgesetzt. Hochstufige Vertragskontrollfluss- und Kerninvarianten wurden auf abstrakter Ebene dargestellt. Das verfeinerte Niveau fügte vertragsspezifische Einschränkungen hinzu, darunter Call-Stack-Beschränkungen, Sichtbarkeitsbeschränkungen und Bedingungen zur Verhinderung von Wiedereintritt.

Algorithmus 3: Verfeinerung und Nachweis-Verpflichtung-Entlastung
Eingabe: Abstrakte Maschine und verfeinerte Maschine
Ausgabe: Erfüllte Beweisverpflichtungen und Statistiken

1) Erzeugung von Beweisverpflichtungen für die abstrakte Maschine in Rodin.
2) Ausführen aktivierter automatischer Prüfer und Aufzeichnen der Entladungsergebnisse.
3) Verfeinerungsnachweisverpflichtungen für die verfeinerte Maschine zu erstellen.
4) Automatische Beweise auf Verfeinerungsverpflichtungen anzuwenden.
5) Erfüllung der verbleibenden Verpflichtungen, wenn nötig, interaktiv.
6) Exportnachweisstatistiken und Statusberichte.

Die Beweisberichterstattung umfasste die Anzahl der Invarianten, Verfeinerungsstufen, erzeugte Beweispflichten, automatische Entladungsrate, interaktive Entladungsrate und endgültige Entladungsrate.

CTL-Eigenschaftsspezifikation und Modellprüfung
Die FSM-SC-Abstraktion wurde in ein SMV-Modell für zeitliche Verzweigungsverifikation in nuXmv übersetzt.

Algorithmus 4: FSM-zu-SMV- und CTL-Prüfung
Ausgabe: PASS/FAIL-Verifikationsergebnis und Gegenbeispiel-Traces (falls vorhanden)

1. Erfassen Sie die FSM-Steuerzustände als aufgezählten SMV-Variablenzustand.
2. Wandeln Sie FSM-Übergänge in bewachte Next(State)-Assignments um.
3. Halte Flaggen für schwachstellenrelevante Bedingungen, wie externe Anrufe und Balance-Updates.
4. CTL-Eigenschaften in nuXmv kodieren und Modellprüfungen durchführen.
5. Wenn eine Eigenschaft fehlschlägt, erzeugen Sie Gegenbeispiel-Spuren, die FSM-Übergangssequenzen repräsentieren.

CTL-Prüfungen umfassten Anforderungen an Wiedereinweisungsanordnungen, die Finalisierung von Zustandsupdates nach Übertragungsoperationen, die Begrenzung uneingeschränkter rekursiver Eingriffe in kritische Abschnitte und die Vermeidung von Deadlocks.

Sicherheitseigenschaften überprüft
Der Simple DAO-ähnliche Vertrag, der Re-Entrancy verhindert, wurde bestätigt, indem eine sichere Reihenfolge zwischen externen Aufrufen und Zustandsupdates über Invarianten und CTL-Constraints sichergestellt wurde. Wo erlaubt, überprüften diese Wächter Zugangskontrollbeschränkungen und stellten sicher, dass unautorisierte Übergänge durch Invarianten eingeschränkt wurden. Das reduzierte Hauptbuchmodell überprüfte die Invarianten der Transaktionseinzigartigkeit und der Konsistenz des Hauptbuchs auf Präventionsebene innerhalb des Vertrags.

Berichtete Ausgaben
Der Ergebnisbereich liefert Berichte zu FSM-Strukturmetriken, Event-B-Modellmetriken und Statistiken für den Nachweis der Verpflichtung und CTL-Verifikation. Die Ergebnisse des formalen Beweises und der CTL-Modellüberprüfung werden separat dargelegt, um den Nachweis von Korrektheitsgarantien durch Invarianten und den Nachweis einer Zeitverifikation mittels zeitlicher Verifikation zu unterscheiden.

Ergebnisse

Die Ergebnisse dieser Arbeit kombinieren die formalen Verifikationsprodukte Event-B und CTL-Modellprüfung mit ausführbaren Informationen aus der Blockchain-Simulation. Die Kombination dieser mehrschichtigen Ausgaben unterstützt die Validierung von Schlüsselverhalten in Smart Contracts, deren Konsenssystemen und deren Ledger-Solidness-Grenzen innerhalb der begrenzten Beispielbildung des Designs.

Umgebungseinrichtung und Abhängigkeitsverifikation

Diskussion

Formale und simulationsbasierte Verifikation zeigt, dass das mehrschichtige Verifikationssystem in der jeweiligen Forschung in der Lage war, das Verhalten von Smart Contracts, die Korrektheit des Konsensmechanismus und die Eigenschaft der Hauptbuchintegrität unter der wohldefinierten Abstraktionsgrenze zu überprüfen. Event-B bietet eine mathematisch fundierte Darstellung von Sicherheitseigenschaften, einem Zustandsfluss und einer Re-Entrancy-Präventionslogik in Bezug auf Invarianten und ...

Materialien

Liste der in diesem Artikel verwendeten Materialien

Name	Unternehmen	Katalognummer	Kommentare
Rodin-Plattform (v3.7.0)	Rodin Team / Eclipse Foundation	https://www.event-b.org/install.html	Event-B-Modellierung, Verfeinerung sowie Erzeugung und Entlastung von Beweisverpflichtungen
Ereignis-B-Methode	Universität Southampton / Rodin-Gemeinschaft	https://www.event-b.org/	Formales Modellierungsrahmen für invariante Spezifikation und Verfeinerung
nuXmv Model Checker (v2.0.0)	FBK (Fondazione Bruno Kessler)	https://nuxmv.fbk.eu/	Symbolische Modellprüfung der CTL-Eigenschaften
Graphviz (v0.20.3)	Graphviz-Team	https://graphviz.org/	FSM-Visualisierung und Graphenrendering
Python (v3.10.12)	Python Software Foundation	https://www.python.org/downloads	Simulations- und Ausführungsumgebung
Web3.py (v7.6.0)	Ethereum Foundation / Mitwirkende	https://web3py.readthedocs.io/	Blockchain-Interaktion und Transaktionssimulation
NetworkX (v3.4.2)	NetworkX-Entwickler	https://networkx.org/	Graphenmodellierung von Blockchain- und FSM-Strukturen
Matplotlib (v3.8.0)	Matplotlib-Entwicklungsteam	https://matplotlib.org/	Darstellung von Bergbauzeiten und Validatorverteilungen
NumPy (v1.26.4)	NumPy-Entwickler	https://numpy.org/	Numerische Berechnungen
Pandas (v2.2.2)	Pandas-Entwicklungsteam	https://pandas.pydata.org/	Datenanalyse und -verarbeitung
OpenJDK 11	Oracle / OpenJDK Community	https://openjdk.org/projects/jdk/11/	Erforderliche Laufzeit für die Rodin-Plattform
Ubuntu 22.04 LTS	Canonical Ltd.	https://ubuntu.com/download	Betriebssystem für alle Experimente
Solidität	Ethereum-Stiftung	https://soliditylang.org/	Smart-Contract-Quellsprache als Eingabe verwendet
nuXmv Eingabesprache (SMV)	FBK	https://nuxmv.fbk.eu/documentation.html	Zwischenmodellrepräsentation für CTL-Verifikation