caliperforge/solana-invariant-atlas

# solana-invariant-atlas [](https://github.com/caliperforge/solana-invariant-atlas/actions/workflows/ci.yml) ## 概述 该 atlas 是一个经过精心整理的 Anchor-program bug 类库，同时也是一个类形状的 emit 层，目前可渲染为 Crucible v0.2.0 测试套件，路线图上计划支持 Trident v0.12.0 测试套件。工作单元是 Anchor 的 account-and-IDL 模型；执行轨道是在锁定的 Solana 轨道上运行的 Crucible v0.2.0 over LiteSVM（anchor-lang 1.0.1，solana-cli 2.1.21，platform-tools v1.52）。该类库背后的依据是在这些相同锁定轨道上对真实目标进行的 `n = 4` 次移植：三个 Jito 程序（tip-distribution, priority-fee-distribution, tip-payment）以及 Pyth Solana Receiver。每次移植都提供了具有成对的 clean 和 planted 双胞胎的类形状 invariants，因此每次推送都能持续证明每个类的捕获能力。该 atlas 原生拥有 `collateral_mint_ref` 参考双胞胎、采用脚手架、覆盖率地图以及此文档集；它通过 `cases/*/CITATION.md` 以 URL 形式引用了四个真实目标移植仓库，并将 `cf-invariants-anchor-*` crates 作为锁定的 git 依赖项进行消费。所有被引用的移植 URL 均保持规范状态。 ## 这是什么 / 这不是什么 **这是什么。** 这是一个建立在 Solana 生态系统已经免费提供的引擎之上的、经过精心整理的 bug 类库和成对 fixture 准则。这是一个类形状的 emit 层，它将 atlas 的类族 invariants 渲染为现有引擎的 fixture 源码，因此相同的类形状可以到达程序团队已经在使用的任何引擎。这是一个具有在每个被引用的 commit 处持续证明检测能力的回归测试套件。 **这不是什么。** 它不是 fuzzer；atlas 会渲染成 fuzzers，但它本身不是。它不是 Trident 或 Crucible 的替代品；这些引擎保持在上游，未经修改，并且是运行 atlas 的 fixture 的运行时基础。它不是 bug 发现引擎或安全发现服务；截至 2026-07-02，atlas 没有任何上游披露，也不做任何发现声明。它不是审计的替代品；手动审查、规范验证和 posture 审查（upgrade authority、program-derived address 维护、sysvar 处理）不是本仓库所做的工作。 ## 已经免费提供的部分 Solana 生态系统已经为 invariant 工作提供了丰富的免费技术栈。该 atlas 位于该技术栈之上；它不会替换其中的任何部分。以下每一项都是第一类依赖项或比较器，在一行中诚实地引用，以便读者能够找到该 atlas 并不打算替换的工具。 - **Trident v0.12.0** (Ackee Blockchain, MIT)。用于 Solana / Anchor 程序的 Stateful 和 invariant fuzzing。已发布并维护；提供了自己的 `#[flow]` 注解的 flows、snapshot API、断言式状态检查，以及涵盖 token、hello_world 和 internal-test 表面的示例树。 - **Crucible v0.2.0** (Asymmetric Research)。通过 sBPF 覆盖率指导在 LiteSVM 上进行基于属性的 fuzzing。提供了 `#[invariant_test]` 宏、运行时 `crucible run` 以及单目标粒度的示例程序（`escrow`、`staking`）。 - **Anchor native tests + `solana-program-test`** (Solana Foundation, Apache-2.0)。Anchor 框架附带的单元和集成测试轨道；对实时账户状态进行确定性的单交易和多指令断言。 - **mollusk v0.13.4** (Anza, Apache-2.0)。用于 `solana-program-test` 用例的轻量级进程内 runtime，在单指令粒度上支持 `Check::account(pubkey).lamports(...)`。 - **LiteSVM v0.13.1** (Apache-2.0)。快速的进程内 SVM，用作 Crucible 下方的底层基础以及通用测试轨道。 **atlas 在此基础上添加了什么。** 一个单一来源的、经过精心整理的 Solana bug 形状类库（通过 fixture 端的 ledger + `fuzz_assert_eq!` 实现余额守恒；通过 `last_seen_*` 快照 + `fuzz_assert_le!` 实现单调记账；通过成对的 probe + sticky-flag 断言实现访问控制，包括缺少 Anchor constraint 的 mint-authority 子形状），一个成对的同源 clean 和 planted 双胞胎准则，其 CI 在每次推送时断言每个单元格上的 `clean = 0` 标记和 `planted >= 1` 标记，一个类形状的 emit 层，将这些类形状渲染为 Crucible（今天）和 Trident v0.12.0（渲染器已合入 T-satlas-03 分支；runtime 验证和表面语言切换根据设计说明受后续调度的限制）的 fixture 源码，以及一个“带上你的程序”的采用路径，在相同的锁定轨道上将 atlas 指向采用者自己的 Anchor 程序。截至 2026-07-02，我们没有找到公开的 Solana 版本的成对 clean 和 planted 准则；我们不主张排他性。 **为什么这不是向 Crucible 提交的 PR。** Crucible 是引擎和原始测试表面。atlas 是它上面的一层：一个精心整理的类库、一个成对 fixture 准则，以及一个与该引擎组合（而非扩展）的类形状 emit 层。fuzzer 团队不会将精心整理的语料库和类注册表代码生成器合并到引擎仓库中；它们的作用范围确实截然不同。Crucible 仍然是规范的引擎大本营；atlas 仍然是规范的类库大本营；Trident v0.12.0 的 emit 目标对另一个引擎执行相同的操作。 ## 覆盖率地图（节选） `docs/coverage_map.md` 的压缩视图。包含文件级引用、读者校对页脚、适用性调查（2026-07-02 抽样的 `n = 24` 个公开 Anchor 程序）和附录的完整表格位于 [docs/coverage_map.md](docs/coverage_map.md)。 | Invariant 类 | Trident v0.12.0 | Crucible v0.2.0 | Anchor native + solana-program-test v1.1.2 | mollusk v0.13.4 | LiteSVM v0.13.1 | 审计机构套件 (awesome-trident-tests, `main` @ 2026-07-02) | 截至 2026-07-02 比较器未覆盖（暂时为 clean） | |---|---|---|---|---|---|---|---| | `balance_conservation` | 仅 harness | 仅 harness | 仅 harness，仅限 unit-level | 仅 harness，仅限 unit-level | (空) | 针对特定目标，无类形状 fixture | 由 atlas 提供 | | `monotonic_accounting` | 仅 harness | 仅 harness | 仅 harness，仅限 unit-level | 仅 harness，仅限 unit-level | (空) | 针对特定目标，无类形状 fixture | 由 atlas 提供 | | `access_control` | 仅 harness | 仅 harness | 仅 harness，仅限 unit-level | 仅 harness，仅限 unit-level | (空) | 针对特定目标，无类形状 fixture | 由 atlas 提供 | | `access_control.collateral_authority` (子形状) | 仅 harness | 仅 harness | (空) | (空) | (空) | (空) | 由 atlas 提供 | | `oracle_freshness` (计划中，Phase 2) | (计划中) | (计划中) | (计划中) | (计划中) | (计划中) | (计划中) | 未由 atlas 提供 | **如何阅读此地图。** 每一行是一个 atlas invariant 类或其子形状。每一列是一个程序级比较器；最右侧的列记录了截至 2026-07-02 哪个程序级比较器没有提供类形状的 fixture。完整地图中的每个非空单元格都带有格式为 `owner/repo/path @ ` 的文件级引用，其中 `` 是一个 7 字符的 commit sha 或一个不可变的发布 tag。`harness-only` 表示比较器提供了引擎，但没有提供类形状的示例，即将同一程序的 clean 和 planted 变体配对，并证明 invariant 在 planted 上触发而在 clean 上通过。最右侧的列截至 2026-07-02 暂时为 clean，并不代表持久的排他性声明；如果审查者发现某个比较器提供了与这些行之一匹配的类形状 fixture，则根据完整地图中的维护规则，atlas 行将以累加方式进行更新。 **范围说明。** Solfuzz / solfuzz-ag-agave (Firedancer) 和 sig-fuzz (Syndica) 是 Solana VM 一致性 harness，用于检查两个 VM 实现是否在执行语义上达成一致；它们超出了作为程序级比较器的范围，因此被有意省略在上面的列中。 ## 参考案例和引用的移植 ### R1 参考: `references/collateral_mint_ref{,_planted}` 合成的 Anchor 抵押 mint 程序形状。Bank config 上的三个指令：`initialize_bank`、`deposit` 和 `mint_receipts`。clean twin 带有 mint-equality 的 Anchor constraint，将 `collateral_account` 绑定到 Bank 初始化时使用的抵押 mint；planted twin 仅删除了这一行，其他什么都不改。这个缺失的 constraint 在 planted twin 中属于规范违规：`deposit` 在未验证其 mint 字段的情况下读取 `collateral_account`，因此 fixture 端的 `expected_receipts` 账本（仅在从授权抵押 mint 提取的存款时增加）与链上的 `bank.total_receipts_minted` 在任何通过未经授权的 mint 路由的存款之后产生分歧。Crucible fuzz walk 和确定性回归步骤都会在出现第一个分歧时停止，并打印 `INVARIANT VIOLATED collateral_authority`。历史事后分析记录了真实的 Anchor 家族 Solana 程序，其中 collateral 或 printer-account mint 在没有 deposit 路径上的 mint-equality constraint 的情况下被接受；Cashio 事件是被广泛引用的示例，此处仅作为动机引用一次。可执行的规范和 fixture 自行独立存在。完整案例说明： [references/collateral_mint_ref/README.md](references/collateral_mint_ref/README.md)； 差异显示在案例 README 中。 ### 四个引用的真实目标移植（恰好 `n = 4`） | 移植 | 练习的类（家族） | 在线 URL | CITATION | |---|---|---|---| | cf-invariants-jito (Jito tip-distribution) | balance_conservation 和三个 access_control 子形状 | https://github.com/caliperforge/cf-invariants-jito | [cases/jito/CITATION.md](cases/jito/CITATION.md) | | cf-invariants-jito-priorityfee (Jito priority-fee-distribution) | monotonic_accounting (state-commit 子形状) | https://github.com/caliperforge/cf-invariants-jito-priorityfee | [cases/jito-priorityfee/CITATION.md](cases/jito-priorityfee/CITATION.md) | | cf-invariants-jito-tippayment (Jito tip-payment) | monotonic_accounting (两个 state-commit 子形状) 和 access_control (bounds-check 子形状) | https://github.com/caliperforge/cf-invariants-jito-tippayment | [cases/jito-tippayment/CITATION.md](cases/jito-tippayment/CITATION.md) | | cf-invariants-pyth (Pyth Solana Receiver) | access_control (governance-transfer atomicity 子形状) 和 balance_conservation (rent-return-authority 子形状) | https://github.com/caliperforge/cf-invariants-pyth | [cases/pyth/CITATION.md](cases/pyth/CITATION.md) | 每个 CITATION 文件内联镜像了移植的 CI 徽章，将移植的类表固定到 7 字符的 commit sha，并明确声明该引用未将任何上游代码引入到 atlas 中，且未声称在上游 Jito 或 Pyth 中发现了 bug。`n = 4` 这个数字恰好是该类库背后的依据；`n = 24` 的公开 Anchor 程序适用性调查中的总体覆盖数据作为一个单独且有边界的数字位于 `docs/coverage_map.md` 中。 ## 带上你的程序 `adopt/` 树包含一个可复制粘贴的 GitHub Actions 工作流，一份采用分步说明 README，其中包含了从 `git clone` 到采用者自己的程序运行通过的所有编号步骤（对 solana-cli 2.1.21 进行固定检查、IDL 解析、带有启发式默认值和位于显式 flag 之后的 AI 来源的 `cf-invariants-anchor suggest`、`emit --target crucible`、运行两个步骤），以及一个针对 `collateral_mint_ref` 端到端执行并带有完整的演示示例。该脚手架设计为可在不到一小时内完成采用；一旦非作者的定时冷运行从 code_quality_reviewer 返回 PASS，观察到的冷运行数字将记录在本节中。诚实的范围：脚手架提供了 harness 和经常出现的类模式；特定于程序的业务逻辑属性仍要求采用者声明他们自己的语义。建议器从 IDL 中对候选者进行排名，它并不了解程序的规范。 完整指南：[adopt/README.md](adopt/README.md)。工作流 模板：[adopt/workflow-template.yml](adopt/workflow-template.yml)。 演示示例记录： [adopt/worked-example-log.md](adopt/worked-example-log.md)。 ## 许可证 该 atlas 采用 Apache-2.0 许可证。参见 [LICENSE](LICENSE)。第三方 署名位于 [NOTICE](NOTICE)：Crucible、Trident v0.12.0、 Anchor、`solana-program-test`、LiteSVM 和 mollusk 分别在各自的发布许可下被引用。没有任何上游程序代码被引入到 atlas 中；`collateral_mint_ref` 合成程序完全是我们自己的代码。创作栈中的 AI 参与情况已在 [AI_DISCLOSURE.md](AI_DISCLOSURE.md) 中披露，包括 suggester 来源模型及其 `MockTransport` 默认值。 ## 治理和累加准则 现有的五个 `experiments/cf-invariants-*` 移植仓库不受此 atlas 的影响而保持字节不变；五个在线引用的移植 URL 在各自的提交历史中保持规范状态。新的类家族将进入此 atlas 或 `cf-invariants-anchor` 中，绝不会作为移植仓库的 fork 出现。最右侧的覆盖率地图列暂时为 clean，日期为 2026-07-02；根据 `docs/coverage_map.md`，未来的重新检查要么重新标注该列的日期，要么清除主要源状态发生更改的行的条目。事后分析来源遵循一句式的不可操作约定：可操作的规范必须在没有事件的情况下独立存在，并且本仓库中不包含任何事件机制、变现路径或特定目标的复现。完整的设计原理、类添加程序、Trident v0.12.0 锁定决策以及 solana-cli 2.1.21 PATH-prefix 说明位于 [docs/design_notes.md](docs/design_notes.md) 中。atlas 所遵循的措辞标准是 CaliperForge 组织仓库中的 `agents/engineering_lead/templates/planted_twin_framing_discipline.md`；设计说明中包含读者摘要和指引。

标签：Solana, 区块链安全, 可视化界面, 安全测试, 攻击性安全, 智能合约, 通知系统