divyangchauhan/Pramana
GitHub: divyangchauhan/Pramana
Pramana 是一款多智能体智能合约审计器,通过强制要求可执行 Foundry PoC 来证明每个漏洞,从而消除 LLM 审计中的幻觉发现。
Stars: 0 | Forks: 0
# Pramana
**一个多智能体智能合约审计器,通过可执行的 exploit 证明每一个漏洞。**
没有 PoC(概念验证),就没有发现结果。在 Claude、GPT 和 Kimi 之间保持提供商中立,并从第一天起就通过评估测试框架进行衡量。
[](https://github.com/divyangchauhan/Pramana/actions/workflows/ci.yml)





大多数 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 onlycontract · 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/
更多选项
``` # 其他 providers(传入有效的 model id) uv run python -m pramana.eval.harness --provider openai --model
旨在端到端地展示 Agentic LLM 系统、评估的严谨性以及智能合约安全性。
标签:DLL 劫持, Foundry, 区块链安全, 多智能体, 大语言模型, 智能合约审计, 逆向工具