Paper 2024/1768

Push-Button Verification for BitVM Implementations

Hanzhi Liu, Nubit, University of California, Santa Barbara
Jingyu Ke, Nubit
Hongbo Wen, Nubit, University of California, Santa Barbara
Robin Linus, ZeroSync, Stanford University
Lukas George, ZeroSync
Manish Bista, Alpen Labs
Hakan Karakuş, Chainway Labs
Domo, Layer 1 Foundation
Junrui Liu, University of California, Santa Barbara
Yanju Chen, University of California, Santa Barbara
Yu Feng, Nubit, University of California, Santa Barbara
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)
PDF
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
Creative Commons Attribution
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}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.