[Paper] Belobog：Move 语言模糊测试框架用于真实世界的智能合约

Source: arXiv - 2512.02918v1

概览

本文提出了 Belobog，这是第一个能够为使用 Move 语言（如 Sui 和 Aptos 区块链）编写的智能合约自动生成有效交易的模糊测试框架。通过“类型感知”，Belobog 克服了 Move 严格的静态类型和资源模型，实现了以往现有模糊测试器无法完成的系统化安全测试。

关键贡献

• 类型感知的交易生成：从 Move 模块构建 类型图，并使用图遍历合成仅类型正确的交易。
• 混合符号执行引擎：结合具体执行与符号推理，以满足复杂的运行时检查（例如资源余额、能力检查）。
• 首个针对 Move 的模糊测试器：提供了一个实用的工具链，可自动发现真实世界 Move 合约中的漏洞。
• 实证验证：在 109 个开源 Move 项目上测试，达成 100 % 手动验证的关键漏洞检测率和 79 % 的主要漏洞检测率。
• 真实攻击复现：在未事先了解漏洞的情况下，成功复现了 Cetus 和 Nemo 攻击。

方法论

1. 静态分析与类型图构建

   • Belobog 解析 Move 源码，提取所有类型定义、结构体、资源和函数签名。
   • 它构建一个有向 类型图，节点代表具体类型，边表示类型之间的组合方式（例如 Vector<T> 节点指向其元素类型 T）。

2. 交易生成 / 变异

   • 从 图遍历（遵循 Move 线性资源规则的类型图路径）开始，Belobog 组装出保证类型检查通过的交易负载。
   • 对已有交易，Belobog 通过遵循替代图遍历来变异参数，确保每一次变异仍然是类型正确的。

3. 混合符号执行

   • 首先在轻量级 Move VM 上对生成的交易进行具体执行。
   • 当运行时守卫（如 assert!、能力检查）失败时，引擎记录分支条件并进行符号求解，以产生满足该守卫的新具体输入。
   • 这种 “具体 + 符号” 循环使 Belobog 能够探索纯随机模糊永远达不到的深层合约逻辑。

4. 漏洞检测

   • 框架监控常见的漏洞模式：重入、未授权资源转移、整数溢出/下溢，以及由 panic 或断言失败标记的逻辑错误。

结果与发现

作者得出结论：在 Move 中，类型感知的模糊测试结合混合符号执行是必不可少的，因为朴素模糊器会生成类型错误的交易，导致在任何合约逻辑运行之前就被拒绝。

实际意义

• 开发者工具：Belobog 可集成到 Move 项目的 CI 流水线中，自动在部署前暴露逻辑错误。
• 审计自动化：安全审计员可使用 Belobog 快速生成高置信度的测试套件，降低人工工作量并减少遗漏细微资源相关漏洞的风险。
• 区块链运营者：Sui/Aptos 节点运营者可在新提交的模块上运行 Belobog，提前捕获可利用的模式，提升网络安全性。
• 语言设计反馈：类型感知模糊测试的成功表明，即使是具有强静态保证的语言也受益于运行时测试，为 Move 类型系统或 VM 诊断的未来扩展提供参考。

局限性与未来工作

• 混合求解的可扩展性：随着合约复杂度提升，符号求解器可能出现性能瓶颈；作者建议采用增量求解和缓存作为后续改进方向。
• 非确定性原语的覆盖：Belobog 目前聚焦于确定性 VM 指令，如何处理随机性（如 random_u64）或外部预言机调用仍是未解挑战。
• 跨合约交互：框架将每个合约视为孤立单元；扩展至模糊多合约工作流（例如 DeFi 组合）是未来工作。
• 用户定义的不变式：引入开发者编写的规范（如 Move 的 spec 块）可引导模糊器针对更具体的安全属性进行测试。

Belobog 表明，即使是像 Move 这样以安全为中心的语言，也需要专门的、类型感知的动态测试。对于构建下一代区块链应用的开发者而言，将此类模糊测试工具纳入开发生命周期，可能决定是安全上线还是代价高昂的漏洞利用。

作者

• Wanxu Xia
• Ziqiao Kong
• Zhengwei Li
• Yi Lu
• Pan Li
• Liqun Yang
• Yang Liu
• Xiapu Luo
• Shaohua Li

论文信息

• arXiv ID: 2512.02918v1
• 分类: cs.CR, cs.PL, cs.SE
• 发布日期: 2025 年 12 月 2 日
• PDF: 下载 PDF