Bitcoin Covenants entfesselt: Ein formales Modell für fortgeschrittene Smart Contracts

1. Einleitung

Bitcoins Unspent Transaction Output (UTXO)-Modell, obwohl elegant für gleichzeitige Währungsübertragungen, weist erhebliche Einschränkungen bei der Implementierung komplexer, zustandsbehafteter Smart Contracts auf, da es keinen gemeinsamen veränderlichen Zustand besitzt. Covenants stellen sich als entscheidendes sprachliches Primitive heraus, das vorgeschlagen wurde, um Bitcoin Script zu erweitern. Sie ermöglichen es einer Transaktion, Einschränkungen für die Scripts zukünftiger einlösender Transaktionen vorzugeben. Diese Arbeit adressiert die Lücke in formalen, abstrakten Modellen für Covenants, die seit ihrer Entstehung um 2013 hauptsächlich aus einer Low-Level, implementierungsfokussierten Perspektive beschrieben wurden. Durch die Bereitstellung einer formalen Grundlage zielt die Arbeit darauf ab, die Argumentation über Vertragseigenschaften zu vereinfachen, die Spezifikation fortgeschrittener Anwendungsfälle jenseits der aktuellen Bitcoin-Fähigkeiten zu ermöglichen und das Design höherer Programmierabstraktionen zu erleichtern.

2. Das reine Bitcoin-Modell

Die Arbeit adaptiert eine Formalisierung des Kern-Bitcoin-Transaktionsmodells. Im UTXO-Modell wird der Blockchain-Zustand durch eine Menge unverbrauchter Transaktionsausgaben definiert. Jede Ausgabe enthält einen Wert (Bitcoin-Betrag) und ein scriptPubKey (Sperrscript), das die Bedingungen für die Ausgabe festlegt. Eine ausgebende Transaktion stellt ein scriptSig (Entsperrscript) bereit und referenziert den UTXO, den sie verbrauchen möchte. Die Validierung umfasst die Ausführung der verketteten Scripts. Entscheidend ist, dass das Standard-Bitcoin Script limitiert ist: Es kann die Struktur der ausgebenden Transaktion über Signaturverifizierung und grundlegende Arithmetik/Logik hinaus nicht introspektieren oder einschränken, was die Erstellung von Verträgen verhindert, die mehrstufige Protokolle erzwingen.

3. Formales Modell von Covenants

Der Kernbeitrag ist ein formales Modell, das vorgeschlagene Covenant-Opcodes (wie OP_CHECKTEMPLATEVERIFY) abstrahiert.

4. Spezifikation komplexer Bitcoin-Verträge

Das formale Modell wird angewendet, um Verträge zu spezifizieren, die in reinem Bitcoin derzeit nicht ausdrückbar oder umständlich sind.

5. Hochsprachliche Primitiven

Die Arbeit diskutiert, wie Covenants als Kompilierungsziel für höhere Vertragssprachen dienen können. Primitiven wie "nach Zeit T auszahlen", "nur ausgeben, wenn Gegenpartei signiert" oder "Zustand von A nach B überführen" können direkt auf spezifische Covenant-Einschränkungen abgebildet werden, was das Abstraktionsniveau für Bitcoin-Vertragsentwickler erhöht.

6. Kernaussage & Analystenperspektive

Kernaussage: Bartoletti et al. schlagen nicht nur einen weiteren Covenant-Opcode vor; sie liefern die fehlende formale Theorie, die einen cleveren Hack in ein legitimes, analysierbares Programmierparadigma für Bitcoin verwandelt. Dies ist der Schlüssel, der die systematische Entwicklung komplexer, sicherer Verträge auf UTXO-Blockchains ermöglicht und über Ad-hoc-Scripting hinausgeht.

Logischer Ablauf: Das Argument ist überzeugend einfach: 1) Bitcoins UTXO-Modell fehlt ein Zustand, was Verträge einschränkt. 2) Covenants wurden als Lösung vorgeschlagen, sind aber formal schlecht verstanden. 3) Daher bauen wir ein formales Modell. 4) Mit diesem Modell demonstrieren wir, dass es wertvolle, komplexe Anwendungsfälle (Vaults, Kanäle, DeFi) ausdrücken kann. 5) Diese Formalisierung ermöglicht dann natürlich das Design höherer Sprachen. Es ist eine klassische "Theorie ermöglicht Praxis"-Pipeline, präzise ausgeführt.

Stärken & Schwächen: Die größte Stärke ist die Überbrückung der Lücke zwischen Kryptografie/PL-Theorie und Bitcoin-Engineering – eine Lücke, die zu kostspieligen Fehlern in Ethereums kontobasiertem Modell geführt hat. Die formale Semantik ermöglicht Eigenschaftsverifikation, ein großer Gewinn. Die implizit eingeräumte Schwäche ist die politische Ökonomie von Bitcoin. Wie die Arbeit feststellt, macht Bitcoins "extrem vorsichtiger Ansatz" die Bereitstellung neuer Opcodes wie Covenants zu einer herkulischen Aufgabe, unabhängig von ihrer formalen Eleganz. Der Erfolg von Layer-2-Lösungen wie Lightning ohne native Covenants wirft auch Fragen nach Notwendigkeit versus Nützlichkeit auf. Darüber hinaus beruht die Sicherheit des Modells auf der Annahme, dass die eingeschränkten Felder (wie Skripthashes) ausreichend sind; unvorhergesehene Interaktionseffekte mit anderen Opcodes könnten bestehen bleiben.

Umsetzbare Erkenntnisse: Für Forscher ist diese Arbeit ein Bauplan: Verwenden Sie formale Methoden, um Blockchain-Upgrades zu entrisiken und zu klären. Für Entwickler: Beginnen Sie jetzt mit dem Design von Vertrags-Frameworks unter der Annahme, dass Covenants existieren werden (wie bei Liquid oder Stacks zu sehen). Für Bitcoin-Protokollentwickler bietet die Arbeit die rigorose Grundlage, die benötigt wird, um für BIP 119 (OP_CTV) oder ähnliche Vorschläge zu argumentieren – sie verwandelt eine Feature-Anfrage in eine technische Spezifikation. Die wichtigste Erkenntnis: Die Zukunft von Bitcoin Smart Contracts besteht nicht darin, Ethereum nachzuahmen, sondern darin, das einzigartige UTXO+Covenants-Paradigma zu nutzen, um eine neue, potenziell sicherere und skalierbarere Klasse dezentraler Anwendungen zu schaffen.

7. Technische Details & Formalisierung

Das formale Modell definiert Transaktionen, Scripts und Validierung kontextuell. Ein wichtiges technisches Detail ist die Darstellung der Covenant-Einschränkung. Sei $\texttt{tx}$ eine Transaktion. Ein Covenant kann als Funktion gesehen werden:

$\text{Covenant}_{\text{cond}} : \texttt{tx}_{\text{current}} \times \texttt{tx}_{\text{next}} \times \sigma \rightarrow \{\text{True}, \text{False}\}$

wobei $\sigma$ den Validierungskontext (Blockhöhe, etc.) repräsentiert. Das Prädikat $\text{cond}$ kann eine Konjunktion von Prüfungen auf $\texttt{tx}_{\text{next}}$-Feldern sein:

$\text{cond} \equiv (\texttt{hashOutputs}(\texttt{tx}_{\text{next}}) = H) \land (\texttt{nLockTime}(\texttt{tx}_{\text{next}}) > T) \land ...$

Dies entspricht Vorschlägen wie OP_CHECKTEMPLATEVERIFY, das einen Hash spezifizierter Teile der ausgebenden Transaktion auf den Stack legt, um ihn zu vergleichen. Die rekursive Eigenschaft wird formalisiert, indem sichergestellt wird, dass eine Ausgabe von $\texttt{tx}_{\text{next}}$ ein Script $S'$ enthält, das selbst einen Covenant $\text{Covenant}_{\text{cond}'}$ erzwingt.

8. Analyseframework & Beispielsfall

Beispiel: Ein einfacher Vault-Vertrag
Ziel: Einen UTXO erstellen, der auf zwei Arten ausgegeben werden kann: 1) Sofort, aber nur an eine spezifische "Cold Storage"-Adresse. 2) An jede Adresse, aber erst nach einer 30-tägigen Verzögerung (ermöglicht Stornierung bei Diebstahl).
Framework-Anwendung mit dem formalen Modell:
1. Initiales Sperrscript (scriptPubKey): Enthält eine Covenant-Bedingung $C_1$.
2. Covenant $C_1(T_{vault}, T_{spend})$: Muss zu True ausgewertet werden. Es prüft:
    a) Pfad A (Sofort): $\texttt{hashOutputs}(T_{spend}) = H_{cold}$ // Ausgabe muss auf vorab festgelegte Cold-Storage-Adresse hashen.
    b) Pfad B (Verzögert): $\texttt{nLockTime}(T_{spend}) \geq \text{currentBlock} + 4320$ (30 Tage in Blöcken) UND $\texttt{hashOutputs}(T_{spend})$ kann beliebig sein.
3. Validierung: Wenn der Vault-UTXO mit $T_{spend}$ ausgegeben wird, führt der Bitcoin-Knoten das Script aus. Es erfordert eine Signatur des Vault-Eigentümers und verifiziert, dass $C_1$ für das Transaktionspaar gilt.
Dieses Beispiel zeigt, wie das Prädikat $C(T_x, T_{next})$ des formalen Modells mit konkreten Prüfungen der Felder der nächsten Transaktion instanziiert wird, was eine Sicherheitseigenschaft (Diebstahlrückgewinnung) ermöglicht, die im Basis-Bitcoin unmöglich ist.

9. Zukünftige Anwendungen & Richtungen

Die Formalisierung eröffnet mehrere zukünftige Wege:

• Verifizierte Compiler: Bau von Compilern von höheren Sprachen (wie Simplicity oder Miniscript-Erweiterungen) zu covenant-eingebettetem Bitcoin Script, mit formalen Korrektheitsbeweisen.
• Cross-Chain Covenants: Erforschung von Covenants, die Ausgaben von Ereignissen anderer Blockchains oder Orakeln abhängig machen, unter Verwendung kryptografischer Nachweise wie SPVs, wie durch frühere Arbeiten zu "Bridges" und aktuelle Forschung zu Rollups angedeutet.
• Datenschutzbewahrende Covenants: Integration von Covenant-Prüfungen mit Zero-Knowledge-Beweisen (z.B. unter Verwendung von Taproot/Schnorr-Signaturen), um die Vertragslogik zu verbergen, während sie dennoch durchgesetzt wird, eine Richtung, die in Projekten wie Ark erforscht wird.
• Formale Sicherheitsanalyse: Nutzung des Modells zur systematischen Analyse der Sicherheit vorgeschlagener Covenant-Konstruktionen gegen wirtschaftliche und kryptografische Angriffe, ähnlich der Arbeit, die von der IEEE Symposium on Security and Privacy-Community zu Ethereums Smart Contracts geleistet wurde.
• Layer-2-Protokollvereinfachung: Neugestaltung von Protokollen wie dem Lightning Network oder Sidechains (Liquid), um sie durch Nutzung nativer Covenants effizienter und vertrauensminimierter zu machen und den Bedarf an komplexen Watchtowers oder Föderationen zu reduzieren.

10. Referenzen

1. M. Bartoletti, S. Lande, R. Zunino. Bitcoin covenants unchained. arXiv:2006.03918v2 [cs.PL]. 2020.
2. S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. 2008.
3. J. Poon, T. Dryja. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. 2016.
4. M. Moser, I. Eyal, E. G. Sirer. Bitcoin Covenants. Financial Cryptography 2016 Workshops.
5. Bitcoin Improvement Proposal 119 (BIP 119). OP_CHECKTEMPLATEVERIFY.
6. G. Wood. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum Yellow Paper. 2014.
7. A. Miller, et al. Hashed Timelock Contracts (HTLCs). 2017.
8. R. O'Connor. Simplicity: A New Language for Blockchains. Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security.
9. Blockstream. Liquid Network. https://blockstream.com/liquid/
10. IEEE Symposium on Security and Privacy. Multiple papers on smart contract security analysis. Various years.