r2SMT

针对 radare2 的 SMT 辅助不透明谓词反混淆与符号分析工具包

## 功能简介 `r2SMT` 会向一个 SMT 求解器询问二进制程序中的每个条件分支是否*真正*能够走向两个分支。无法做到的分支即为**不透明谓词**、**死分支**或**恒定条件**——这些都是典型的混淆手段。随后，该工具允许您注释或修补二进制文件以消除它们。 处理流程：`radare2 反汇编 → 带类型 IR → 向后切片 → SSA → Z3 → 结论`。 设计上与样本无关（无硬编码的家族指标）。支持的架构提升器：x86 / x86_64 / AArch64 / AArch32（包括 Thumb 模式）。 ## 安装 ``` # 从源码编译 — 链接 Z3，因此需先安装 libz3 # macOS： brew install z3 # Debian： apt-get install libz3-dev git clone https://github.com/seifreed/r2SMT.git cd r2SMT && cargo build --release ./target/release/r2smt version # 预构建版本（内置 Z3，无运行时依赖）— 支持 Linux/macOS，x86_64/aarch64 架构 curl -fL https://github.com/seifreed/r2SMT/releases/latest/download/r2smt-$(uname -s)-$(uname -m).tar.gz | tar -xz # 或通过 r2pm 安装 r2pm -ci r2smt ``` 需要系统 `PATH` 中有 `radare2` ≥ 6.1 版本。 ## 60 秒快速上手 ``` # 1. 存在哪些条件分支？ r2smt branches ./sample # 2. 求解所有分支并分类输出结果 r2smt solve ./sample # 3. 深入分析一个可疑地址 — 单行结论 r2smt at ./sample 0x401234 ``` `solve` 命令会为每个分支打印一行分类结果，例如： ``` 0x00401234 opaque_predicate AlwaysFalse high je → never taken 0x004012a0 dead_branch AlwaysTrue high jne → always taken 0x00401310 real_branch BothPossible high jg (genuine) ``` ## 使用示例 每个分析命令都接受 `--at <地址>` (单个分支)、`--function <地址>` (单个函数) 和 `--timeout-ms <毫秒>` (每个分支的求解器超时时间)。 **导出标准化的程序模型：** ``` r2smt analyze ./sample --dump-program --json program.json ``` **求解并导出报告以供分析：** ``` # 一次性生成 JSON 报告、可读 Markdown 以及 r2 注释脚本 r2smt solve ./sample --json findings.json --markdown findings.md --r2-script annotate.r2 # 同时发现真实分支与未知分支，为求解器分配更多时间 r2smt solve ./sample --include-real --include-suspicious --timeout-ms 5000 ``` **查看求解器的具体分析过程（分阶段）：** ``` r2smt slice ./sample --at 0x401234 # bounded backward data-flow slice r2smt lift ./sample --at 0x401234 # that slice lifted to IR r2smt ssa ./sample --at 0x401234 # IR after SSA renaming ``` **在活跃的 radare2 会话中进行标注：** ``` r2smt annotate ./sample --dry-run # preview r2smt annotate ./sample --min-confidence high --save-project triage # apply + save ``` …或在 r2 内部，针对光标下的分支： ``` [0x00401234]> #!pipe r2smt at "${R2_FILE}" $$ ``` **修补——始终有备份，且可逆：** ``` r2smt patch ./sample # plan only, writes nothing r2smt patch ./sample --apply --min-confidence high # backup + manifest + patch r2smt patch ./sample --rollback # restore originals from manifest ``` `--apply` 会写入 `<样本>.r2smt.bak` 和 `<样本>.r2smt.manifest.json` (包含修补前后的 SHA-256)；`--rollback` 会反向回放清单文件。 **扫描目录（每个样本一个独立的 r2 进程，结果汇总）：** ``` r2smt batch ./corpus --threads 8 --json corpus.json --markdown corpus.md ``` **深度探索——以下选项都是可靠的** (它们只会将结论扩展到 `BothPossible`，而不会捏造结论)： ``` r2smt solve ./sample --allow-memory --allow-calls --max-blocks 4 \ --unknowns-on-truncation --allow-join-merge --solver cvc5 ``` ## 结论与发现类型 | 结论 | 含义 | | :----------- | :----------------------------------------- | | `AlwaysTrue` / `AlwaysFalse` | 分支只能走向一个方向 → 属于混淆 | | `BothPossible` | 真实分支（真实的控制流） | | `Unsound` / `Timeout` | 切片不完整或求解器放弃 —— 不具有可操作性 | | 发现类型 | 备注 | | :--------------- | :--------------------------------------- | | `opaque_predicate`, `dead_branch`, `constant_condition` | 可操作；置信度 `high` (干净切片) → `medium` (部分未建模输入) → `unknown` | | `real_branch`, `suspicious_but_unknown` | 仅供参考信息 —— 需使用 `--include-real` / `--include-suspicious` 选项启用 | 默认情况下，修补操作仅作用于 `--min-confidence high` 的结论；降低此阈值需明确指定并自行承担风险。 ## 系统要求 - 从源码构建需要 Rust 1.85+ (edition 2024) - 系统 `PATH` 中需要 `radare2` ≥ 6.1 - Z3 (系统 `libz3`，或使用内置构建功能) ## 许可证 本项目根据您的选择采用 **MIT OR Apache-2.0** 双重许可 —— 详见 [LICENSE](LICENSE)。 - 作者：**Marc Rivero López** — [@seifreed](https://github.com/seifreed) - 支持：Buy Me a Coffee

标签：Hakrawler, radare2插件, Rust编程语言, SMT求解器, TLS抓取, 不透明谓词检测, 二进制分析, 云安全运维, 云资产清单, 代码混淆, 分支优化, 反混淆, 可视化界面, 常量条件分析, 恶意代码分析, 死分支识别, 符号分析, 软件安全, 逆向工程, 通知系统, 配置文件