divyangchauhan/Pramana

GitHub: divyangchauhan/Pramana

Pramana 是一款多智能体智能合约审计器,通过强制要求可执行 Foundry PoC 来证明每个漏洞,从而消除 LLM 审计中的幻觉发现。

Stars: 0 | Forks: 0

# Pramana **一个多智能体智能合约审计器,通过可执行的 exploit 证明每一个漏洞。** 没有 PoC(概念验证),就没有发现结果。在 Claude、GPT 和 Kimi 之间保持提供商中立,并从第一天起就通过评估测试框架进行衡量。 [![CI](https://static.pigsec.cn/wp-content/uploads/repos/cas/ad/ad5834178f7599af9fdda11629d49cae07f2997beec49821b2920eff5bfd50e7.svg)](https://github.com/divyangchauhan/Pramana/actions/workflows/ci.yml) ![Python](https://img.shields.io/badge/python-3.11%2B-3776ab) ![Foundry](https://img.shields.io/badge/tested_with-Foundry-2a2a2a) ![Providers](https://img.shields.io/badge/providers-Anthropic%20·%20OpenAI%20·%20Kimi-6f42c1) ![Verification](https://img.shields.io/badge/findings-verified_by_executable_PoC-2ea043) ![License](https://img.shields.io/badge/license-MIT-green)
大多数 LLM “审计”工具会向你抛出一堆听起来言之有理的发现结果,然后让你自己去从幻觉中筛选出真正的 bug。Pramana 采取了相反的立场: 这一设计选择——*以可执行的证明取代模型的置信度*——正是演示程序与你愿意信任的工具之间的分水岭。该项目中的其他一切,都是为了让这一想法具有可复现性和可衡量性而存在的。 **Pramāṇa** (प्रमाण) 在梵语中意为*“获取知识/证明的有效手段”*——一个发现结果只有在被证明之后,才能算作知识。 ## 结果 核心指标是**由可执行 PoC 确认的真阳性发现**——即测试框架在干净的工作区中*独立重新运行并观察其通过*,且与已知的真实漏洞相匹配的发现结果。 在双智能体 pipeline 上使用 `claude-opus-4-8` 运行完整语料库,**重复 3 次——每次运行结果完全相同**: | 测试集 | 漏洞类别 | 已知 bug | 通过 PoC 证明 | 真阳性 | |---|---|:---:|:---:|:---:| | `reentrancy-vault` | reentrancy | 1 | ✅ | 1 | | `unprotected-owner` | access-control | 1 | ✅ | 1 | | `tx-origin-wallet` | tx-origin | 1 | ✅ | 1 | | `unchecked-overflow-token` | integer-overflow | 1 | ✅ | 1 | | `bank-multi` | reentrancy **+** access-control | 2 | ✅ ✅ | 2 | | `reentrancy-vault-patched` | *无——阴性对照* | 0 | — | 0 **(0 假阳性)** | **6 / 6 真阳性 · 召回率 1.00 · 精确率 1.00 · 阴性对照中 0 假阳性。** 每个发现都附带了一个 Foundry exploit,测试框架会从零开始针对未触及的目标合约重新运行它——包括组合型的 `bank-multi`,其中两个不同的 bug 都被独立发现并证明。 阴性对照是值得深思的结果。交给它一个*看起来*完全像 DAO reentrancy 测试集的合约时,pipeline 报告什么都没发现——finder 读取了调用顺序,看到状态修改在交互之前发生,因此完全没有提出任何候选项,所以也没有调用任何 verifier。 单智能体 Phase 0 运行通过一条更易懂的路径得出了相同的结论:它编写了一个 reentrancy exploit,运行它,然后**看着它失败**。 无论哪种方式,这都是对代码进行推理与对其形状进行模式匹配之间的区别——而且只有*因为*语料库中包含了不应被报告的内容,这一点才得以显现。诚实地指出一点:这种拆分使得*干净合约*的报告变得更单薄,因为在提案阶段被过滤掉的声明不会留下任何关于检查了什么的记录。这是一个当前任何指标都无法捕捉到的交付质量问题,也是 Phase 2 reporter 的工作。 📊 **[完整基线记录 →](baselines/phase-1/)** ——所有 3 次运行、每个测试集的稳定性、锁定的 commit 和 config,以及针对 [Phase 0](baselines/phase-0/) 的回归检查。每个测试集对应的智能体自身审计报告也都随之一并提交。 一个离线的 `--self-check` 可以复现整个评分 pipeline(工作区构建 → `forge test` → 类别匹配 → 计数),且**无需 API key**。 ### 评估发现的、而召回率无法捕捉的问题 每个架构变更都会与前一阶段记录的基线进行比对,作为下限和上限而不是平均值——一次幸运的运行绝不能掩盖糟糕的运行: ``` $ uv run python -m pramana.eval.baseline --runs runs/*.json \ --out-dir baselines/phase-1 --against baselines/phase-0/baseline.json ✅ No regression - True positives: floor 6 vs baseline floor 6 — gate held - Negative-control false positives: worst 0 vs baseline ceiling 0 — gate held - Unmatched confirmed findings: worst 0 vs baseline ceiling 0 — gate held ``` 第三行的存在是因为前两行漏掉的一个 bug。拆分 pipeline 保持了 6/6 的真阳性和 0 个阴性对照假阳性——一次顺利通过——但同时悄悄地把 `tx.origin` bug 报告了**两次**:一次是 `tx-origin`,一次是 `access-control`,且有两个 PoC 演示了相同的钓鱼攻击。这个重复项没有匹配到任何*未被认领*的已知 bug,因此它从所有被观测的数字中消失了。 这是上下文隔离的直接后果:每个 verifier 只能看到一个声明,无法知道另一个声明是同一个 bug。修复方法是在 finder 处(每个不同的根本原因对应一个发现),但教训在于指标——**召回率在结构上对重复项视而不见**,因此 pipeline 可以在获得 6/6 分数的同时,用报告充斥着重复内容。`unmatched_confirmed_findings` 现在会对它们进行计数并进行拦截。 ## 工作原理 ``` flowchart TD C["Solidity contract"] --> SL["run_slither → prioritized leads"] SL --> F subgraph F["Anumana · finder — read-only"] direction LR FL["LLM"] -->|"tool calls"| FT["read_file · run_slither"] FT -->|"results"| FL end F --> CLAIM{"bare claim only
contract · location
vuln_class · hypothesis"} subgraph V["Khandana · verifier — one per finding, fresh context"] direction LR VL["LLM"] -->|"tool calls"| VT["read_file · write_file
run_foundry_test"] VT -->|"results"| VL end CLAIM --> V V --> OUT["confirmed / refuted / inconclusive
+ audit report"] OUT --> EV["eval harness"] EV -->|"re-runs each confirmed PoC
in a pristine workspace"| TP["✅ true positives"] ``` 一次从头到尾的完整审计: 1. **奠定基础。** [Slither](https://github.com/crytic/slither) 运行一次,其 detector 的命中结果为 finder 提供种子——*这些是需要调查的线索,其本身绝不是最终的发现。* 2. **调查。** finder 阅读实际的 Solidity 代码(`read_file`),追踪流程,并基于它实际检查过的代码提出可证伪的 exploit 假设。它没有能力编写或执行任何内容。 3. **隔离。** 每个假设都作为一个**光秃秃的声明**(bare claim)传递给一个独立的 verifier——包含合约、位置、类别、假设。finder 的笔记和严重程度猜测都会被保留不予传递。 4. **证伪。** verifier 的默认假设是该声明是*错误的*。它会编写一个 Foundry PoC(`write_file`)并运行它(`run_foundry_test`);只有通过的、由断言支持的测试才会将结论翻转为 `confirmed`。否则,它会返回 `refuted` 或 `inconclusive`。 5. **评分。** 测试框架使用*原始的*目标重建一个全新的工作区,仅复制智能体的 PoC,然后重新运行它——因此,只有当 exploit 真正执行成功时,该发现才算数。 **为什么这种拆分很重要。** 这种隔离是结构性的,而不是通过 prompt 实现的:每次验证都是一次独立的 `run_agent` 调用,拥有一个物理上分离的 `messages` 列表,并由一个白名单(`contracts.bare_claim`)进行初始化。finder 的置信度没有任何渠道可以传递给 verifier——而且由于种子是一个白名单,以后添加到 `Finding` 的字段不可能在不知不觉中开始泄露信息。工具范围也强制执行了相同的边界:finder *无法*证明其自身的假设,因为它没有 `write_file`。 以下是一次真实的审计过程(`--verbose`),包括 verifier 调试其自身 PoC 的过程: ``` [finder] read_file src/EtherStore.sol [finder] read_file src/EtherStore.sol # traces withdraw() call order [finder] (final JSON) F-001 · reentrancy · "external call precedes state update" ↓ bare claim only — notes and severity guess withheld [verifier] read_file src/EtherStore.sol # verifies the claim against the code [verifier] write_file test/F-001.t.sol # first PoC attempt [verifier] run_foundry_test # ❌ fails: ETH-seeding bug in the test [verifier] write_file test/F-001.t.sol # self-corrected [verifier] run_foundry_test # ✅ passes: vault drained 6→0 [verifier] (final JSON) confirmed · high · PoC test/F-001.t.sol ``` ## 为什么该设计经得起考验 三个理念承担了主要作用——每一个都是经过深思熟虑的工程选择,而不是原型阶段的偶然产物: - **可执行的验证。** Ground truth 是 `forge test`,而不是模型的自我评估。测试框架在隔离的工作区中针对*原始*合约重新运行每个 PoC,因此智能体无法通过编辑目标来伪造通过。`inconclusive` 结论和非通过的 PoC 绝不计入结果。 - **评估优先,而非事后评估。** 衡量测试框架与 pipeline 在同一切片中发布。每次运行都会产生可复现的真阳性计数以及支持性诊断(候选数量、验证前后的精确率、召回率)——这是用于凭经验回答*“哪个模型、哪个 prompt、哪个 config 才真正有效?”*这一问题的工具。 - **提供商中立的核心。** 智能体循环从不导入特定实验室的 SDK;它只使用一种标准的 message/tool 格式。在 Claude ↔ GPT ↔ Kimi 之间切换只是更改一下 config,而添加一个实验室只需一个 adapter 文件。这正是让评估能够扫描不同模型、而不是把赌注押在一个模型上的原因。 ## 语料库 五个自包含的测试集,每一个都以一次标志性的现实世界 exploit 为原型,包含带有标签的已知 bug 集和参考 PoC: | 测试集 | 类别 | 原型 | |---|---|---| | `reentrancy-vault` | reentrancy | The DAO (2016) | | `unprotected-owner` | access-control | Parity multisig unprotected initializer (2017) | | `tx-origin-wallet` | tx-origin (SWC-115) | `tx.origin` 钓鱼 | | `unchecked-overflow-token` | integer-overflow | BeautyChain (BEC) `batchOverflow` (2018) | | `bank-multi` | reentrancy **+** access-control | 组合型双 bug 合约——演练 1:1 匹配 | 每个 `pramana/eval/datasets//` 都包含易受攻击的源代码(`src/`)、一个 `fixture.json` 标签集,以及一个用于离线验证评分器的 `reference/` exploit PoC。 **没有提示性信息。** 目标源代码只包含那些*对 bug 一无所知*的开发者也会编写的注释——它们描述的是意图,而不是缺陷。一个记录了自身漏洞的测试集衡量的是阅读理解能力,而不是发现能力,因此测试会拒绝目标注释中出现描述 bug 名称的词汇,并且每次运行都会记录语料库指纹:来自不同语料库的结果永远不会被相互比较。 **阴性对照。** 仅靠召回率很容易被一个报告所有内容的模型所欺骗,因此语料库还附带了 `reentrancy-vault-patched`——它是 `reentrancy-vault` 的一个在其他方面完全相同的孪生版本,其 `withdraw()` 在交互之前应用了状态修改。它声明了**零**已知 bug,因此针对它的每一个确认的发现都明确无疑是一个假阳性。它的 `reference/` 包含的是控制测试而不是 exploit,它断言资金耗尽操作现在会 revert *并且*正常的提款仍然会成功——否则,一个退化的、总是 revert 的“修复”会被当成是安全的而通过。CI 还会针对修补后的孪生版本重放真实的 exploit,并要求其失败,从而确保该对照不会悄无声息地失效。 扩展到公共基准(Code4rena / Sherlock / DeFiHackLabs / EVMbench)以及完整的成对补丁集已在路线图上。 ## 快速开始 需要 [`uv`](https://docs.astral.sh/uv/),以及位于 `PATH` 中的 [`forge`](https://getfoundry.sh) (Foundry) 和 [`slither`](https://github.com/crytic/slither)。 ``` uv sync # Python deps (cd pramana/eval/foundry_template && forge soldeer install) # restore forge-std ``` `forge-std` 是一个锁定了版本的 [Soldeer](https://soldeer.xyz) 依赖项(`foundry.toml` + `soldeer.lock`)——它是被获取的,而不是被直接打包的;如果缺少它,测试框架会打印出确切的恢复命令。 **离线自检** ——无需 API key;对参考 PoC 进行评分,以端到端地证明评分机制: ``` uv run python -m pramana.eval.harness --self-check ``` ``` fixture cfg cand ref conf poc+ TP recall ---------------------------------------------------------------------------------- bank-multi reference-poc 2 0 2 2 2 1.00 reentrancy-vault reference-poc 1 0 1 1 1 1.00 reentrancy-vault-patched reference-poc 0 0 0 0 0 - tx-origin-wallet reference-poc 1 0 1 1 1 1.00 unchecked-overflow-token reference-poc 1 0 1 1 1 1.00 unprotected-owner reference-poc 1 0 1 1 1 1.00 ---------------------------------------------------------------------------------- HEADLINE — true-positive findings confirmed with executable PoCs: 6 / 6 known bugs NEGATIVE CONTROLS (1) — false positives: 0 confirmed, 0 with a passing PoC ``` `recall` 显示为 `-` 表示这是一个阴性对照:它没有已知 bug,因此召回率未定义,真正重要的数字是它的假阳性计数。 **实时的智能体运行** ——将你的 key 放入 `.env`(应用程序会自动加载它,并且如果所选提供商的凭证缺失,它会拒绝启动): ``` cp .env.example .env # fill in ANTHROPIC_API_KEY (or OPENAI / MOONSHOT) uv run python -m pramana.eval.harness --provider anthropic ``` `--pipeline phase1` (finder → 隔离的 verifier) 是默认设置。传入 `--pipeline phase0` 以运行最初的单智能体切片——两者都保持可运行状态,以便对架构变更进行*衡量*,而不是主观断言。表中的 `ref` 计算了 verifier 主动驳回的声明数量。 **捕获基线** ——重复运行,然后将结果汇总到已提交的回归记录中(pipeline 是非确定性的,因此单次运行只是一个点估计值,而不是基线): ``` for i in 1 2 3; do uv run python -m pramana.eval.harness --provider anthropic \ --json runs/run-$i.json --report-dir runs/reports-$i done uv run python -m pramana.eval.baseline --runs runs/run-*.json \ --out-dir baselines/phase-0 --label "Phase 0" ```
更多选项 ``` # 其他 providers(传入有效的 model id) uv run python -m pramana.eval.harness --provider openai --model uv run python -m pramana.eval.harness --provider kimi --model # 实用 flags --fixtures reentrancy-vault tx-origin-wallet # restrict the set --json results.json # full per-finding results --report-dir ./reports # write a per-fixture audit report.md --verbose # stream tool calls to stderr --work-dir ./runs # keep workspaces (agent PoCs) to inspect --forge-retries 3 # retries for transient forge/anvil flakiness ```
## 提供商 核心仅依赖于 `providers/base.py` 中的标准类型;每个 adapter 都是唯一接触特定供应商 SDK 的文件。 | 提供商 | Adapter | 说明 | |---|---|---| | **Anth** | `providers/anthropic.py` | 通过流式传输(对大 `max_tokens` 安全)的 Messages API;默认为 `claude-opus-4-8`。无 `temperature`/`thinking` 配置。 | | **OpenAI** | `providers/openai.py` | Chat Completions + function calling;使用 `max_completion_tokens`;无 `temperature`(对 reasoning-model 友好)。 | | **Kimi / Moonshot** | `providers/kimi.py` | 通过 Moonshot 的 OpenAI 兼容 API 的 Kimi K3——重用 OpenAI 的网络协议转换,仅替换 endpoint(`MOONSHOT_API_KEY`)和传统的 `max_tokens` 参数。 | 每个 adapter 都会在启动时验证其模型,并且绝不会悄悄地回退到另一个提供商——审计结果和成本从而保持可复现性。 ## 布局 ``` pramana/ ├── providers/ # canonical adapter boundary (base) + anthropic / openai / kimi ├── agents/ # run_agent (bounded, isolated loop) + finder / verifier prompts & tool scopes ├── tools/ # sandboxed read_file / write_file / run_slither / run_foundry_test ├── contracts.py # Pydantic Finding / Verdict / Phase0Output + boundary parsing ├── pipeline.py # the orchestrator — audit_phase0 / audit_phase1 ├── config.py # per-role provider/model config, pinned per run ├── env.py # .env auto-load + startup credential validation └── eval/ ├── datasets/ # the real-world corpus (5 vulnerable fixtures / 6 known bugs + 1 negative control) ├── foundry_template/ # foundry.toml + soldeer.lock (forge-std pinned) ├── workspace.py # per-run Foundry workspaces ├── harness.py # runs audit() over fixtures, counts true positives └── baseline.py # folds repeated runs into a baseline; gates later phases baselines/ # recorded baselines + the agent's audit reports baselines/phase-0/ # the recorded Phase 0 baseline + the agent's audit reports tests/ # 105 offline tests (parsing, grading, isolation, tool scope, corpus integrity, negative control) .github/workflows/ci.yml # ruff + pytest + self-check on every push docs/design.md # full system design & staged build plan ``` ## 质量 ``` uv run pytest # 105 offline tests, no network/keys uv run ruff check pramana tests # lint uv run pyright pramana tests # type check (clean) ``` 测试涵盖了边界 JSON 解析、漏洞类别匹配(包括多 bug 的 1:1 匹配)、评分路径(未通过的 PoC 或错误的类别绝不计入)、Foundry 运行器的瞬时故障重试、所有三个实验室的标准格式↔提供商网络协议转换、环境变量验证、在结果不一致的多次运行间进行基线聚合,以及阴性对照自身的完整性——包括针对修补后的孪生版本重放真实的 exploit 以证明其失败。CI 会在每次 push 时运行完整的测试套件以及离线自检([`.github/workflows/ci.yml`](.github/workflows/ci.yml))。 ## 路线图 Pramana 是按照**垂直切片优先**的原则构建的,在拓宽之前先深化——每个阶段都是对可运行的、可演示系统的重构,绝不是重写。完整计划见 [`docs/design.md`](docs/design.md)。 - **Phase 0 —— 垂直切片** ✅ —— 单个提供商中立的智能体(发现 → 证明 → 报告)、评估测试框架和真实世界语料库。[基线](baselines/phase-0/)。 - **Phase 1 —— 拆分 verifier** ✅ *(当前)* —— 一个上下文隔离的 verifier,它只能看到光秃秃的声明(而不是 finder 的推理过程),因此验证不会受到假设的偏差影响。通过 [Phase 0 基线](baselines/phase-0/) 进行门控,并记录为独立的 [Phase 1 基线](baselines/phase-1/)。 - **Phase 2 —— 添加 reporter + 路由** —— 编写交付物的第三个智能体(并且,由于能同时看到所有结论,它是捕获跨发现重复项的天然场所);由测试框架扫描的基于角色的模型路由;Slither/编译缓存。 - **Phase 3 —— 规模化与强化** —— 公共基准、完整的易受攻击/已修补配对集、结构化的可观测性以及基于角色的成本报告。 这三个智能体具有固定的身份——**Anumana**(finder / 推理)、**Khandana**(verifier / 反驳)、**Nirnaya**(reporter / 结论)——这是一个发现成为被证明的知识的三个 *pramāṇas*(知识来源)。
旨在端到端地展示 Agentic LLM 系统、评估的严谨性以及智能合约安全性。
标签:DLL 劫持, Foundry, 区块链安全, 多智能体, 大语言模型, 智能合约审计, 逆向工具