5 步破解密码
工作原理
不是暴力破解，不是 fuzzing——是解方程。16 字节输入有 2128 种可能，约束条件将其化简为 Z3 秒级求解的方程组。
argv[1] 变成 4 字节未知量：
BVS("argv1", 32)if (input[0] == 'P') → 一条路径加约束 byte0 == 0x50，另一条加 byte0 != 0x50到达目标的路径：
byte0==0x50 ∧ byte1==0x34 ∧ byte2^0x42==0x10 ∧ byte3+0x20==0x87Z3 的 CDCL 引擎毫秒级解出 →
P4RgTriton 后端：Concolic 混合执行
Ponce4Ghidra 内置两个引擎。angr 探索所有路径；Triton 沿一条具体路径执行，同时追踪符号状态——永远不会路径爆炸。
Triton 原理 — 指令级语义建模
Triton 将每条 CPU 指令翻译为数学表达式。没有中间表示——直接在 x86/ARM 机器码上建立 AST。
什么时候用哪个引擎
| 场景 | angr | Triton |
|---|---|---|
| 小函数，找密码 | 最佳 — 探索所有路径，保证找到 | 可用 — 但需要一个具体输入作为起点 |
| 大二进制，DRM key 派生 | 路径爆炸 | 最佳 — 沿一条 trace 走，不会爆炸 |
| 混淆代码（VM/白盒加密） | 约束爆炸 | 最佳 — 不需要"理解"代码 |
| 有 Frida trace | 无法回放 trace | 最佳 — 回放 trace 同时追踪符号状态 |
| 没有具体输入 | 最佳 — 从零开始 | 需要一个起始输入 |
| 想找所有可能的解 | 最佳 — 找到每条满足路径 | 一次一条路径（取反分支 + 重跑） |
真实测试：angr vs Triton
两个引擎在同一台机器上求解相同的二进制，使用 symbolize_function_argument：
| 二进制 | 输入大小 | angr | Triton | 胜出 |
|---|---|---|---|---|
test_crackme4 个字节比较，无 libc 调用 |
4 字节 | 0.18s ✓ | 0.065s ✓ | Triton 快 2.8 倍 |
test_license19 字节密钥，含 strlen、XOR、校验和 |
19 字节 | 3.65s ✓ | 超时 ✗ | angr |
为什么有差异？
Triton 胜出的场景：纯计算——没有路径分叉开销，直接指令→AST 翻译。对 check_password（4 个简单字节比较），快 3 倍。
angr 胜出的场景：函数调用了 libc（strlen、printf）——angr 自动用 SimProcedures 接管，而 Triton 试图执行真实指令（Mach-O 的 libc 桩没有加载）。对复杂的真实函数，angr 的 SimOS 层是决定性优势。
经验法则：默认用 angr。当 angr 在大函数上路径爆炸，或者你有 Frida trace 要回放时，切换到 Triton。
DRM 逆向工作流
Frida 采集运行时数据（密钥、I/O 样本）→ Ponce4Ghidra 分析算法（小函数用 angr，大函数用 Triton）→ unidbg 复现为独立服务。
功能特性
多解求解器
每个变量最多返回 5 个不同的解。密码可能有多个合法输入。
约束可视化
查看求解器收集的每一条约束。理解路径为什么可达——不只是"可达"。
Veritesting
循环边界智能路径合并。大型二进制不会路径爆炸。
Unicorn 引擎
不涉及符号变量的代码块通过 Unicorn 快速具体执行，仅在符号分支处切回符号执行。
会话持久化
跨 Ghidra 重启保存/恢复会话。Find/Avoid 目标和符号化命令不会丢失。
实时进度
探索过程中状态栏每秒更新：活跃路径数、已找到路径数、步数、耗时。
何时使用哪种符号化方式
| 方式 | 适用场景 | 速度 |
|---|---|---|
| Function Argument | 已知哪个函数负责校验输入。分析 .so 库。大型二进制。 | 快 |
| argv[N] | 程序从命令行读取输入。小型/简单二进制。需要完整程序上下文。 | 中等 |
| Register | 未知量是标量（int/long），不是缓冲区。 | 快 |
| Memory | 未知量位于已知固定内存地址（全局变量、结构体字段）。 | 快 |
经验法则：优先使用 Function Argument。只有需要完整程序执行上下文时才用 argv。
平台支持
| 格式 | 架构 | 状态 |
|---|---|---|
| Mach-O | x86_64 | 完整测试 |
| ELF | x86_64, ARM64, ARM32, MIPS | 已测试（静态链接） |
| Android .so | ARM64, ARM32 | 支持（延迟状态创建） |