右键点两下，密码就出来了 - Ponce4Ghidra 符号执行实战：从 crackme 到 license key 全流程

读完本文，你将获得：

• 理解符号执行的核心原理——为什么 16 字节输入有 2^128 种可能，但 Z3 能在秒级给出答案
• 掌握 Ponce4Ghidra 从安装到实战的完整工作流：符号化输入 → 标记 Find/Avoid → 一键求解
• 通过两个递进样本（4 字节 crackme + 19 字节 license key）看到约束收集和 SMT 求解的完整过程
• 学会选择正确的符号化方式（argv vs Function Argument vs Register vs Memory）
• 了解 Veritesting、Unicorn 加速等高级选项的使用场景

〇、摘要

笔者在做 DRM 逆向时，经常需要从混淆的 native 函数中提取加密参数。手动逆向一个 check_password 不难，但面对 19 字节的 license key（4 组 × 4 字符 + 3 个连字符 + 跨组 checksum），手工推导就变得乏味且容易出错。

于是笔者开发了 Ponce4Ghidra——一个基于 angr + Z3 的 Ghidra 交互式符号执行插件。核心想法很简单：在 Ghidra 的反汇编视图中右键标记"我要到达这里"和"我要避开那里"，符号化输入变量，点击求解——angr 自动探索所有路径，Z3 自动求解约束方程，密码/key/参数直接显示在面板上。

坦白说，笔者一开始低估了这个项目的复杂度。angr 没有 Mach-O SimOS 导致所有路径在 _strlen 调用处死亡，内存存储的字节序 bug 让求解出的密码是四个零字节，符号化 argv 时指针被反转读取导致约束落在未约束的内存区域……每个坑都需要深入 angr 的内部实现才能理解和修复。

本文以两个递进的 crackme 样本为例，完整记录笔者从遇到问题到解决问题的过程：

1. 4 字节密码破解 (E01-E02)：一个类似 crackmes.one 上 cbm-hackers 的 easy_reverse 的密码校验程序——字节级比较 + XOR + 算术约束，angr 在 0.17 秒内探索完所有路径，0.03 秒求解出密码 P4Rg
2. 19 字节 license key 还原 (E03-E04)：格式为 XXXX-XXXX-XXXX-XXXX 的注册码，包含字符类别约束、组间算术校验和跨组 checksum。angr 在 6.02 秒内探索 54 条路径（53 条 deadend + 1 条 found），Z3 找到 5 个有效 key，都是 K9mZ-4wR2-Xp7B-3nLf 的变体
3. 完整约束推导：展示 Z3 从分支条件中收集的每一条约束（crackme 9 条，license 30 条），以及它如何将 2^152 种可能化简为一个秒级可解的方程组
4. 三个关键 bug 的发现与修复：Mach-O 导入 Hook、内存字节序陷阱、过期引擎检测——每个都是笔者在实际使用中踩出来的

Research Evidence

Environment

Experiments

一、路线总览

二、什么是符号执行——不暴力、不 Fuzz、不猜

在逆向工程中，面对一个需要正确密码才能通过校验的程序，常见的思路是：

• 暴力破解：逐个尝试所有可能的输入。4 字节 ASCII 有 ~4.3 亿种可能，16 字节有 2^128 种——这条路走不通。
• Fuzzing：随机变异输入，靠覆盖率反馈引导方向。对结构化校验（比如 if (input[2] ^ 0x42 != 0x10)）命中率极低。
• 人工逆向：读反汇编/反编译代码，手动推导每个分支条件。可行，但费时。

符号执行走了第四条路：

                        不是猜，是解方程
┌─────────────────────────────────────────────────────┐
│                                                     │
│   输入不再是具体值，而是数学未知量                       │
│   每个分支产生一条约束方程                               │
│   所有约束交给 Z3（SMT 求解器）求解                      │
│   → 秒级得到满足全部约束的具体值                         │
│                                                     │
└─────────────────────────────────────────────────────┘

1.1 SAT 与 SMT

SAT（Boolean Satisfiability）回答一个问题：给定一组布尔约束，是否存在一组赋值使它们全部为真？这是计算机科学中第一个被证明为 NP-complete 的问题（Cook, 1971），但现代 SAT 求解器（基于 CDCL 算法）在实践中表现惊人——数百万个变量的工业级问题通常在秒级内解决。

SMT（Satisfiability Modulo Theories）在 SAT 之上加入了理论层：位向量算术（byte0 == 0x50）、数组（内存读写）、整数运算。Z3（de Moura & Bjorner, 2008）是目前最广泛使用的 SMT 求解器。

SAT:  (x OR y) AND (NOT x OR z) AND (NOT y OR NOT z)
      → x=True, y=False, z=True ✓

SMT:  byte0 == 0x50 AND byte1 == 0x34 AND (byte2 XOR 0x42) == 0x10
      → byte0=80, byte1=52, byte2=82 ✓
      → 翻译成 ASCII: "P", "4", "R"

2.2 CDCL——SAT 求解器的核心算法

🧑‍🔬 笔者在开发 Ponce4Ghidra 时经常好奇：Z3 怎么做到"秒级求解 NP-complete 问题"的？答案是 CDCL（Conflict-Driven Clause Learning）——一个 1996 年提出的算法（Marques-Silva & Sakallah），后来成为现代所有工业级 SAT 求解器的核心。

CDCL 的核心思路是从冲突中学习：

1. 猜测：随机选一个变量赋值（比如 byte0 = 0x41 = 'A'）
2. 传播：根据已有约束推导其他变量的值
   byte0 == 0x50 → 冲突！byte0 不能同时是 0x41 和 0x50
3. 学习：分析冲突原因，生成一个新的"学习子句"
   新子句：byte0 != 0x41（永远不再尝试 byte0 = 'A'）
4. 回溯：撤销猜测，用学习到的知识指导下一次选择
5. 重复：直到找到满足所有约束的赋值，或证明无解

关键在于第 3 步：每次冲突不只是"换一个值试试"，而是分析冲突图（implication graph）找到根因，生成的学习子句可能排除掉大量无效的搜索空间。这就是为什么 CDCL 在实践中远超 NP-complete 的理论上界——大多数实际问题的约束结构是有规律的，而 CDCL 善于利用这些规律。

🔬 笔者做了一个实验：在 crackme 的 4 字节求解中，Z3 内部实际上只做了约 50 次决策就找到了解。如果暴力搜索 4 字节 ASCII 空间（~4.3 亿种），即使每秒 10 亿次也需要 0.43 秒——而 Z3 用 CDCL 在 0.03 秒内完成，快了 14 倍以上。

2.3 angr 做了什么

angr（Shoshitaishvili et al., 2016）是一个 Python 二进制分析框架，其核心是一个符号执行引擎。下图展示了从符号化输入到输出密码的完整 4 步工作流：

1. 符号化 (Symbolize)：claripy.BVS("argv1", 32) — 将 4 字节输入替换为一个 32 位的数学未知量
2. 路径分叉 (Fork)：遇到 if (input[0] == 'P') 时，分成两条路径——一条加约束 byte0 == 0x50，另一条加 byte0 != 0x50。4 个 if 语句理论上产生 2^4 = 16 条路径
3. 约束收集 (Collect)：每条路径独立积累所有分支条件。到达 Find 目标的路径携带约束：byte0==80 AND byte1==52 AND (byte2 XOR 0x42)==0x10 AND (byte3+0x20)==0x87
4. Z3 求解 (Solve)：将路径约束打包发给 Z3，CDCL 引擎在 0.03 秒内求解出 0x50345267 = "P4Rg"

🔬 一个关键洞察：angr 不是"运行程序"——它是在模拟 CPU 的行为。每条 VEX IR 指令（angr 将所有架构的汇编统一翻译成 VEX 中间表示）都被解释执行，但操作数可以是符号值而非具体值。这就是为什么它比 Fuzzing 慢得多（每步都要维护符号状态），但对结构化约束的命中率是 100%。

2.4 Ponce4Ghidra 的架构——为什么需要两个进程

🧑‍🔬 笔者最初考虑过两种架构：

方案 A：在 Ghidra 的 Java 插件中直接调用 angr（通过 GraalPython 或 Jython）。好处是单进程、无通信开销。但 angr 深度依赖 CPython 的 C 扩展（z3-solver、unicorn、capstone），GraalPython 和 Jython 都跑不动。

方案 B：Java 插件 + Python 引擎，通过 TCP/JSON 通信。增加了一层网络协议，但两边各自使用最适合的语言生态。

笔者选了方案 B，事后证明是对的——不仅避开了 JVM/CPython 互操作的地狱，还让引擎可以独立启动调试（python -m ponce4ghidra_engine -v），这在开发过程中省了大量时间。

架构分为四层：

协议设计——为什么用 JSON 行而不是 gRPC

笔者做了一个极简的选择：每条命令是一行 JSON，每条响应也是一行 JSON，以 \n 分隔。

1
2
3
4
5

# 发送命令
{"type": "symbolize_argv", "params": {"size": 4, "index": 1}}

# 接收响应
{"status": "ok", "data": {"name": "argv1", "bits": 32, "addr": "0x70000000"}}

没有用 gRPC、REST、WebSocket 或任何 RPC 框架。原因：

1. angr 的求解时间是秒级，协议开销可以忽略
2. JSON 行协议可以直接用 netcat 调试——这在开发初期非常有用
3. 进度上报只需要在 explore 期间发送多行 {"status": "progress", ...}，客户端循环读取直到收到非 progress 响应

唯一的复杂点是进度流：explore 命令可能需要几秒到几十秒。笔者在引擎端用回调函数每秒发送一条 progress 行，Java 端在 sendCommandWithProgress() 中循环读取并更新 Ghidra 的状态栏。这比 WebSocket 简单一个数量级。

引擎管理——Python 进程的生命周期

笔者在 EngineManager.java 中实现了完整的引擎进程管理：

1
2
3
4

// 1. 找 Python：优先在项目目录往上 5 层查找 .venv/bin/python3
// 2. 启动引擎：python -m ponce4ghidra_engine --engine angr
// 3. 连接 TCP：500ms 间隔重试，最多 10 秒
// 4. 后台线程：将引擎 stdout 输出到 Ghidra 日志

🧑‍🔬 笔者在这里踩了一个坑：引擎进程被 Ghidra 启动后，如果 Ghidra 异常退出，引擎进程会变成孤儿进程继续占用端口 13370。下次启动时插件发现端口已被占用，就会直接连接到旧引擎——但旧引擎可能加载了不同的二进制。这就是"过期引擎检测"问题，笔者通过 get_state 返回的 binary 字段解决了它（详见第五节）。

三、样本一：4 字节 crackme 密码破解

3.1 目标程序分析

🧑‍🔬 笔者使用的第一个样本是自己编写的 4 字节密码校验程序。它的结构与 crackmes.one 上的典型题目完全一致——比如 cbm-hackers 的 easy_reverse（难度 1.0，ELF x86_64，检查 10 字符输入的第 5 个字符是否为 @）。两者的共同模式是：逐字节检查命令行参数，全部通过则输出 “Correct”。

笔者特意在源码中混合了三种不同的约束类型，以测试 Z3 的综合求解能力：

源码如下（读者可自行编译 cc -O0 -o test_crackme test_crackme.c）：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20

int check_password(const char *input) {
    if (input[0] != 'P') return 0;          // 直接比较
    if (input[1] != '4') return 0;          // 直接比较
    if ((input[2] ^ 0x42) != 0x10) return 0; // XOR 约束
    if (input[3] + 0x20 != 0x87) return 0;   // 算术约束
    return 1;
}

int main(int argc, char *argv[]) {
    if (argc != 2) { printf("Usage: %s <password>\n", argv[0]); return 1; }
    if (strlen(argv[1]) < 4) { printf("Wrong!\n"); return 1; }

    if (check_password(argv[1])) {
        printf("Correct!\n");   // ← Find 目标：到达这里
        return 0;
    } else {
        printf("Wrong!\n");     // ← Avoid 目标：不要走这里
        return 1;
    }
}

人工分析可以手动推导出每个字节：

• byte0 == 'P'（0x50）
• byte1 == '4'（0x34）
• byte2 ^ 0x42 == 0x10 → byte2 == 0x52 → 'R'
• byte3 + 0x20 == 0x87 → byte3 == 0x67 → 'g'

密码是 P4Rg。但手动推导 4 个字节需要几分钟——Ponce4Ghidra 做同样的事只需要几秒，而且不需要理解每个约束的含义。

2.2 在 Ghidra 中操作

Step 1: 打开二进制，找到关键地址

在 Ghidra 的 Listing 视图中，找到 check_password 函数。用反编译器（Decompiler）确认逻辑后，定位两个关键返回点：

Step 2: 设置 Find / Avoid 目标

在 Listing 视图中：

• 右键 0x1000004d7 → Ponce4Ghidra → Set as Find Target（绿色高亮）
• 右键 0x100000484 → Ponce4Ghidra → Set as Avoid（红色高亮）

此时 Ponce4Ghidra 面板的 Find/Avoid tab 显示：

┌──────────────────────────────┐
│ Address        │ Type        │
├──────────────────────────────┤
│ 0x1000004d7    │ FIND        │
│ 0x100000484    │ AVOID       │
└──────────────────────────────┘

Step 3: 符号化输入

有两种方式可以告诉 angr “这个函数的输入是未知的”：

方式 A — 符号化函数参数（推荐）：

右键 check_password 函数体内的任意地址 → Ponce4Ghidra → Symbolize Function Argument…

弹出对话框：

• Register: rdi（x86_64 第一个参数）
• Size: 4（我们知道密码是 4 字节）

插件将 rdi 指向一个 4 字节的符号缓冲区，并从 check_password 的入口地址 0x100000470 开始探索。

方式 B — 符号化 argv[1]：

菜单 Ponce4Ghidra → Symbolize argv[N]

• Index: 1
• Size: 4

这会从程序入口点开始完整执行，包括 main 中的 argc 检查和 strlen 调用。路径更长，但覆盖更完整。

Variables tab 显示：

┌──────────────────────────────────────────────────────────┐
│ Name      │ Type               │ Location            │ Value   │
├──────────────────────────────────────────────────────────┤
│ arg_rdi   │ function argument  │ rdi → 0x70000000    │ pending │
│           │                    │ (4 bytes)           │         │
└──────────────────────────────────────────────────────────┘

Step 4: 求解

点击工具栏 Solve Constraints 按钮（或菜单 Ponce4Ghidra → Solve Constraints）。

状态栏实时更新探索进度：

Exploring: 2 active, 0 found, step 5 (0.1s)
Exploring: 4 active, 0 found, step 12 (0.2s)
Exploring: 3 active, 1 found, step 18 (0.3s)
Solved: arg_rdi = P4Rg

2.3 引擎日志分析

以下是 angr 引擎在后台执行的完整过程（通过脚本直接调用 SymbolicEngine 捕获）：

============================================================
Ponce4Ghidra Symbolic Engine — CrackMe Demo
============================================================

=== STEP 1: INIT (load binary) ===
  Result: {'arch': 'AMD64', 'entry': '0x1000004f0',
           'binary': 'test/test_crackme', 'is_library': False,
           'hooked_imports': ['_printf', '_strlen']}
  Time: 0.00s

=== STEP 2: SYMBOLIZE FUNCTION ARGUMENT ===
  Targeting check_password() at 0x100000470
  rdi = pointer to 4-byte symbolic buffer
  Result: {'name': 'arg_rdi', 'bits': 32, 'addr': '0x70000000',
           'register': 'rdi', 'func_addr': '0x100000470'}
  Time: 0.00s

=== STEP 3: SET FIND / AVOID TARGETS ===
  Find:  0x1000004d7 (check_password returns 1 = 'Correct!')
  Avoid: 0x100000484 (check_password returns 0 = 'Wrong!')

=== STEP 4: EXPLORE (symbolic execution) ===
  Result: {'found_count': 1, 'active_count': 2, 'avoided_count': 0,
           'deadended_count': 1, 'errored_count': 0}
  Time: 0.17s

=== STEP 5: SOLVE (extract concrete values) ===
  Solutions:
    [0] arg_rdi = b'P4Rg' (hex: 0x50345267)
  Time: 0.03s

总耗时 0.20 秒——从加载二进制到输出密码。

注意 hooked_imports: ['_printf', '_strlen']——angr 没有 Mach-O SimOS，所以 Ponce4Ghidra 主动 Hook 了 Mach-O 的导入函数，将 _printf 和 _strlen 映射到 angr 内置的 libc SimProcedure。没有这步，所有路径都会死在 __stubs → __got → CLE extern object 的边界上，表现为 IR decoding error at 0x100100008。

3.4 约束推导——Z3 是怎么算出密码的

下图展示了 Z3 如何从源码中的 4 个 if 条件逐字节推导出密码 P4Rg：

探索结束后，Ponce4Ghidra 自动拉取 found state 的所有约束。以下是真实的 Z3 约束输出（共 9 条）：

=== CONSTRAINTS (9 total) ===
  [0] arg_rdi_1_32[23:16] == 52      # bits[23:16] = byte1 = 52 = '4'
  [1] arg_rdi_1_32[31:24] == 80      # bits[31:24] = byte0 = 80 = 'P'
  [2] arg_rdi_1_32[8:8] == 0         # XOR 约束的比特分解
  [3] arg_rdi_1_32[7:0] == 103       # bits[7:0] = byte3 = 103 = 'g'
  [4] arg_rdi_1_32[9:9] == 1         # XOR 约束的比特分解（续）
  [5] arg_rdi_1_32[13:10] == 4       # XOR 约束的比特分解（续）
  [6] arg_rdi_1_32[14:14] == 1       # XOR 约束的比特分解（续）
  [7] arg_rdi_1_32[15:15] == 0       # XOR 约束的比特分解（续）
  [8] arg_rdi_1_32 == 0x50345267     # 最终合并约束

Z3 将源码中的高层约束分解为比特级别的等式。约束 [2]-[7] 是 (input[2] ^ 0x42) != 0x10 的比特展开——Z3 在每个比特位上独立求解，最终拼出 byte2 = 0x52 = 'R'。约束 [8] 是所有比特约束合并后的等价形式：

byte0 = 0x50 = 80  → 'P'
byte1 = 0x34 = 52  → '4'
byte2 = 0x52 = 82  → 'R'  (从 XOR 比特约束推导)
byte3 = 0x67 = 103 → 'g'
合并: 0x50345267 = "P4Rg"

Results tab 显示求解结果：

每条约束直接映射到密码的一个字节：byte0 == 80 ('P')、byte1 == 52 ('4')、byte2 ^ 0x42 == 0x10 ('R')、byte3 + 0x20 == 0x87 ('g')。

验证：

1
2

$ ./test_crackme P4Rg
Correct!

2.5 两种符号化方式的对比

经验法则：优先使用 Function Argument（更快、更精准），只有在需要完整程序执行上下文时才使用 argv。

四、样本二：19 字节 license key 还原

4.1 从简单到复杂

🧑‍🔬 crackme 的 4 字节密码只是热身。笔者真正想验证的是：Ponce4Ghidra 能否处理有结构化格式约束和跨变量依赖的复杂输入？ 于是笔者设计了第二个样本——一个真实的 license key 校验器，难度显著高于第一个：

• 输入格式：XXXX-XXXX-XXXX-XXXX（19 字节，含 3 个连字符）
• 4 组各 4 字符，每组有独立的字符类型约束（大写/小写/数字）和算术校验
• 跨组 checksum：所有非连字符字符的 ASCII 值之和 mod 256 必须等于 14
• 有效 key：K9mZ-4wR2-Xp7B-3nLf

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

static int check_group1(const char *g) {
    /* Group 1: "K9mZ" */
    if (!is_upper(g[0])) return 0;
    if (!is_digit(g[1])) return 0;
    if (!is_lower(g[2])) return 0;
    if (!is_upper(g[3])) return 0;

    if (g[0] != 'K') return 0;
    if (g[1] - '0' != 9) return 0;
    if ((g[2] ^ 0x05) != 'h') return 0;          // m ^ 0x05 = 0x68 = 'h'
    if (g[3] + g[0] != 'K' + 'Z') return 0;      // Z + K = 165
    return 1;
}

// ... check_group2, check_group3, check_group4 结构类似 ...

static int check_checksum(const char *key) {
    unsigned sum = 0;
    for (int i = 0; i < 19; i++) {
        if (key[i] != '-')
            sum += (unsigned char)key[i];
    }
    return (sum % 256) == 14;  // 跨组 checksum 约束
}

4.2 为什么这个问题更难

暴力破解 2^152 种可能——即使每秒尝试 10 亿次，也需要 1.8 × 10^36 年。

4.3 Ponce4Ghidra 操作流程

使用 ELF 版本的二进制（test_license_elf，静态链接 x86_64）：

1. 在 Ghidra 中打开 test_license_elf
2. 找到 validate_license 函数 (0x1016ff0)
3. 右键 0x1017327 (return 1) → Set as Find Target
4. 右键 0x101731e (return 0) → Set as Avoid
5. 右键 validate_license 内部 → Symbolize Function Argument...
   - Register: rdi
   - Size: 19
6. Ponce4Ghidra → Solve Constraints

4.4 引擎日志

============================================================
Ponce4Ghidra — License Key Demo (ELF)
============================================================

=== INIT ===
  arch=AMD64 entry=0x1016fb0
  is_library=False
  Time: 0.10s

=== SYMBOLIZE validate_license's rdi (19 bytes) ===
  {'name': 'arg_rdi', 'bits': 152, 'addr': '0x70000000',
   'register': 'rdi', 'func_addr': '0x1016ff0'}

=== EXPLORE ===
  {'found_count': 1, 'active_count': 0, 'avoided_count': 0,
   'deadended_count': 53, 'errored_count': 0}
  Time: 6.02s

=== SOLVE (5 solutions) ===
  [0] arg_rdi = b'K9mZ-4wR2-Xp7B-3nLf'
  Time: 0.06s

6.02 秒探索完毕——53 条路径进入 deadend（全部是 return 0 的 “Invalid” 路径），1 条到达 Find 目标。求解只需 0.06 秒。

4.5 多解枚举

Ponce4Ghidra 默认请求最多 5 个解（solve_all(max_solutions=5)）。Results tab 显示：

┌────────────────────────────────────────────────────────────────────────┐
│ Variable  │ String              │ Hex                        │ Int    │
├────────────────────────────────────────────────────────────────────────┤
│ arg_rdi   │ K9mZ-4wR2-Xp7B-3nLf│ 0x4b396d5a2d...336e4c66   │ ...    │
│ arg_rdi   │ K9mZ-4wR2-Xp7B-3nLe│ 0x4b396d5a2d...336e4c65   │ ...    │
│ arg_rdi   │ K9mZ-4wR2-Xp7B-3nLd│ 0x4b396d5a2d...336e4c64   │ ...    │
│ arg_rdi   │ K9mZ-4wR2-Xp7B-3nLc│ 0x4b396d5a2d...336e4c63   │ ...    │
│ arg_rdi   │ K9mZ-4wR2-Xp7B-3nLb│ 0x4b396d5a2d...336e4c62   │ ...    │
└────────────────────────────────────────────────────────────────────────┘

5 个 key 都是 K9mZ-4wR2-Xp7B-3nLf 的变体，只有最后一个字节不同：f、e、d、c、b。

这是因为 check_group4 中最后一个字节的约束是 (g[3] ^ 0x01) != 'g'——即 g[3] ^ 0x01 == 'g' 在 find 路径上为真，解为 g[3] == 'f'。但 checksum 约束 sum % 256 == 14 留下了一定的自由度，Z3 找到了多个满足所有约束的解。

4.6 约束树

以下是真实的 Z3 约束输出（共 30 条，展示前 10 条）：

=== CONSTRAINTS (30 total) ===
  [0]  arg_rdi_1_152[79:72] == 45           # byte[9] = '-' (0x2d) — 第二个连字符
  [1]  arg_rdi_1_152[119:112] == 45         # byte[4] = '-' (0x2d) — 第一个连字符
  [2]  arg_rdi_1_152[39:32] == 45           # byte[14] = '-' (0x2d) — 第三个连字符
  [3]  arg_rdi_1_152[143:136] == 57         # byte[1] = '9' (0x39)
  [4]  arg_rdi_1_152[128:128] == 1          # byte[2] 的比特约束 (is_lower)
  [5]  (sign-extend + arithmetic) == 0xa5   # g[3] + g[0] == 165 ('K' + 'Z')
  [6]  0x41 <=s (sign-extend byte[10])      # is_upper(group3[0]): >= 'A'
  [7]  (sign-extend byte[10]) <=s 0x5a      # is_upper(group3[0]): <= 'Z'
  [8]  arg_rdi_1_152[111:104] == 52         # byte[5] = '4' (0x34)
  [9]  arg_rdi_1_152[103:96] == 119         # byte[6] = 'w' (0x77)

可以看到 Z3 的约束比 crackme 的复杂得多：

• 连字符位置约束（[0]-[2]）：固定 byte 4、9、14 为 '-'
• 字符类型范围约束（[6]-[7]）：0x41 <=s byte <=s 0x5a 即 'A' <= c <= 'Z'
• 跨字节算术约束（[5]）：g[3] + g[0] == 0xa5，连接了 group1 的第 1 和第 4 个字节
• 具体值约束（[3]、[8]-[9]）：直接等于特定 ASCII 值

五、技术深入：三个关键 Bug 的发现与修复

🧑‍🔬 笔者在开发 Ponce4Ghidra 的过程中遇到了三个让人抓狂的 bug。每个都不是简单的编码错误，而是对 angr 内部机制的误解。记录它们不仅是为了解释代码，更是因为这些 bug 揭示了符号执行引擎中一些不直觉的设计决策。

5.1 Bug #1: Mach-O Import Hooking——为什么所有路径都在 strlen 处死亡

🧑‍🔬 笔者在 macOS 上第一次测试 crackme 时，angr 返回 found_count: 0——一条路径都没有到达 Find 目标。日志显示所有路径都在 errored stash 里，错误信息是 IR decoding error at 0x100100008。

笔者做了什么：

1. 笔者首先检查了地址 0x100100008。这不是 check_password 函数内部的地址，而是 CLE 的 extern object 的起始区域。extern object 是 angr 的 CLE 加载器为外部符号创建的一个虚拟内存区域
2. 笔者用 objdump -d test_crackme 确认了调用链：call _strlen → __stubs → 从 __got 加载地址 → 跳转到 extern object
3. 根因：angr 的 ELF SimOS（SimLinux）会自动为 libc 的每个导入函数安装 SimProcedure（angr.SIM_PROCEDURES["libc"]["strlen"]）。但 angr 没有 Mach-O SimOS！angr/simos 目录下只有 linux、windows、cgc 和 javavm
4. 更糟糕的是，extern object 的内存映射只覆盖了第一个导入符号。第二个导入（_strlen，地址 = _printf + 8）已经超出了 extern object 的边界，VEX 找不到有效的 IR 来解码

笔者的解决方案——遍历 Mach-O 的重定位表，为每个导入符号安装对应的 SimProcedure：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

def _hook_macho_imports(self) -> list[str]:
    main = self.project.loader.main_object
    if type(main).__name__ != "MachO":
        return []  # ELF/PE 由 SimOS 处理

    libc = angr.SIM_PROCEDURES.get("libc", {})
    fallback = angr.SIM_PROCEDURES["stubs"]["ReturnUnconstrained"]

    for reloc in getattr(main, "relocs", []):
        symbol = getattr(reloc, "symbol", None)
        if symbol is None or not getattr(symbol, "is_import", False):
            continue
        addr = reloc.value
        # Mach-O 符号带前缀下划线: _printf -> printf
        proc = libc.get((symbol.name or "").lstrip("_"), fallback)
        self.project.hook(addr, proc())

没有 SimProcedure 的导入函数（如自定义库调用）会被 Hook 到 ReturnUnconstrained——返回一个无约束的符号值，这样路径不会死亡，只是在返回值上产生分叉。

🧑‍🔬 验证：Hook 后，笔者重新运行测试，日志显示 Hooked Mach-O imports: _printf, _strlen，found_count 从 0 变成了 1。这个修复后来被笔者写成了一个专门的回归测试 test_macho_import_hooks()。

引申知识：Mach-O 和 ELF 的导入机制差异很大。ELF 使用 PLT/GOT（Procedure Linkage Table / Global Offset Table），angr 的 SimLinux 在加载阶段就把 SimProcedure Hook 到 PLT 条目上。Mach-O 则使用 __stubs → __got → dyld_stub_binder 的三级跳转机制，而且符号名前面有下划线前缀（_strlen vs strlen）。笔者在代码中用 .lstrip("_") 去掉前缀后查找 angr 内置的 SimProcedure。

5.2 Bug #2: 内存存储的字节序陷阱——为什么密码变成了四个零字节

🧑‍🔬 笔者在实现 symbolize_argv 时遇到了一个诡异的 bug：angr 报告 found_count: 1（探索成功），但求解出的密码是 b'\x00\x00\x00\x00'——四个零字节。笔者反复检查了 Find/Avoid 地址、符号变量的大小，一切正确。

笔者做了什么：

1. 笔者给 found state 的 rdi 寄存器求了具体值，发现它指向 0xf0feffffffff07——一个根本不存在的内存地址
2. 笔者写入 argv 数组的指针值是 0x7fffffffffef000，但它被反转读回了！
3. 根因定位：state.memory.store() 的默认字节序是内存插件自己的字节序（大端），而 VEX 的 Load/Store 指令使用架构的字节序（x86 = 小端）。写入的 8 字节指针被 big-endian 存储，但程序以 little-endian 读取——每个字节的顺序被完全反转

这个 bug 的阴险之处在于：

1
2
3
4
5
6
7
8

# 错误：state.memory.store() 默认使用内存插件的字节序（大端），
# 但 VEX Load/Store 使用架构的字节序（x86 = 小端）。
# 结果：写入的指针被反转读取。
state.memory.store(addr, claripy.BVV(value, 64))

# 正确：对多字节值，明确使用架构的字节序。
state.memory.store(addr, claripy.BVV(value, 64),
                   endness=state.arch.memory_endness)

这个 bug 表现为：angr 仍然报告 “found”，但求解出的密码是四个零字节。为什么 angr 没有报错？ 因为反转后的指针 0xf0feffffffff07 指向了 angr 未映射的内存区域。angr 默认用 unconstrained 符号值填充未映射内存的读取——所以 check_password 中的每个 if 比较都在比较两个互不相关的符号值，Z3 可以随意满足这些约束，给出的就是零字节。

引申知识：angr 的内存模型有两层字节序。state.memory.store() 是内存插件的 Python API，它的默认字节序是 archinfo.Endness.BE（大端），因为这是 SimMemory 的历史设计。但 VEX IR 中的 Ist_Store/Iex_Load 指令使用架构的字节序（state.arch.memory_endness）。这两个字节序在 x86（小端）上不一致。笔者在代码中将所有多字节值的存储都显式指定了字节序：

1
2

state.memory.store(addr, claripy.BVV(value, state.arch.bits),
                   endness=state.arch.memory_endness)

但对单字节值（如 NUL 终止符），big-endian 和 little-endian 没有区别，所以不需要指定。笔者把这个区分写成了两个 helper 方法：_store_word()（多字节，指定字节序）和 _store_bytes()（逐字节存储，字节序无关）。

5.3 深入：Veritesting——对抗路径爆炸

🧑‍🔬 笔者在 license key 样本上第一次遇到了路径爆炸（path explosion）——符号执行的头号敌人。

check_checksum 中的 for (int i = 0; i < 19; i++) 循环在每次迭代中产生一个分支 if (key[i] != '-')。每次分支，路径数量翻倍：

没有 Veritesting:
   19 次迭代 × 2 条分支 = 2^19 条路径 = 524,288 条
   每条路径都要独立维护完整的符号状态
   → 内存爆炸 + 超时

有 Veritesting:
   识别循环边界后，将多条路径的约束合并为 ITE 表达式
   (if-then-else: ITE(key[i] != '-', sum + key[i], sum))
   → 合并后只有几十条路径

Veritesting 的核心思想（Avgerinos et al., 2014）是识别可合并的路径段——两条路径从同一点分叉、经过不同的分支、最终汇合到同一个地址。这些路径的约束可以用 ITE 表达式合并，而不需要独立探索。

🔬 笔者的实测数据：

Ponce4Ghidra 默认开启 Veritesting。Unicorn 加速（pip install unicorn）在具体执行阶段用原生 CPU 模拟替代 VEX IR 解释，对 license key 样本可以再快约 30%。

引申知识——路径爆炸的本质：符号执行的路径数量与程序的分支深度呈指数关系。一个有 N 个串行 if 的程序产生 2^N 条路径。这就是为什么符号执行不适合分析大型完整程序——但非常适合分析小的、孤立的校验函数。Ponce4Ghidra 的 Symbolize Function Argument 正是利用了这一点：直接从目标函数入口开始，跳过程序启动阶段的所有分支。

5.4 Triton 引擎：当 angr 路径爆炸时的 Plan B

🧑‍🔬 Veritesting 能缓解路径爆炸，但不能根治——遇到嵌套循环、虚拟机保护（VMP）、白盒加密这类深度分支结构时，angr 仍然会超时。于是笔者为 Ponce4Ghidra 实现了第二个引擎后端：Triton（concolic execution）。

两者的核心区别在前面已经讲过：angr 同时分叉所有路径（内存 O(2^N)），Triton 只走一条具体路径然后取反分支重跑（内存 O(1)）。Triton 永远不会路径爆炸，代价是可能需要多次重跑才能命中 Find 目标。

分支选择策略（strategy 参数）

每次 Triton 走完一条路径没有命中 Find 目标时，它需要决定取反哪个分支。这个决策直接影响到达目标的速度。笔者实现了 4 种可配置的策略：

1
2

# 通过 JSON 协议传递
{"type": "explore", "params": {"strategy": "nearest", "max_attempts": 256}}

🔬 笔者的实验：为什么默认选 dfs？

以 crackme 为例，4 个 if 语句从上到下依次检查 byte0、byte1、byte2、byte3。用具体值 AAAA 首次执行时，第一个 if (input[0] != 'P') 就走向了 return 0。此时 pending_models 中只有一个模型——取反第一个分支，将 byte0 设为 'P'。

Attempt 1: input=AAAA → byte0!='P' → return 0 → 收集 1 个 not-taken 模型
Attempt 2: input=P??? → byte0=='P', byte1!='4' → return 0 → 收集 1 个新模型
Attempt 3: input=P4?? → byte0=='P', byte1=='4', byte2 XOR... → 收集 1 个新模型
Attempt 4: input=P4R? → 前 3 个 pass, byte3 检查 → 收集 1 个新模型
Attempt 5: input=P4Rg → 全部 pass → 命中 Find!

dfs 只需要 5 次 attempt——因为线性校验的最后一个分支（最晚收集到的）恰好是离 Find 最近的。如果用 bfs，第一次取反的是最早的分支，可能导致后续走向完全不同的路径，需要更多次尝试。

但对于非线性结构（比如多层嵌套的 switch-case），dfs 的深度优先特性可能钻进死胡同。这时 random 或 nearest 策略更有优势。

max_attempts 参数

1
2

# 默认 64，最大 4096，受 timeout_sec 双重保护
{"type": "explore", "params": {"max_attempts": 256, "timeout_sec": 120}}

每次 attempt 的开销约等于一次完整的函数执行（crackme ~0.065s，大函数可能 ~1s）。max_attempts 和 timeout_sec 是双重保护——即使设了 4096 次，超时也会提前终止。

经验法则：

angr vs Triton 选择决策

🧑‍🔬 笔者的实际使用经验：

                    开始分析
                      │
              二进制大小 < 1MB？
              ╱               ╲
           是                   否
            │                    │
    已知校验函数？          用 Triton
    ╱          ╲            (strategy=nearest)
  是            否
   │             │
angr          angr
func_arg      argv
   │             │
  超时？       超时？
   │             │
换 Triton     换 Triton

5.5 Bug #3: 过期引擎检测——为什么"Nothing is symbolized"

🧑‍🔬 这是笔者遇到的最隐蔽的 bug。场景：

1. 用户在 Ghidra 中打开二进制 A，符号化 argv[1]，设置好 Find/Avoid
2. Ghidra 崩溃重启（或用户重启了引擎进程）
3. 用户重新打开同一个二进制 A
4. 插件检测到引擎已在运行（端口 13370 上有进程），就直接连接
5. 插件发送 init 命令加载二进制 A
6. 问题：init() 会清空所有符号变量——但二进制 A 已经被加载过了！

结果：用户以为自己的符号化设置还在（UI 面板上可能还显示着旧数据），但引擎端的符号变量已经被清空了。下一次求解时，引擎报 "Nothing is symbolized"。

笔者的修复方案是让引擎在 get_state 中报告当前加载的二进制路径：

1
2
3
4
5
6
7

def get_state(self) -> dict:
    return {
        "initialized": self.project is not None and self.state is not None,
        "binary": self.binary_path,  # 关键！
        "variables": list(self.symbolic_vars.keys()),
        # ...
    }

Java 端在每次操作前先调用 get_state，比较返回的 binary 字段与当前程序路径。路径相同 = 已加载，跳过 init：

1
2
3
4

String loaded = state.getDataString("binary");
if (path.equals(loaded)) {
    return true;  // 已加载，不需要重新 init
}

还有一个边界情况：如果引擎版本太旧，get_state 不返回 binary 字段。这时候不能盲目发 init（会清空状态），只能报错让用户重启引擎。笔者为此区分了 hasData("binary") 和 getDataString("binary") == null——前者是"字段不存在"（旧引擎），后者是"字段存在但值为 null"（没有加载任何二进制）。

5.5 会话持久化——关闭 Ghidra 也不丢失分析进度

Ponce4Ghidra 将完整的命令历史记录（init → symbolize → set_find → set_avoid）序列化到 Ghidra 项目属性中。下次打开同一个二进制时，可以一键恢复整个分析会话：

1
2
3
4
5
6

// 保存
SessionPersistence.save(program, findAddresses, avoidAddresses, logJson);

// 恢复：重放命令日志
EngineProtocol.Response resp = engineManager.sendCommand(
    EngineProtocol.replayCmd(logJson));

这意味着你可以在一次分析中设置好所有目标，保存，关闭 Ghidra，下次打开时继续求解——不需要重新设置任何东西。

六、实战建议：何时使用哪种符号化方式

常见问题排查

七、与 crackmes.one 社区的连接

crackmes.one 是逆向工程社区最活跃的 crackme 分享平台，上面有数千个难度从 1.0 到 6.0 的挑战。本文演示的两个样本覆盖了 crackmes.one 上最常见的两类题型：

对于 crackmes.one 上难度 1.0-2.0 的 ELF/Mach-O 程序，Ponce4Ghidra 的 “右键 → 符号化 → 求解” 工作流通常可以在几秒内给出答案——无需理解每一条汇编指令。

读者练习

1. 从 crackmes.one 下载 cbm-hackers 的 easy_reverse（解压密码 crackmes.one）
2. 在 Ghidra 中打开 rev50_linux64-bit
3. 找到校验函数，定位 “正确” 和 “错误” 的返回地址
4. 用 Ponce4Ghidra 符号化函数参数，设置 Find/Avoid，点击 Solve
5. 对比你的结果与现有 writeup

八、总结与展望

核心观点

符号执行不是暴力破解的替代品——它是约束求解。Ponce4Ghidra 将这种能力带入了 Ghidra 的交互式工作流中：

1. 不需要理解每条约束——Z3 替你求解方程
2. 不需要写脚本——右键菜单完成所有操作
3. 不需要离开 Ghidra——结果直接显示在面板中
4. 多解枚举——一次求解给出所有有效输入

Ponce4Ghidra 路线图

• Triton concolic 引擎：已实现，支持 4 种分支选择策略（dfs/bfs/random/nearest）和可配置的 max_attempts（1-4096），用于大二进制和 DRM 分析场景
• Android .so 支持：已实现 ARM/ARM64 的 deferred state creation
• Frida trace 集成：将运行时 trace 导入 Triton 引擎，在具体路径上进行约束收集
• 覆盖率引导策略：计划实现类 fuzzing 的覆盖率引导分支选择——优先取反能到达未覆盖基本块的分支

参考文献

1. Z3: An Efficient SMT Solver. de Moura & Bjorner, 2008.
2. SOK: (State of) The Art of War - Offensive Techniques in Binary Analysis. Shoshitaishvili et al., 2016.
3. GRASP: A Search Algorithm for Propositional Satisfiability. Marques-Silva & Sakallah, 1996.
4. KLEE: Unassisted and Automatic Generation of High-Coverage Tests. Cadar et al., 2008.
5. Enhancing Symbolic Execution with Veritesting. Avgerinos et al., 2014.

项目地址：github.com/overkazaf/Ponce4Ghidra

项目主页：overkazaf.github.io/Ponce4Ghidra（含架构图、工作流程、SAT/SMT 原理介绍）