The two most important infrastructures in the BTC ecosystem are Babylon and BitVM. Recently, BitVM has received good news.
The Nubit team @nubit_org has introduced a formal verification tool called BitGuard, which allows ordinary developers to automate the code verification process, thereby ensuring the security of BitVM.
The renowned BitVM has appeared in several of my articles; it is a Bitcoin extension framework proposed by Robert that allows complex computations to be executed off-chain while verifying their correctness on-chain. This enables the Bitcoin network, which only has simple programming script capabilities, to support Turing-complete smart contracts, thereby expanding Bitcoin's functionality. One of the greatest functionalities that BitVM can bring to Bitcoin ecosystem projects (mainly layer 2) is the ability to perform Roll-up verification on the Bitcoin mainnet, representing true BTC security verification. Unlike Ethereum, implementing verification on the native BTC network is very challenging (there have been technical breakthroughs during this period), making BitVM a scarce resource. Many Bitcoin layer 2 projects will use BitVM as a core component.
However, the difficulty of developing on BitVM is significantly higher than on ETH, a challenge posed by the BTC network due to the non-Turing complete scripting language lacking loops and recursion, as well as strict block size limitations. This not only results in a greater workload for developers but also increases the risks of developing applications. Even on the Turing-complete Ethereum, vulnerabilities and attacks frequently occur. Therefore, this issue should be particularly emphasized in the more challenging Bitcoin network. For many capital-intensive applications such as DEXs and lending, even a small error could be exploited by hackers, leading to significant economic losses and potentially impacting the entire ecosystem.
To address this issue, Professor YuFeng from Nubit has led the design of the formal verification tool BitGuard for BitVM. It reduces developers' reliance on code testing and manual checks, allowing the behavior of the code to be rigorously proven. To clarify, formal verification tools are a class of tools that use mathematical techniques and algorithms to verify the correctness of software and hardware system designs. These tools ensure that the system's behavior aligns with its formal specifications or properties through strict mathematical methods, helping developers identify potential design flaws and errors.
The design principle of BitGuard IR is to elevate the low-level, stack-based Bitcoin scripting language to a higher-level, register-based representation. It uses registers to store and manipulate data, making programs easier to understand and verify due to clearer data flow.
The overall verification algorithm of BitGuard can be divided into three steps:
Decomposition: BitGuard first decomposes the entire program into smaller code segments. This decomposition process can be achieved by combining the developer's semantic background knowledge with automatic syntax pattern matching.
Verified Lifting: BitGuard uses program synthesis techniques to rewrite each decomposed code segment into the corresponding BitGuard intermediate representation (IR) code segment. BitGuard IR is a register-based DSL designed to abstract complex stack operations while preserving the semantics of the original Bitcoin script. This process ensures that the generated BitGuard IR code segments are semantically equivalent to the original Bitcoin script code segments.
Verification: Users construct specifications and annotations using the verification language of BitGuard IR (e.g., assume and assert) in a style similar to Hoare logic, such as preconditions, postconditions, and loop invariants. BitGuard infers the invariants of complex loops and rewrites the code to improve verification efficiency. Finally, BitGuard uses symbolic execution to convert the BitGuard IR program into constraints and employs a backend constraint solver (e.g., Bitwuzla) to reason about these constraints.
The advantages of BitGuard are evident, including:
● Simplified reasoning: By abstracting complex stack operations, BitGuard IR makes reasoning about program behavior easier. Register-based operations are more understandable and analyzable than stack-based operations.
● Improved verification efficiency: The loop invariant predicates in BitGuard IR can summarize repetitive computations, thereby reducing the complexity of the generated SMT formulas. This makes the verification process more efficient.
● Preserved semantics: The mixed execution model ensures that even when DSL code cannot be synthesized, BitGuard IR still retains the full semantics of the original Bitcoin script.
In summary, BitGuard has designed a higher-level register-based domain-specific language (DSL) that abstracts complex stack operations, simplifies the program reasoning process, while preserving the semantics of the original Bitcoin script. BitGuard also utilizes loop invariants to efficiently handle loop computations and employs counterexample-guided inductive synthesis (CEGIS) methods to elevate low-level Bitcoin scripts to DSL for more convenient verification. Evaluation results indicate that BitGuard successfully verified 94% of 98 BitVM SNARK verifier benchmark tests, demonstrating its effectiveness and practicality.
The above work was published under the leadership of Professor YuFeng from Nubit, in collaboration with Robin, the founder of BitVM, @ZeroSync, as well as @AlpenLabs, @citreaxyz, and Domo from BRC20 at @L1Fxyz. The paper is published at https://eprint.iacr.org/2024/1768
免责声明：本文章仅代表作者个人观点，不代表本平台的立场和观点。本文章仅供信息分享，不构成对任何人的任何投资建议。用户与作者之间的任何争议，与本平台无关。如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到support@aicoin.com，本平台相关工作人员将会进行核查。
