Push-Button Verification for BitVM Implementations

Hanzhi Liu; Jingyu Ke; Hongbo Wen; Robin Linus; Lukas George; Manish Bista; Hakan Karakuş; Domo; Junrui Liu; Yanju Chen; Yu Feng

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: BitVM Bitcoin Script Formal Verification Program 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: revised; 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}
}