用 REA 和 AI agent 解 CTF 逆向题：从 crackme 到可验证的 flag

让 AI agent 做一道简单的 CTF 逆向题，几分钟就能出结果，但它也可能信心满满地给你一个错的 flag。解决办法不是把提示词写得更花哨，而是换一套工作流：agent 的每个结论都要能追溯到二进制里真实存在的东西，最终答案要交给原程序本身来判定。

本文用 REA（morluto 维护的开源项目）演示这套工作流。REA 通过 MCP 给 agent 提供原生分析工具（字符串、交叉引用、函数档案、原始字节），以及一个能记录真实可执行文件输出的进程捕获工具。每个结果都带一个 Evidence ID，agent 的推理过程因此可以被核对。

适合谁读： 已经在用 Claude Code、Cursor 或 Codex 的 CTF 选手和学生，想用 agent 做 rev 题、又不想盲目相信它。

你会学到：

自己动手写一道可以合法练习的 crackme
agent 从一个字符串走到校验循环应该调用哪些工具、按什么顺序
怎样把读出来的字节变成求解脚本
怎样用 Evidence 和进程捕获验证 agent 的答案

思路和 REA 网站上的 DownUnderCTF masked-squares 案例一致，只是换成了一个你自己编译的小程序。

前置条件

REA 已接入你的 agent。 运行 npx rea-agents setup，确认改动后重启 agent。还没装的话，先看安装 REA 并接入 Claude Code / Cursor / Codex。
一个原生分析 provider。 本文用 Ghidra。REA 连接你已安装的 Ghidra 12.1.x 和完整 JDK，不会替你装 Ghidra 或 Java。按安装文档设置好路径后，检查就绪状态：
```
rea doctor --provider ghidra --json
```
Hopper 或 IDA 也可以。Ghidra 的详细配置见 REA + Ghidra 免费原生二进制分析。
最后一步验证需要 Linux 或 macOS。 进程捕获依赖原生 PTY；macOS 上还需要能通过 xcrun 调用 Apple 的 Swift 编译器。原生 Windows 不能捕获新进程，请在 WSL 里运行 Linux 版 REA。详见 process capture 文档。
C 编译器（clang 或 gcc）和 Python 3。

REA 面向 CTF、教学以及你拥有或已获授权分析的软件。运行题目程序就是以你当前用户的权限执行它，进程捕获并不是沙箱。开始前请先读项目的 DISCLAIMER.md。

第 1 步：写一道练习用的 crackme

用自己写的程序练习，好处是你事先知道正确答案，可以评判 agent 做得对不对，而不是只能祈祷它对。保存为 xor_gate.c：

#include <stdio.h>
#include <string.h>

#define FLAG_LEN 20

static const unsigned char expected[FLAG_LEN] = {
    0x45, 0x60, 0x5e, 0x3e, 0x34, 0x7c, 0x2a, 0x43, 0x2b, 0x40,
    0x14, 0x2b, 0x77, 0x39, 0x4c, 0x12, 0x16, 0x2f, 0x1a, 0x20,
};

static int check(const char *s) {
    if (strlen(s) != FLAG_LEN)
        return 0;
    for (int i = 0; i < FLAG_LEN; i++) {
        unsigned char c = (unsigned char)s[i];
        unsigned char key = (unsigned char)(0x37 + 3 * i);
        if ((unsigned char)((c ^ key) + i) != expected[i])
            return 0;
    }
    return 1;
}

int main(void) {
    char buf[64];
    printf("Password: ");
    fflush(stdout);
    if (!fgets(buf, sizeof buf, stdin))
        return 1;
    buf[strcspn(buf, "\r\n")] = '\0';
    if (check(buf)) {
        puts("Access granted");
        return 0;
    }
    puts("Access denied");
    return 1;
}

出题思路是典型的入门 rev 套路：

长度门槛：输入不是正好 20 字节就直接失败。
随位置变化的密钥：每个字符和 0x37 + 3*i 异或，单字节异或爆破行不通。
一个偏移：异或之后再加下标。逆运算时顺序很关键：先减，再异或。
一张存储表：20 个期望字节放在只读数据段里，agent 得自己去读。

编译并去掉符号，免得 agent 直接搜一个叫 check 的函数就完事：

clang -O0 -o xor_gate xor_gate.c
strip xor_gate

-O0 让循环在反编译结果里更好读。熟练之后可以换 -O2 重新编译，优化器可能展开或向量化这个循环，正好练习读不那么友好的输出。

最后把源码挪走，只让 agent 看到二进制。

第 2 步：给 agent 目标，不要替它规定方法

在 xor_gate 所在目录打开 agent，输入：

Use REA to analyze ./xor_gate and find the password. Explain how the check
works, cite the Evidence ID for each fact you rely on, and verify the answer
by running the original program with REA's process capture.

这段提示词刻意做了三件事：

点名用 REA，避免 agent 只凭 strings 的输出去猜。
要求每个事实附 Evidence ID，逼它把“观察到的”和“推断出的”分开。
把“完成”定义为原程序接受这个输入，而不是 agent 自己觉得对。

REA 还内置了 investigate_feature、trace_crash 等引导式 MCP prompt，可以当起点用；对 crackme 来说，上面这种直接的请求就够了。参见 MCP prompts。

第 3 步：跟着 agent 的工具调用顺序走

面对一个去了符号的二进制，一次靠谱的 agent 运行通常是下面这个顺序。工具名是 REA 的 MCP 工具，同时给出对应的 CLI 命令，方便你手动复现任意一步。

3.1 打开目标，找提示语

agent 先打开二进制，再搜像提示语或判定结果的字符串：

open_binary            {"path": "/absolute/path/to/xor_gate", "provider_id": "ghidra"}
search_strings         {"pattern": "password|granted|denied", "mode": "regex", "case_sensitive": false}

CLI 对应：

rea search /absolute/path/to/xor_gate "password|granted|denied" \
  --mode regex --provider ghidra --json

为什么这样做： 去符号的程序里，用户能看到的字符串是最快的切入点。Access granted 是你想让程序走到的地方，Access denied 是校验失败时的去处。

3.2 从字符串走到函数

xrefs                          {"address": "<address of \"Access granted\">"}
resolve_containing_procedure   {"address": "<address of the reference>"}

rea xrefs /absolute/path/to/xor_gate 0xADDRESS --provider ghidra --json

为什么这样做： 交叉引用告诉你哪条指令加载了这个字符串，resolve_containing_procedure 再把这条指令换算成函数入口和函数体范围。REA 网站的案例就是这样从 "What is the flag? " 找到位于 0x10124d 的校验函数的。

3.3 读调用者和校验函数

analyze_function   {"procedure": "<main-like function>"}
analyze_function   {"procedure": "<function called before the branch>"}

rea function /absolute/path/to/xor_gate 0xADDRESS --provider ghidra --json
rea decompile /absolute/path/to/xor_gate 0xADDRESS --provider ghidra --json

analyze_function 返回函数档案，包含伪代码、指令、调用和引用。在这道题里，agent 应该能找到：

输入长度和 0x14（20）的比较；
一个同时用来索引输入和数据表的循环计数器；
和一个由计数器算出来的值异或（0x37 + i*3，反编译器可能写成 i*3 + 0x37，也可能是逐次累加）；
异或之后加上计数器的 ADD；
和表中字节比较，不相等就跳到失败分支。

让 agent 为上面每一点引用具体指令，而不只是贴伪代码。反编译输出是一种解释，指令才更接近 CPU 真正执行的内容。

3.4 读表里的字节

伪代码会按地址引用这张表，agent 接着直接读取它：

read_bytes   {"address": "<table address>", "length": 20}

rea read-bytes /absolute/path/to/xor_gate 0xTABLE --length 20 --provider ghidra --json

为什么这样做： 反编译器有时把常量数组显示成字符串，有时遇到零字节就截断，有时又显示成有符号数。直接读原始字节就没有歧义了。REA 网站的案例里，正是这一步确认了 mask 字节 eb 代表 -21，因为代码用的是 MOVSX。

地址取决于编译器、平台和 provider，你看到的数值会和任何文章里的都不一样。这没关系，方法本身不依赖具体地址。

第 4 步：把规则写成求解脚本

根据函数档案和读出的字节，正向校验是：

((input[i] XOR (0x37 + 3*i)) + i) mod 256 == expected[i]     for i in 0..19

每一步都可逆，所以这道题用不上 Z3。先减下标，再用同一个密钥异或：

EXPECTED = [0x45, 0x60, 0x5e, 0x3e, 0x34, 0x7c, 0x2a, 0x43, 0x2b, 0x40,
            0x14, 0x2b, 0x77, 0x39, 0x4c, 0x12, 0x16, 0x2f, 0x1a, 0x20]

def key(i):
    return (0x37 + 3 * i) & 0xFF

flag = bytes(((e - i) & 0xFF) ^ key(i) for i, e in enumerate(EXPECTED))
# Re-run the forward check on the candidate before trusting it.
assert all(((c ^ key(i)) + i) & 0xFF == EXPECTED[i] for i, c in enumerate(flag))
print(flag.decode())

agent 写出这个脚本后，先检查两件事再接受：

常量来自 read_bytes 的 Evidence，而不是 agent 凭印象从伪代码里抄的。问它这张表对应哪个 Evidence ID。
脚本对候选答案重新跑了一遍正向校验。 逆运算里一个符号写反，照样能打印出一串像 flag 的东西，assert 能拦住这种情况。

如果题目的约束互相交叠，比如 DownUnderCTF 案例里的 26 个掩码求和，agent 就该改为列方程，交给 Z3 之类的求解器。那个案例把格式假设（DUCTF{...} 前缀和允许的字符集）和从二进制里观察到的约束明确分开。你也应该这样要求：如果 agent 加了一句“flag 大概以 rea{ 开头”，那是假设，不是 Evidence。

第 5 步：用 Evidence 验证，而不是看它多自信

agent 辅助解题和碰运气解题的区别就在这一步。

5.1 每个结论对应一个 Evidence ID

REA 每个工具结果都包含 evidence_id 和 normalized_result。让 agent 给你列一张表：

结论	工具	Evidence ID
成功提示字符串及其地址	`search_strings`	`ev_...`
引用它的函数	`xrefs`、`resolve_containing_procedure`	`ev_...`
长度 20、异或密钥、`+ i`、比较	`analyze_function`	`ev_...`
表中的 20 个字节	`read_bytes`	`ev_...`

REA 网站的案例的 evidence 笔记用的就是这种格式。如果某个结论 agent 给不出 Evidence ID，就当它没被验证。想查看之前的记录又不想拉取完整内容，可以让 agent 调用 get_evidence_bundle，传 detail: "summary"，再按 operation 过滤。

5.2 把观察、推断和未知分开

“循环和 0x37 + 3*i 异或”是根据指令做出的推断；“这个地址的表里是这 20 个字节”是观察；“程序没有其他校验”在 agent 读完所有通往成功分支的路径之前，都属于未知。REA 的 prompt 和结果也按这三类区分。agent 一旦把它们混为一谈，错误就容易漏过去。

5.3 运行原程序

静态分析告诉你代码“应该”做什么，进程捕获告诉你它“实际”做了什么。agent 会调用 capture_process_scenario，你也可以把下面内容保存为 scenario-pass.json：

{
  "executable": "/absolute/path/to/xor_gate",
  "working_directory": ".",
  "events": [
    { "type": "input", "at_ms": 250, "data": "rea{s1mple_x0r_gate}\r" }
  ],
  "timeout_ms": 5000
}

rea capture-process ./scenario-pass.json --json > capture-pass.json

捕获结果会记录终端输出、退出状态和清理情况。预期是 Access granted，退出码 0。

然后做一次反向对照：改掉一个字符（比如 } 前面那个字母），再捕获一次，写到 capture-fail.json。预期是 Access denied，退出码 1。REA 网站的案例也这么做：把一个 z 改成 y，观察到 Incorrect! 和退出码 255。反向对照能证明校验确实对你的输入敏感；没有它，一个什么都接受的程序也能“验证”你的 flag。

两个实用提示：

输出文件要和场景文件分开。shell 重定向会在 REA 读取输入之前就把输出文件清空。
rea compare-process-captures 会拒绝比较契约不同的两次捕获，而脚本化的输入正是契约的一部分。所以请分别查看两次捕获各自的输出和退出码，不要拿成功和失败两次去做 diff。

5.4 保存记录

导出会话，方便你自己、队友或 write-up 审阅者日后复查：

export_evidence_bundle   {"path": "/absolute/path/to/xor_gate-evidence.json"}

rea evidence-import /absolute/path/to/xor_gate-evidence.json

evidence-import 会校验这个 bundle。完整的 Evidence 模型、快照和版本对比，见 Evidence、快照与版本对比。

常见问题和排错

第一次 Ghidra 查询很慢，或者客户端超时。 REA 在第一次查询时才开始 Ghidra 的导入和自动分析。客户端超时只是不再等待，Ghidra 可能还在跑。大文件可以调高 REA_GHIDRA_STARTUP_TIMEOUT_MS，参见 Ghidra 首次查询期限。

报 ambiguous provider 错误。 有多个 provider 都支持这个目标。MCP 里给 open_binary 传 provider_id，CLI 里加 --provider ghidra。

字符串搜不到。 有些题在运行时拼字符串或者加密了字符串。改为搜索函数（rea search PATH main --kind procedures），从入口点开始看，或者找 strcmp、memcmp、puts 这类导入函数。

agent 给的 flag 在捕获里失败。 常见原因：有符号和无符号字节搞混；逆运算顺序错了（- i 应该在异或之前还是之后）；表里漏了结尾。让 agent 重新读相关指令和字节，并演示正向校验在它的候选答案上为什么失败。

二进制在“指挥” agent。 字符串、伪代码和终端输出都来自目标程序。出题人有时会埋一句“忽略之前的指令”之类的文字。REA 会把这类结果标记为不可信内容，agent 应该只把它当数据。如果 agent 因为程序里的某段文字就提议去运行或下载什么东西，立刻叫停。

macOS 上进程捕获失败。 确认 xcrun swift 能用。REA 要用它编译一个小的辅助程序，但不会替你装 Xcode 或 Command Line Tools。

比赛中能这么用吗？ 先看赛事规则对 AI 工具的规定。很多 CTF 允许使用，也有一些会限制。

下一步

深入练习 provider 部分：REA + Ghidra 免费原生二进制分析。
了解 Evidence bundle、快照和对比：Evidence、快照与版本对比。
挑战逻辑在 JavaScript 或网页里的题目：用 REA 追踪网站 API 调用。
对比 REA 与其他逆向 MCP：REA 与 GhidraMCP、IDA Pro MCP 对比。
完整读一遍 DownUnderCTF masked-squares 案例，并下载它的求解脚本。