Paper 2024/1768
Push-Button Verification for BitVM Implementations
Abstract
Bitcoin, while being the most prominent blockchain with the largest market capitalization, suffers from scalability and throughput limitations that impede the development of ecosystem projects like Bitcoin Decentralized Finance (BTCFi). Recent advancements in BitVM propose a promising Layer 2 (L2) solution to enhance Bitcoin's scalability by enabling complex computations off-chain with on-chain verification. However, Bitcoin's constrained programming environment—characterized by its non-Turing-complete Script language lacking loops and recursion, and strict block size limits—makes developing complex applications labor-intensive, error-prone, and necessitates manual partitioning of scripts. Under this complex programming model, subtle mistakes could lead to irreversible damage in a trustless environment like Bitcoin. Ensuring the correctness and security of such programs becomes paramount. To address these challenges, we introduce the first formal verification tool for BitVM implementations. Our approach involves designing a register-based, higher-level domain-specific language (DSL) that abstracts away complex stack operations, allowing developers to reason about program correctness more effectively while preserving the semantics of the original Bitcoin Script. We present a formal computational model capturing the semantics of BitVM execution and Bitcoin Script, providing a foundation for rigorous verification. To efficiently handle large programs and complex constraints arising from unrolled computations that simulate loops, we summarize repetitive "loop-style" computations using loop invariant predicates in our DSL. We leverage a counterexample-guided inductive synthesis (CEGIS) procedure to lift low-level Bitcoin Script into our DSL, facilitating efficient verification without sacrificing accuracy. Evaluated on 98 benchmarks from BitVM's SNARK verifier, our tool successfully verifies 94% of cases within seconds, demonstrating its effectiveness in enhancing the security and reliability of BitVM.
Metadata
- Available format(s)
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- BitVMBitcoin ScriptFormal VerificationProgram Synthesis
- Contact author(s)
-
hanzhi @ ucsb edu
windocotber @ riema xyz
hongbowen @ ucsb edu
roblinus @ stanford edu
lukas @ zerosync org
manish @ alpenlabs io
hakan @ chainway xyz
domodata @ proton me
junrui @ ucsb edu
yanju @ ucsb edu
yufeng @ ucsb edu - History
- 2024-10-31: last of 2 revisions
- 2024-10-30: received
- See all versions
- Short URL
- https://ia.cr/2024/1768
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2024/1768, author = {Hanzhi Liu and Jingyu Ke and Hongbo Wen and Robin Linus and Lukas George and Manish Bista and Hakan Karakuş and Domo and Junrui Liu and Yanju Chen and Yu Feng}, title = {Push-Button Verification for {BitVM} Implementations}, howpublished = {Cryptology {ePrint} Archive, Paper 2024/1768}, year = {2024}, url = {https://eprint.iacr.org/2024/1768} }