caliperforge/invariant-atlas

# Exploit→Invariant Atlas (v0.1) 一个跨 VM、防守方侧、部署前的 CI 基准测试：对于每个历史漏洞利用， 包含一个可运行的不变性属性，以及一个同源孪生样本，该属性在 CI 运行的预漏洞代码上*原本会*捕获该类 bug。 **状态：** v0.1 已发布 —— 全部六个案例涵盖 Cairo、Move、Solana 和 EVM，每个案例均断言了两条 CI 分支（正常通过 / 注入报错）。 ## 相关工作与定位 ## 本 Atlas 不作声明的方面 - **不是“完整”的基准测试。** Trace2Inv 的 27 个 EVM 案例是由一个经过同行评审的学术团队完成的；v0.1 发布了跨 4 个 VM 的 6-8 个案例。客观的声明是*首个防守方侧的跨 VM 基准测试*，而非*详尽无遗*。 - **不是“我们捕获了这些漏洞利用”。** 本 Atlas 展示了存在可运行的不变性属性，这些属性*原本会*在预漏洞代码上触发失败。协议本身并没有运行它们；CaliperForge 并没有在线发现这些漏洞利用。 - **不是形式化验证。** 部署前的属性测试是覆盖率引导的，而非详尽无遗的。本 Atlas 的声明是“该属性在 CI 运行中捕获了这一特定历史漏洞利用的失败类别”，而不是“该属性证明了该 bug 类的不存在”。 ## 案例集 (v0.1) 案例顺序将非 EVM 分支放在首位，因此其直观信号是“由非 EVM 主导的基准测试，并带有连接到经典体系的 EVM 桥接”，而不是“带有非 EVM 附录的 EVM 基准测试”。 | # | VM | 漏洞利用 | 日期 | 损失 | 不变性类别 | 状态 | |---|---|---|---|---|---|---| | **C1** | Cairo / Starknet | [zkLend](cases/01-cairo-zklend/) | 2025年2月 | ~$10M | 累加器单调性 + 往返守恒 + 精度损失界限 | **已发布 (模板设定者)** | | **C2** | Move / Sui | [Cetus](cases/02-move-cetus/) | 2025年5月 | ~$223M | 溢出安全 + 流动性↔token 守恒 | **已发布** | | **C3** | Solana | [Cashio](cases/03-solana-cashio/) | 2022年3月 | ~$50M | 账户 / 权限验证 | **已发布** | | **C4** | Solana | [Mango Markets](cases/04-solana-mango/) | 2022年10月 | ~$117M | oracle 新鲜度 + 价格合理性界限 | **已发布** | | **C5** | Solana | [Loopscale](cases/05-solana-loopscale/) | 2025年4月 | ~$5.8M | 抵押品估值 oracle 界限 | **已发布** | | **C6** | EVM (桥接) | [Trace2Inv-set，访问控制类](cases/06-evm-access-control/) | 2021年8月 (代表案例) | ~$8.9M (Punk Protocol 代表案例) | 特权函数授权 | **已发布** | ## 每个案例的结构 ``` cases/--/ README.md # post-mortem cite, property prose, run instructions clean/ # reconstructed pre-exploit Cairo + property test # — invariants HOLD under fuzz planted/ # same-source twin with the planted bug # — invariants FAIL under fuzz within timeout scorecard.clean.md # expected clean-leg run scorecard.planted.md # expected planted-leg run ``` `clean/` 和 `planted/` 都是完整的 Scarb 项目（按案例 VM 区分），因此 `diff cases/-*/clean/src cases/-*/planted/src` 会以单个局部代码块的形式展示注入的 bug。CI 会在每次 push 时运行这两个分支。 ## CI 对于每个案例，工作流会显式断言这两个分支： - **clean-passes：** 案例的不变性套件针对 CLEAN 参考运行；CI 断言在特定于案例的超时时间内没有属性违规。Exit code 为零且没有 `INVARIANT VIOLATED` 标记。 - **planted-bug-twin-fails：** 相同的套件针对 PLANTED-BUG 孪生样本运行；CI 断言至少存在一处违规。Exit code 为非零且 stdout 上出现该标记。 顶层 `atlas-all.yml` 工作流会在每次 push 时运行每个案例。 `nightly.yml` cron 作业每天运行矩阵，以便上游工具链的发布（scarb / snforge / anchor / foundry / move）在其上线的第二天早晨就能显示为红色徽章，而不是等下一个贡献者偶然发现它。 ## 在本地运行案例 1 需要 `scarb 2.18.0` 以及 `snforge 0.60.x` 或 `0.61.x`。 ``` # clean leg — 属性保持 cd cases/01-cairo-zklend/clean scarb build snforge test # planted leg — 属性触发（≥1 INVARIANT VIOLATED 标记；非零退出） cd ../planted scarb build snforge test ``` 请参阅 [cases/01-cairo-zklend/README.md](cases/01-cairo-zklend/README.md) 以获取属性说明、注入 bug 的 diff 以及事后分析引用。 ## 许可证 Apache-2.0（见 [LICENSE](LICENSE)）。对上游经典体系、受影响协议发布的事后分析以及工具链作者的致谢位于 [NOTICE](NOTICE) 中。 ## AI 披露 参见 [AI_DISCLOSURE.md](AI_DISCLOSURE.md)。 ## 联系方式 运营者：Michael Moffett — michael@caliperforge.com — team@caliperforge.com。

标签：DeFi, Web3, 区块链安全, 智能合约审计, 通知系统