kamiyo-ai/kamiyo-kani

# KAMIYO Kani [](https://github.com/kamiyo-ai/kamiyo-kani/actions/workflows/ci.yml) [](https://github.com/kamiyo-ai/kamiyo-kani/actions/workflows/kani.yml) [](https://github.com/kamiyo-ai/kamiyo-kani/actions/workflows/docs.yml) [](https://github.com/kamiyo-ai/kamiyo-kani/actions/workflows/benchmark.yml) [](https://github.com/kamiyo-ai/kamiyo-kani/actions/workflows/audit.yml) [](https://crates.io/crates/kamiyo-kani) [](LICENSE)  用于 Solana 程序的可复用 Kani 验证原语和 harness。 ## 为什么？ 大多数 Solana 团队不需要完整的各种形式化方法堆栈。他们需要一条快速路径来在 CI 中证明高价值的 invariant（不变量）： - 值守恒（lamports 和拆分数学） - 风险数学中的边界和单调性 - PDA seed 和 bump 约束 - 重放和状态转换安全 - `AccountInfo` 变更 invariant 本项目遵循一个简单的原则：协作提升生态系统。共享证明原语，减少重复错误，并让验证成为发布流程中的常态。 项目定位： - 将通用的验证缺口贡献给上游 Kani - 在此处保留聚焦 Solana 的 agentic 验证层 - 将证明关键的规约逻辑保留在库内（不扩展对外部 spec-crate 的信任） - 提供可运行的 fail->fix（失败->修复）示例，以便团队在没有形式化方法团队的情况下也能采用 ## 安装 ``` [dev-dependencies] kamiyo-kani = "0.1.1" ``` ## 快速开始 ``` #![cfg(kani)] use kamiyo_kani::risk::{effective_pnl, haircut_ratio}; #[kani::proof] fn payout_is_bounded_by_profit() { let vault: u128 = kani::any(); let principal_total: u128 = kani::any(); let insurance: u128 = kani::any(); let pnl_pos_total: u128 = kani::any(); let my_pnl: i128 = kani::any(); let (h_num, h_den) = haircut_ratio(vault, principal_total, insurance, pnl_pos_total); let payout = effective_pnl(my_pnl, h_num, h_den); kani::assert(payout <= my_pnl.max(0) as u128); } ``` 运行： ``` cargo install --locked kani-verifier cargo kani setup cargo kani -p kamiyo-kani ``` ## 真实用例 ### Escrow 释放策略（前后对比） 修复前（失败的释放策略）： ``` let release_allowed = oracle_signed && now >= expires_at; ``` 修复后（正确的策略）： ``` let release_allowed = agent_signed || (oracle_signed && now >= expires_at); assert_timelock_release_policy(now, expires_at, agent_signed, oracle_signed, release_allowed); ``` 失败运行示例： 通过运行示例： Cargo Kani 输出快照： 可运行的 fail->fix crate： - `examples/escrow-release-policy-vulnerable` - `examples/escrow-release-policy-fixed` ``` # 预期 FAIL cargo kani --manifest-path examples/escrow-release-policy-vulnerable/Cargo.toml \ --harness proofs::vulnerable_allows_oracle_before_expiry # 预期 PASS cargo kani --manifest-path examples/escrow-release-policy-fixed/Cargo.toml \ --harness proofs::fixed_blocks_oracle_before_expiry ``` ### CPI allowlist 执行（前后对比） 修复前（失败的门控）： ``` // BUG: ignores target program identity. !allowed_programs.is_empty() ``` 修复后（正确的门控 + 契约建模）： ``` let should_invoke = cpi_gate_fixed(target_program, &allowed_programs); if should_invoke { invoke_allowlisted_cpi(amount, &mut cpi_log); // via cpi_contract! } assert_cpi_authorized(&cpi_log, &allowed_programs); ``` 可运行的 fail->fix crate： - `examples/cpi-allowlist-vulnerable` - `examples/cpi-allowlist-fixed` ``` # 预期 FAIL cargo kani --manifest-path examples/cpi-allowlist-vulnerable/Cargo.toml \ --harness proofs::vulnerable_allows_unauthorized_program # 预期 PASS cargo kani --manifest-path examples/cpi-allowlist-fixed/Cargo.toml \ --harness proofs::fixed_allows_allowlisted_contract ``` ### PDA seed/bump 约束（前后对比） 修复前（失败的验证器）： ``` // BUG: accepts 17 seeds and up to 64-byte seed length. seeds.len() <= 17 && seeds.iter().all(|seed| seed.len() <= 64) ``` 修复后（正确的验证器 + 辅助断言）： ``` let accepted = pda_validate_fixed(&seeds); if accepted { assert_seed_count_valid(seeds.len()); assert_seed_lengths_valid(&seeds); } ``` 可运行的 fail->fix crate： - `examples/pda-seed-bump-vulnerable` - `examples/pda-seed-bump-fixed` ``` # 预期 FAIL cargo kani --manifest-path examples/pda-seed-bump-vulnerable/Cargo.toml \ --harness proofs::vulnerable_accepts_invalid_shape # 预期 PASS cargo kani --manifest-path examples/pda-seed-bump-fixed/Cargo.toml \ --harness proofs::fixed_rejects_seed_count_overflow ``` ### 重放/幂等语义（前后对比） 修复前（失败的重放语义）： ``` if state.event_id == event_id { return true; // BUG: accepts conflicting duplicate payload } ``` 修复后（幂等语义）： ``` if state.event_id == event_id { return state.payload_hash == payload_hash; } ``` 可运行的 fail->fix crate： - `examples/replay-idempotency-vulnerable` - `examples/replay-idempotency-fixed` ``` # 预期 FAIL cargo kani --manifest-path examples/replay-idempotency-vulnerable/Cargo.toml \ --harness proofs::vulnerable_accepts_conflicting_duplicate_event_id # 预期 PASS cargo kani --manifest-path examples/replay-idempotency-fixed/Cargo.toml \ --harness proofs::fixed_rejects_conflicting_duplicate_event_id ``` ### Oracle quorum/median 约束（前后对比） 修复前（失败的共识检查）： ``` // BUG: only compares reveals <= commits. reveals <= commits ``` 修复后（正确的共识检查）： ``` reveals <= commits && reveals >= quorum && median <= cap ``` 可运行的 fail->fix crate： - `examples/oracle-quorum-median-vulnerable` - `examples/oracle-quorum-median-fixed` ``` # 预期 FAIL cargo kani --manifest-path examples/oracle-quorum-median-vulnerable/Cargo.toml \ --harness proofs::vulnerable_accepts_insufficient_reveals # 预期 PASS cargo kani --manifest-path examples/oracle-quorum-median-fixed/Cargo.toml \ --harness proofs::fixed_accepts_valid_consensus ``` ### Signer/owner 权限检查（前后对比） 修复前（失败的权限门控）： ``` authority_is_signer || true // BUG: bypasses signer + owner checks ``` 修复后（正确的权限门控）： ``` authority_is_signer && authority_owner == expected_owner ``` 可运行的 fail->fix crate： - `examples/signer-owner-authority-vulnerable` - `examples/signer-owner-authority-fixed` ``` # 预期 FAIL cargo kani --manifest-path examples/signer-owner-authority-vulnerable/Cargo.toml \ --harness proofs::vulnerable_allows_unsigned_wrong_owner_authority # 预期 PASS cargo kani --manifest-path examples/signer-owner-authority-fixed/Cargo.toml \ --harness proofs::fixed_accepts_signed_expected_owner ``` ### FSM 状态转换守卫（前后对比） 修复前（失败的转换门控）： ``` before != Settled // BUG: allows non-terminal state to jump anywhere ``` 修复后（显式转换表）： ``` before == after || matches!((before, after), (Init, Funded) | (Funded, Revealed) | (Revealed, Settled)) ``` 可运行的 fail->fix crate： - `examples/fsm-transition-guard-vulnerable` - `examples/fsm-transition-guard-fixed` ``` # 预期 FAIL cargo kani --manifest-path examples/fsm-transition-guard-vulnerable/Cargo.toml \ --harness proofs::vulnerable_allows_skip_to_terminal # 预期 PASS cargo kani --manifest-path examples/fsm-transition-guard-fixed/Cargo.toml \ --harness proofs::fixed_accepts_valid_progression ``` ### 完整 agent 流程基准测试 harness `agent::bench::verify_agent_flow_end_to_end` 证明了一个带有守恒检查的紧凑 escrow 结算路径。 ``` KANI_AGENT=1 cargo kani -p kamiyo-kani --features solana-agent --harness agent::bench::verify_agent_flow_end_to_end ``` 当前基准测试目标：在 `ubuntu-latest` 上于 5 秒内证明此 harness。 ### 端到端自主支付 oracle（x402 风格） `examples/autonomous-payment-oracle-fixed` 证明了一个集成流程： - 带有 quorum/cap 和轮次单调性的 oracle 报价接受 - x402 事件重放/幂等语义 - 用于结算授权的 timelock 策略 - allowlisted CPI 结算和 lamport 守恒 - FSM 从 quote-locked 到 settled 的进展 ``` cargo kani --manifest-path examples/autonomous-payment-oracle-fixed/Cargo.toml \ --harness proofs::proof_autonomous_payment_oracle_flow ``` ### 端到端 x402 SVM agentic 支付 `examples/x402-svm-agent-payments-fixed` 证明了一个 SVM 支付结算流程，包含： - x402 请求重放/幂等语义 - allowlisted CPI 结算目标检查 - payer 和 merchant 账户的 lamport 守恒 - CPI 元数据检查（`lamports_transferred`，`accounts_touched`） ``` cargo kani --manifest-path examples/x402-svm-agent-payments-fixed/Cargo.toml \ --harness proofs::proof_svm_x402_agentic_payment ``` ## 功能标志 (Feature flags) - `kani-full`：CI 可行的完整证明集 - `kani-stress`：SAT 密集型证明（依赖于 `kani-full`） - `solana-agent`：agent invariant + CPI 契约 + FSM 守卫 - `solana-account-info`：符号化 `AccountInfo` 助手和证明 Proof 配置文件： ``` # smoke (默认 CI profile) ./scripts/kani.sh # full (CI-viable full profile) KANI_FULL=1 ./scripts/kani.sh # stress (最重 profile) KANI_FULL=1 KANI_STRESS=1 ./scripts/kani.sh ``` ## 用于分支定制的 AI skills 使用 skills 生成分支本地的证明，而不是为每种 Solana 程序形态扩展上游核心。 列出可用的 skills： ``` ./scripts/skills-apply.sh --list ``` 渲染一个 skill prompt： ``` ./scripts/skills-apply.sh \ --skill solana-account-generator \ --version 1.0 \ --files-modified crates/kamiyo-kani/src/account_info.rs,crates/kamiyo-kani/tests/account_info_verify.rs ``` 应用一个已审查的 AI patch： ``` ./scripts/skills-apply.sh \ --skill add-solana-token-proof \ --version 1.0 \ --patch-file /tmp/llm.patch ``` 运行日志写入 `.skills/runs/` 以便审计。 ## 阶段路线图 - 阶段 1：发布了核心 Solana invariant 和 `AccountInfo` 生成器 - 阶段 2：发布了 `cpi_contract!` 宏和显式 timelock/oracle/FSM 自动断言助手 ## API 文档 - 托管文档：https://kamiyo-ai.github.io/kamiyo-kani/kamiyo_kani/ - 本地生成：`cargo doc --no-deps --open` ## 文档 - `docs/BUG_CLASSES.md` - `docs/ROADMAP.md` - `docs/RELEASE_CHECKLIST.md` - `docs/ADOPTION.md` - `docs/USER_GUIDE.md` - `docs/SKILLS.md` - `docs/FORK_GUIDE.md` - `docs/TRUST_MODEL.md` ## 包含的资产 - `crates/kamiyo-kani`：验证原语和 harness - `templates/anchor-invariants`：面向 Anchor 团队的入门模板 - `docs/BUG_CLASSES.md`：此 crate 针对的显式 bug 类别 - `docs/RELEASE_CHECKLIST.md`：质量和采用发布标准 - `packages/kamiyo-kani-js`：用于解析证明产物的实验性 TypeScript shim ## 相关工作 - Kani `AccountInfo` generator RFC：https://github.com/model-checking/kani/issues/4550 - Percolator risk primitive alignment：https://github.com/aeyakovenko/percolator/pull/19 ## 社区 - Rust Zulip `#model-checking`：https://rust-lang.zulipchat.com/#narrow/stream/266514-model-checking - Solana Discord：https://discord.com/invite/solana ## 许可证 MIT

标签：Kani, Rust, Solana, TLS抓取, Web3, 不变量, 云安全监控, 区块链, 可视化界面, 形式化验证, 智能合约安全, 测试工具, 程序证明, 网络流量审计, 软件安全, 通知系统, 通知系统, 静态分析, 验证原语