Im Jahr 2026 stellt die zunehmende Code-Komplexität von Blockchain-Knoten und die Gefahr von KI-generierten Exploits die Sicherheit von Ethereum-Clients vor neue Herausforderungen. Formale Verifikation (FV) bietet mathematische Korrektheitsgarantien, kann aber die Trusted Computing Base (TCB) nicht vollständig eliminieren – sie kann sie jedoch signifikant verkleinern. Dieser Artikel fasst die wichtigsten Erkenntnisse aus aktuellen Forschungsarbeiten und Praxisbeispielen zusammen und zeigt, wie unterschiedliche Verifikationsansätze die TCB von Ethereum-Clients reduzieren.

Warum die Trusted Computing Base (TCB) entscheidend ist

Die TCB umfasst alle Komponenten, Spezifikationen, Werkzeuge und Annahmen, denen man vertraut, ohne dass sie formell bewiesen sind. Selbst wenn ein Implementierungsteil formal verifiziert ist, bleiben Grundannahmen wie die Korrektheit des Proof-Kernels, die physikalische Hardware, das Betriebssystem und das formale Modell der Befehlssatzarchitektur (ISA) unverifiziert. Deshalb kann FV die TCB nicht auf null reduzieren, aber sie kann den vertrauenswürdigen Umfang drastisch verringern.

Modularisierung: Pure- und Dirty-Module

Ein zentraler Schritt für die praktische Durchführbarkeit von Softwarebeweisen ist die Trennung in seiteneffektfreie (pure) und I/O-lastige (dirty) Module.

• Pure Module: Keine oder minimale Seiteneffekte, mathematisch gut beschreibbar. Beispiele: Kryptographie, SSZ (Simple Serialize), Fork-Choice-Regeln.
• Dirty Module: Viele Seiteneffekte und I/O-Interaktionen. Beispiele: Netzwerk-Stack, Peer-Management, Datenbank-Zugriffe.

Die reine Trennung ermöglicht es, reine Module relativ einfach zu verifizieren, während für dirty Module zunächst ein untrusted-by-design-Modell angenommen wird. Langfristig sollen auch dirty Module näher an die Netzwerkschicht verifiziert werden.

Vier Wege zur End-to-End-Formalen Verifikation

Option 1: Übersetzer-Tool (Aeneas) – Rust nach Lean4

Das Werkzeug Aeneas übersetzt Rust-Code über eine Zwischensprache namens Low-Level Borrow Calculus (LLBC) in reines Lambda-Kalkül, das von Theorembeweisern wie Lean4 oder Coq verarbeitet werden kann. Dadurch entfällt das manuelle Beweisen von Speichersicherheit, solange der Rust-Code keine unsafe -Blöcke oder Interior Mutability verwendet. Die wichtigsten Fakten:

• Publikationsjahr des Kern-Frameworks: 2022 (ICFP).
• TCB-Erweiterung: Der Übersetzer selbst und der Rust-Compiler bleiben Teil der TCB.
• Einschränkung: Nur ein Subset von Rust, das keine unsafe -Features nutzt, kann verarbeitet werden.

Option 2: Module direkt in Lean4 schreiben

Hier werden kritische Module in Lean4 implementiert; die Spezifikation und der Code sind identisch. Der Lean-zu-C-Extraktor ( leanc ) erzeugt C-Code, der anschließend mit einem herkömmlichen C-Compiler kompiliert wird. Vertraut bleiben:

• Der Extraktor leanc.
• Der C-Compiler.
• FFI-Bindings zwischen Lean-Code und dem Rest des Clients.

Option 3: Lean-maxxing – Client komplett in Lean4

Der gesamte Client wird in Lean4 geschrieben, wobei dirty Module über FFI in andere Sprachen eingebunden werden. Die TCB-Komponenten entsprechen denen von Option 2 (Extraktor, C-Compiler, Bindings). Der Vorteil liegt darin, dass die formalen Beweise tiefer in die Glue-Logik zwischen den Modulen reichen.

Option 4: Assembler-Verifikation – s2n-bignum (AWS)

Amazon hat die Open-Source-Bibliothek s2n-bignum entwickelt, die kryptografische Routinen direkt auf Assembler-Ebene in HOL Light gegen ein formales ISA-Modell verifiziert. Dadurch wird der Compiler vollständig aus der TCB entfernt. Wesentliche Ergebnisse:

• Durchsatzsteigerung bei RSA-Signaturen auf Graviton2-Prozessoren: 33 % bis 94 % gegenüber herkömmlichen Implementierungen (2024).
• Komplette mathematische Beweisbarkeit der Assembler-Implementierung.
• Eliminierung von Compiler-Fehlern als potenzielle Angriffsfläche.

Option 5: Verifizierter Compiler – Pancake / CakeML

Pancake ist eine imperative Sprache ohne dynamische Speicherallokation, deren Compiler auf dem verifizierten CakeML-Compiler aufbaut. Der Compiler garantiert semantische Äquivalenz vom AST bis zum Maschinencode. Kernpunkte:

• Unterstützte Ziel-Befehlssatzarchitekturen: 6 (x86-64, ARMv8, RISC-V u. a., 2024).
• Der gesamte Übersetzungspfad – von Pancake-Quellcode über CakeML bis zum Maschinencode – ist formal bewiesen.
• Der Proof-Kernel, die Hardware und das ISA-Modell bleiben jedoch Teil der TCB.

Praktische Bedeutung der Optionen

Der theoretische Gewinn einer schrumpfenden TCB wird in der industriellen Praxis durch konkrete Vorbilder untermauert. Bei AWS demonstrierte die Automated Reasoning Group mit der Open-Source-Bibliothek s2n-bignum, dass handgeschriebener und per HOL Light verifizierter Maschinencode nicht nur Speicherfehler ausschließt, sondern auf ARM-Graviton2-Prozessoren Leistungssteigerungen von bis zu 94 % bei kryptografischen Operationen ermöglicht (Amazon Science, 2024). Statt Compiler-Optimierungen zu vertrauen, verlagert dieser Assembler-Ansatz die Leistungsgarantie in mathematisch abgesicherte Algorithmen.

Auf Compilerebene schließen Projekte wie Pancake – entstanden im Umfeld des CakeML-Ökosystems – die Lücke zwischen systemnahem C-Stil und formaler Korrektheit (Tan et al., 2024). Indem Pancake restriktive Sprachannahmen trifft und den Übersetzungsschritt bis zur Zielarchitektur vollständig beweist, entfallen unvorhersehbare Compiler-Bugs als Fehlerquelle. Für Ethereum-Clients bedeutet dies: Je granularer mathematische Beweise an die Maschinenebene heranreichen, desto geringer wiegt das Risiko stiller Protokolldivergenzen durch Toolchain-Fehler.

Hybrid-Ansätze

Die vorgestellten Optionen können innerhalb desselben Clients kombiniert werden. Ein rein mathematischer Kern kann in Lean4 entwickelt werden, während rechenintensive Routinen über Aeneas oder Pancake eingebunden werden. Durch sorgfältige Schnittstellendefinitionen lässt sich die TCB weiter reduzieren, ohne die gesamte Code-Basis auf eine einzige Technologie zu beschränken.

Risiken und Gegenargumente

• Spezifikationsfehler (Specification Mismatch): FV garantiert nur die Übereinstimmung von Implementierung und Spezifikation. Fehlerhafte oder unvollständige Spezifikationen führen zu mathematisch korrekten, aber falschen Systemen.
• Entwicklungs- und Wartungsaufwand (Proof Maintenance): Ethereum-Protokoll-Upgrades sind häufig. Jede Code-Änderung erfordert das Aktualisieren interaktiver Beweisskripte, was spezialisierte Proof-Engineers benötigt und den Release-Zyklus verlangsamen kann.

Häufig gestellte Fragen

• Warum kann formale Verifikation die Trusted Computing Base niemals auf null reduzieren? Weil stets Grundannahmen unverifiziert bleiben müssen: die Korrektheit des mathematischen Beweisprüfers (Proof Kernel), die physikalische Hardware, das Betriebssystem sowie die formale Modellierung der Befehlssatzarchitektur (ISA).
• Was unterscheidet den Pancake-Ansatz von traditionellen C-Compilern wie Clang oder GCC? Herkömmliche Compiler können bei Optimierungen semantische Fehler oder unerwünschtes Verhalten einführen; der Pancake/CakeML-Compiler besitzt einen maschinell geprüften Beweis, dass der Maschinencode exakt dieselbe Semantik wie der Quellcode hat.

Fazit

Formale Verifikation stellt einen entscheidenden Hebel dar, um die Trusted Computing Base von Ethereum-Clients zu verkleinern. Durch die modulare Trennung in pure und dirty Komponenten, die Nutzung von Übersetzern wie Aeneas, die direkte Verifikation von Assembler-Code (s2n-bignum) oder den Einsatz verifizierter Compiler (Pancake/CakeML) kann die Menge an unbewiesenen Annahmen erheblich reduziert werden. Gleichzeitig zeigen Praxisbeispiele, dass diese Methoden nicht nur die Sicherheit erhöhen, sondern auch messbare Performance-Gewinne liefern – etwa bis zu 94 % höhere RSA-Durchsätze auf Graviton2. Dennoch bleiben Risiken bestehen, insbesondere bei fehlerhaften Spezifikationen und dem hohen Wartungsaufwand für Beweise. Ein ausgewogener, hybrider Ansatz, der die Stärken der einzelnen Optionen kombiniert und auf klar definierte Schnittstellen setzt, bietet derzeit das realistischste Modell, um Ethereum-Clients zukunftssicher und sicher zu gestalten.