SABBA

面向编程代理的安全模板 CLI 与 MCP 服务器，它能够通过实际运行来证明每一个发现。
Claude Code、Codex、OpenCode、Cursor 和 Hermes 调用 Sabba 来证明变更、查找并证明 Bug、审查技能，并在仅限授权范围内驱动安全工具链。
如果无法运行，Sabba 就不会将其报告。

**两个真实的 cJSON 漏洞，通过实际运行复现并证明了它们：** 一个栈耗尽 （CWE-674，已于 2017 年在上游修复）和一个在 `parse_object` 中的堆越界读取 （CWE-125，已于 2024 年修复）。两者均源自对上游修复提交的变体分析，因此它们是 已知 Bug 的复现，而非新发现。Sabba 的贡献在于提供了证据：[docs/scans](docs/scans) 中的每份报告都附带了确切的输入和一个 bundle，你可以在自己的机器上重新运行它， 以观察 AddressSanitizer 是如何被触发的。全新的零日漏洞发现属于后续阶段，本仓库目前 尚未对此作出声明。 这就是整体设计。大多数使用语言模型的工具会问它“这个函数有漏洞吗？”这几乎就像抛硬币， 即使对于大型模型也是如此，而且未经证实的猜测会将维护者淹没在误报中。Sabba 采取了相反的 立场：模型负责提出候选，但**执行预言机（execution oracle）会运行 exploit**，并决定安全 属性是否真的被破坏了。除非 exploit 能够复现，否则什么都不会被报告。发现不是一个分数，它 是一个可重新运行的证明。

## 从任何编程代理中使用它 (MCP) Sabba 作为 MCP 服务器运行，因此 Claude Code、Codex、OpenCode、Cursor 和 Hermes 都可以调用它。 对于 **Codex CLI**，将其添加到 `~/.codex/config.toml`： ``` [mcp_servers.sabba] command = "sabba" args = ["mcp"] ``` 对于 **Claude Code**： ``` claude mcp add sabba -- sabba mcp # after installing; see Install below ``` 14 个工具，大部分无需 token：**`verify_change`**（证明变更在 16 种语言中的任何一种中均有效： 通过内置的 Magga 引擎，一个新测试在基础分支上失败并在目标分支上通过） 和 **`prove`**（相同的差异测试，针对 C/C++/EVM 原生运行）、`verify` / `solve` / `hunt` / `scan`（查找并证明 Bug）、**`security_scan`**（在观察下运行技能以进行审查）、 `rank`、`run_sandboxed` 以及 **`kali_run`**（驱动 nmap / nuclei / ffuf / sqlmap 及其他工具，强制执行范围限制并在沙箱中运行）。通过 `sabba templates install` 安装安全命令模板。完整目录和各客户端配置请参见 [docs/AGENT_INTEGRATION.md](docs/AGENT_INTEGRATION.md)。 **在一个服务器中实现正确性与安全性。** `verify_change` 证明变更达到了其声称的效果； `prove` / `hunt` / `scan` 证明它没有增加新的 Bug。变更验证引擎是 [Magga](https://github.com/8NobleTruths/magga)，作为子模块 vendored 在 `magga/` 下， 并通过 `npx` 驱动，因此这两部分作为一个工具发布。 ## SABBA 能做什么 **找到一个真实的 Bug 并交给你证明，而不是凭直觉。** 每一个发现都作为一个 bundle 提供： 触发它的输入、目标、复现它的命令，以及它产生的 sanitizer 输出。你不必信任报告，你 可以重新运行它。上面的 cJSON Bug 就是这些 bundle 中的两个。 **跨语言、跨链工作，遵循同一规则。** 预言机起源于 C 和 C++ 的内存安全，并泛化为一个 prover 注册表，每个运行时和漏洞类别各有一个 prover。每个 prover 都遵循相同的契约： 只有当判定结果表明在*目标内部*确实发生了与安全相关的真实崩溃时，才会生成发现。 | 领域 | 证明所用的运行时 | 什么才算被证明 | 示例 | | --- | --- | --- | --- | | **C / C++** | clang + AddressSanitizer / UBSan | sanitizer 报告了真实的内存错误 | 堆 / 栈溢出，释放后重用 (use-after-free) | | **Solidity / EVM** | Foundry 主网分叉 | 攻击者的 ETH 利润或链上测得破坏了偿付能力不变量 | 重入资金耗尽 | | **Python** | atheris | 在目标（而非测试框架）中引发的崩溃 | 栈耗尽，C 扩展段错误 | | **Go** | `go test -fuzz` | 在目标帧上恢复的运行时 panic | 索引 / 切片越界，空指针解引用 | | **Java / JVM** | Jazzer | 目标抛出的异常或 Bug 检测器的发现 | 栈溢出，注入检测器 | | **Node JS / TS** | Jazzer.js | 目标崩溃或 Bug 检测器的发现 | 原型污染，ReDoS，路径遍历 | **拒绝被愚弄，即使面对恶意的测试框架。** 当模型编写 fuzz harness 时， 恶意的目标可能会试图引导它伪造崩溃。Sabba 的 fuzzing prover 是*harness-untrusted（不信任测试框架）*的： fuzzer 只负责发现候选输入，然后由 Sabba 控制的重现器重新运行该输入， 并从 harness 无法伪造的通道（真实异常的结构化堆栈，或父进程自己对已终止子进程的测量）中读取判定结果。 它不读取任何 stdout，不读取任何 artifact 文件，也不读取任何魔法短语。完整的模型请见 [docs/PROVER_SOUNDNESS.md](docs/PROVER_SOUNDNESS.md)。 **宁可牺牲覆盖率也要保证可靠性，并且说到做到。** 当崩溃无法被可靠地归因于目标时 （例如挂起或内存不足，这同样很容易是由 harness 死循环或预填充堆引起的），Sabba 会将其 作为未经验证的候选结果提供给人类查看，但绝不会将其生成为正式发现。它宁愿漏报一个 Bug， 也不愿报告一个根本没发生的 Bug。 **在你的工作场景中与你相遇。** 一个命令，多种界面：一个可编写脚本的 CLI（`verify`、 `solve`、`hunt`）和一个交互式 REPL（如上图所示），它能流式传输模型、运行工具， 并将每个证明渲染为一张卡片。运行不带参数的 `sabba` 即可打开 REPL。 ## 在本地运行它，并让它学习该关注哪里 预言机和 prover 从来都不需要模型，而且由模型驱动的部分也可以在你自己的 机器上运行。通过 `SABBA_LLM_BACKEND=local` 将推理指向兼容 OpenAI 的本地端点， 并训练一个小型 CPU 风险排序器，以便检索优先关注高风险函数： ``` sabba mltrain # trains a risk ranker (TF-IDF + logistic), saved to ~/.sabba ``` 三级级联让工作保持低成本：Reflex（无模型：排序器、Z3、预言机）、Resident （本地模型）以及仅用于困难情况的 Teacher（前沿模型）。判定规则在各层级间保持一致， 因此更便宜的层级只会降低覆盖率，而绝不会影响可靠性。参见 [docs/LOCAL_ML.md](docs/LOCAL_ML.md)。 ## 为什么它与众不同 ``` model / z3 / retrieval -> candidate input | v +---------------------------------------+ | execution oracle / prover | | compile, run the exploit, measure | +---------------------------------------+ | | reproduces does not | | FINDING dropped ``` 预言机是唯一的守门员。无论候选结果来自 Z3 合成器还是来自 模型，它都会在被报告之前被编译和运行。Z3 提出输入，预言机决定。模型提出输入， 预言机决定。同样的原则适用于上表中的每个领域：在 EVM 分叉上，由*链*来衡量攻击者的 利润，而不是由模型来衡量，因此模型无法给自己的工作打分。 ## 安装 ``` pip install sabba # or: pipx install sabba / uvx sabba mcp ``` 然后运行 `sabba doctor` 查看此机器上的工具链能证明什么。`verify_change` 通过 `npx` 调用 Magga 引擎，因此它需要你的 PATH 中有 Node，但不需要额外的安装 步骤。 若要参与开发 Sabba 本身，请使用子模块克隆它并使用安装程序，该程序会在 `~/.sabba` 下设置一个隔离的环境，并将 `sabba` 命令放在你的 PATH 中： ``` git clone --recurse-submodules https://github.com/8NobleTruths/sabba.git cd sabba ./install.sh ``` 以后使用 `sabba update` 更新，使用 `sabba uninstall` 卸载。 Prover 使用你所针对领域的工具链：C 和 C++ 使用带有 AddressSanitizer 的 clang， EVM 使用 Foundry，托管语言则使用 atheris、`go`、Jazzer 或 Jazzer.js。 `sabba doctor` 会报告当前存在哪些内容。 ## 快速开始 ``` sabba # opens the REPL; type /setup for guided first-run setup # 无需 model，证明已知目标： sabba verify cwe121_stack_overflow sabba solve cwe121_stack_overflow ``` 这两个名称是包内置的演示目标，因此安装好的 Sabba 可以在第一条命令中证明 一个真实的 Bug，无需克隆、无需模型、也无需 API 密钥。将相同的命令指向一个 包含 `target.json` 的你自己的目录，即可处理你自己的代码。 首次运行会打开一个引导式设置：`/setup` 会显示一个清单，每个步骤都会解释为什么 值得去做、如果跳过它会怎样以及执行它会怎样。`/local-llm-config` 会检测你的 CPU 和 RAM，推荐合适的 Qwen2.5-Coder 尺寸，并使用 Ollama 拉取它，以便 模型在你的机器上运行；`/add-model-key` 会改为使用云模型；`/ml-config` 会训练 风险排序器。你可以从 `/` 菜单中选择任何命令。`/solve` 和 `/verify` 完全 无需模型即可证明 Bug，因此它们在任何设置完成之前就能工作。 通过 OpenRouter（或任何兼容 OpenAI 的端点）引入模型，以猎取新代码中的漏洞： ``` export SABBA_LLM_BACKEND=openrouter export OPENROUTER_API_KEY=... # from openrouter.ai/keys sabba hunt cwe122_heap_overflow --model qwen/qwen-2.5-coder-32b-instruct ``` 密钥从环境中读取，从不存储在仓库中，并且 pre-commit hook 会拦截 任何看起来像凭据的内容（参见 [CONTRIBUTING.md](CONTRIBUTING.md))。 ## 工作原理的深入解析 - [docs/SABBA_AGENT_DESIGN.md](docs/SABBA_AGENT_DESIGN.md) - C 和 C++ Bug 查找器： 预言机、检索、Z3 合成器和推理代理。 - [docs/PROVERS_MULTI_DOMAIN_DESIGN.md](docs/PROVERS_MULTI_DOMAIN_DESIGN.md) - 预言机如何 泛化为 prover 注册表，包括 Web3 和 Solidity。 - [docs/PROVER_SOUNDNESS.md](docs/PROVER_SOUNDNESS.md) - harness-untrusted 验证 模型，它使得 fuzzing prover 能够对抗恶意的 harness 保持可靠性。 - [docs/WATER_LAYER_DESIGN.md](docs/WATER_LAYER_DESIGN.md) - 下一层：一个将 其技能保持为可运行代码的代理，无需前沿模型即可运行，并且可以从 种子重建。Prover 是它积累的技能。 ## 状态 原生预言机、检索、Z3 合成、推理代理，以及涵盖 C/C++、Solidity/EVM、Python、Go、Java 和 Node 的完整 prover 注册表 现均已推出，且每个都有实时的证明。 Water Layer 和更广泛的符号执行阶段将是接下来的内容。 ## 许可证 Apache-2.0。请参见 [LICENSE](LICENSE)。该框架是开源的。训练好的模型权重和 数据集是独立开发的，不属于本仓库的一部分。

标签：AI编程助手, AI风险缓解, Maven, MCP Server, MITM代理, 漏洞验证, 逆向工具