在BTC生态中最重要的两个基建就是babylon 和BitVM。近期BitVM又迎来好消息。
Nubit团队 @nubit_org 带来了形式化验证工具BitGuard，它可以让普通开发者几乎自动化下完成代码的验证，进而确保BitVM安全性。
大名鼎鼎的BitVM已经在我多篇文章中出镜过，它是由Robert提出的比特币扩展框架，允许在链下执行复杂的计算，而链上验证其正确性。让只有简单编程脚本功能的比特币网络，能够支持图灵完备的智能合约来扩展比特币的功能。BitVM能带给比特币生态项目（主要是layer2）带来的最大的功能之一就是能够比特币主网进行Roll-up验证，是真正意义的BTC安全验证。不像以太坊，在原生BTC网络验证的实现非常困难（这段时间陆续技术上有所突破），所以BitVM成为稀缺品。很多的比特币layer2会使用BitVM作为核心组建。
但是，在BitVM开发的难度要比ETH上大很多，这个难度由BTC网络带来的，来自非图灵完备的脚本语言缺乏循环和递归，以及严格的区块大小限制。这不仅造成了开发者需要更大的工作量，也增加开发应用的风险。即使是在图灵完备的以太坊，依然会经常出现漏洞攻击的现象。那么在开发难度更大的比特币网络，这个问题就应该尤为重视。因为很多资金密集型的应用例如dex、借贷等，一个小错误都可能被黑客抓住，进而造成巨大的经济甚至影响到整个生态。
为了解决这个问题，由Nubit 的YuFeng教授牵头设计针对 BitVM 的形式化验证工具 BitGuard。它能够减少开发者对代码测试和人工检查的依赖，使得代码的行为可以被严格证明。科普一下，形式化验证工具是一类使用数学技术和算法来验证软件和硬件系统设计正确性的工具。这些工具通过严格的数学方法，确保系统行为与其正式规范或属性一致，从而帮助开发者识别潜在的设计缺陷和错误。
BitGuard IR 的设计原理是将低级的、基于栈的比特币脚本语言提升到更高级别的、基于寄存器的表示形式。使用寄存器来存储和操作数据。这使得程序更易于理解和验证，因为数据流更加清晰。
BitGuard 的整体验证算法可以分为三步：
1.分解 (Decomposition): BitGuard 首先将整个程序分解成较小的代码片段。这个分解过程可以结合开发者的语义背景知识和自动语法模式匹配来实现。
2.验证提升 (Verified Lifting): BitGuard 使用程序合成技术，将每个分解后的代码片段重写成对应的 BitGuard 中间表示 (IR) 代码片段。 BitGuard IR 是一种基于寄存器的 DSL，旨在抽象复杂的堆栈操作，同时保留原始比特币脚本的语义。 这个过程会确保生成的 BitGuard IR 代码片段在语义上等价于原始的比特币脚本代码片段。
3.验证 (Verification): 用户使用 BitGuard IR 的验证语言构造（例如 assume 和 assert）以 Hoare 逻辑的风格提供规范和注释，例如前置条件、后置条件和循环不变式。 BitGuard 会推断复杂循环的不变量，并对代码进行重写以提高验证效率。 最后，BitGuard 使用符号执行将 BitGuard IR 程序转换为约束，并使用后端约束求解器 (例如 Bitwuzla) 对这些约束进行推理。
BitGuard的优点是显而易见的，包括
●简化推理：通过抽象化复杂的栈操作，BitGuard IR 使得对程序行为的推理更加容易。基于寄存器的操作比基于栈的操作更易于理解和分析。
●提高验证效率：BitGuard IR 中的循环不变式谓词可以总结重复的计算，从而减少生成的 SMT 公式的复杂性。这使得验证过程更加高效。
●保留语义：混合执行模式确保了即使在无法合成 DSL 代码的情况下，BitGuard IR 仍然可以保留原始比特币脚本的完整语义。
总的来说，BitGuard设计了一种更高层次的寄存器型领域特定语言（DSL），抽象掉复杂的栈操作，简化程序推理过程，同时保留原始比特币脚本的语义。BitGuard还利用循环不变式来高效处理循环计算，并使用反例引导归纳综合（CEGIS）方法将低级比特币脚本提升至DSL，从而进行更便捷的验证。评估结果表明，BitGuard在98个BitVM SNARK验证器基准测试中成功验证了94%，证明了其有效性和实用性。
以上的工作发表由 Nubit YuFeng教授牵头，与 BitVM 创始人 Robin 的 @ZeroSync_，还有@AlpenLabs, @citrea_xyz，BRC20 创始人 Domo 所在的 @L1Fxyz 共同完成。论文发表在https://eprint.iacr.org/2024/1768
免责声明：本文章仅代表作者个人观点，不代表本平台的立场和观点。本文章仅供信息分享，不构成对任何人的任何投资建议。用户与作者之间的任何争议，与本平台无关。如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到support@aicoin.com，本平台相关工作人员将会进行核查。
