--- title: CTF 逆向工程：DownUnderCTF flag 检查器 — REA url: https://rea.tools/zh-CN/showcase/ctf/ --- [首页](https://rea.tools/zh-CN/) / [案例展示](https://rea.tools/zh-CN/showcase/) /CTF 案例研究 · DownUnderCTF 2023 # 在一个 CTF 二进制文件中 找到 flag。 用 REA 分析这个小型 flag 检查器，把它的规则转成方程，找出能让原程序打印 `Correct!` 的输入。 掩码方格 flag 检查器 · 简单 · Linux x86-64 [查看原始挑战](https://github.com/DownUnderCTF/Challenges_2023_Public/tree/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker) 从二进制文件到经过验证的答案 1. 01 · 找到检查 **字符串→检查函数** REA 查找提示、其引用以及接受或拒绝输入的代码。 2. 02 · 提取规则 **36 个字符 · 26 个求和式** REA 返回每项检查背后的指令和数据。编程助手把它们转化为方程。 3. 03 · 求解并运行 **还原出的 flag → 正确！** 一个 Python 脚本解出这些方程。REA 捕获到原程序接受该结果。 该挑战由 joseph 编写，发布在 DownUnderCTF 的官方仓库中。 ## 查找检查代码 题目附件是一个 15 KB 的可执行文件。它要求输入一个 flag，然后打印 `Correct!` 或 `Incorrect!`。先向你的编程助手发出一个简单的请求。 你的编程助手 使用REA分析ms_flag_checker并找到标志。 解释检查是如何工作的，然后用原始程序验证答案。 一个示例提示，题目已下载到本地，并连接了原生分析提供程序。 1. #### 从输入提示追踪到对应函数 编程助手→ REA ``` open_binary {"path": "ms_flag_checker"} search_strings {"pattern": "flag|correct|wrong|input", "mode": "regex", "case_sensitive": false} xrefs {"address": "0x102004"} resolve_containing_procedure {"address": "0x10126d"} ``` REA →编程助手 · 选定结果 ``` 0x102004 "What is the flag? " 0x10201c "Incorrect!" 0x102027 "Correct!" Prompt referenced at: 0x10126d Containing function: 0x10124d ``` 这条引用为编程助手提供了调查入口，即使可执行文件的原始函数名已被移除。 2. #### 阅读检查器及其两个辅助函数 编程助手→ REA ``` analyze_function {"procedure": "0x10124d"} analyze_function {"procedure": "0x101189"} analyze_function {"procedure": "0x101217"} ``` REA → 编程助手 · 选定指令 ``` 0x1012c1: CMP EDI, 0x24 0x1012c6: LEA RBX, [0x1040e0] 0x1012cd: LEA RBP, [0x104060] 0x1012d4: LEA R13, [RBX + 0x270] 0x1012e1: CALL 0x00101189 0x1012ec: CALL 0x00101217 0x1012f1: CMP dword ptr [RBP], EAX 0x1012f4: JNZ 0x00101335 0x1012f6: ADD RBX, 0x18 ``` 第一个循环复制36个字符代码。 检查循环解码掩码，对所选代码求和，并将结果与存储的数字进行比较。 它以 `0x18` 字节为步长跨越 `0x270` 字节，得到 26 个掩码。 以下是从一次全新 REA 分析中选取的结果。本地目标路径为显示而做了缩短；地址对应 REA 导入的内存映像。 ## 一次检查揭示一个字符 检查器把输入排列在 6×6 网格中。掩码决定哪些单元格参与求和。它的紧凑编码用负数跳过单元格，用正数选中它们。 ![第七个掩码跳过21个单元格，选择位置21，然后跳过14。 只有该单元格贡献总和。 它所需的字符代码是55，这意味着字符是7。](https://rea.tools/assets/localized/zh-CN/figures/ctf-mask-equation.svg) 第七个检查只选择一个位置。 [打开图](https://rea.tools/assets/localized/zh-CN/figures/ctf-mask-equation.svg). ### 从二进制文件中读取掩码及其目标 编程助手→ REA · read_bytes ``` {"address": "0x1040e0", "length": 624} {"address": "0x104060", "length": 144} ``` REA → 编程助手 · 结果中的第七个条目 ``` Mask at 0x104170: eb 01 f2 00 → -21, +1, -14, stop Target at 0x104078: 37 00 00 00 → 55 ``` 指令 `MOVSX` 会把掩码字节按有符号值读取。这就是 `eb` 表示 −21 的原因。目标是一个小端整数。这些字节一起告诉编程助手 `code[21] = 55`，因此该字符是 `7`。 ## 从指令到可读的检查 选择一个步骤，把求和辅助函数及其调用方对应到 C 中的同一条规则。 REA · 选取的原始指令 ``` 0x10121c: MOV ECX, 0x0 0x10122c: CMP dword ptr [RSI + RAX*0x1], 0x0 0x101230: JZ 0x00101223 0x101232: ADD ECX, dword ptr [RDI + RAX*0x1] 0x101223: ADD RAX, 0x4 0x1012f1: CMP dword ptr [RBP], EAX 0x1012f4: JNZ 0x00101335 ``` 可读的 C · 单次检查摘要 ``` int check_one_mask(const int codes[36], const int mask[36], int target) { int total = 0; for (int i = 0; i < 36; ++i) { if (mask[i]) { total += codes[i]; } } return total == target; } ``` **01 · 从零开始。** `ECX` 保存当前的累加和。 **02 · 检查掩码单元格。** 零值表示跳过该字符，非零值表示将其计入。 **03 · 添加字符代码。** 输入在相同偏移量处的整数被添加到总和中。 **04 · 移动到下一个单元格。** 原始循环每处理一个整数前进 4 字节，遍历 6 行、每行 6 个单元格。 **05 · 与存储的目标值比较。** 调用方在 `EAX` 中得到总和，不匹配则跳转到 `Incorrect!`。 指令来自求和辅助函数及其调用方。C 版本是一份说明性摘要：使用有意义的命名，并将二维遍历改写为遍历 36 个单元格的单层循环。 ## 求解26个方程 大多数掩码会选中多个单元格。例如，第一次检查累加 16 个字符编码，要求总和等于 1441。这些相互重叠的选择构成方程，一个小型 Python 脚本即可一并求解。 Python · 求解器摘录 ``` from z3 import Int, Or, Solver, Sum, sat codes = [Int(f"code_{i}") for i in range(36)] solver = Solver() alphabet = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_{}" for code in codes: solver.add(Or(*[code == ord(c) for c in alphabet])) for code, char in zip(codes, "DUCTF{"): solver.add(code == ord(char)) solver.add(codes[-1] == ord("}")) for selected, target in checks: solver.add(Sum([codes[i] for i in selected]) == target) assert solver.check() == sat model = solver.model() print("".join(chr(model.eval(code).as_long()) for code in codes)) ``` Z3 是一个求解器，可以找到满足这些方程的值。此节选使用提取出的检查，并假定 flag 以 `DUCTF{…}` 为前缀，包含字母、数字、下划线和大括号。完整下载包含全部 26 个掩码及其目标值。 [下载完整的求解器](https://rea.tools/showcase/ctf/solve.py) ## 用原始程序检查答案 REA 的进程捕获记录了原始可执行文件接受已求得 flag 的过程。把某个被选中的字符从 `z` 改成 `y`，第一个总和就从 1441 变成 1440，程序随之拒绝该输入。 | 输入 | 观察到的输出 | 退出代码 | | --- | --- | --- | | 求解器得到的 flag | `Correct!` | 0 | | 改动一个字符 | `Incorrect!` | 255 | 显示恢复的标志和捕获的输出 REA · 原始程序输出 ``` What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa} Correct! ``` 解出该二进制文件的 flag 后核对：还原出的值也与主办方公布的题目元数据中的 flag 一致。 来源、目标身份和分析详细信息 2026 年 10 月 8 日完成了全新分析，并做了两次进程捕获，使用 REA 4.1.0 与 Ghidra 12.1.4，运行于 Linux x64。该二进制文件是一个去符号的 x86-64 ELF，大小为 15,248 字节。 原始可执行文件 · SHA-256 ``` dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae ``` 在阅读主办方的源码或解答之前，先用 REA 检查了字符串引用、函数和常量。Python 求解器与图示都是根据这些 REA 结果构建的。 [与主办方来源比较](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/src/ms_flag_checker.c) · [挑战元数据和标志](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/ctfcli.yaml) · [REA证据说明](https://github.com/morluto/rea/blob/main/website/evidence/ctf-masked-squares.md) ## 你自己试试吧 将原始挑战和求解器下载到一个文件夹中。 使用上面的提示与你的编程助手进行调查，或运行包含的脚本。 [下载原始挑战](https://raw.githubusercontent.com/DownUnderCTF/Challenges_2023_Public/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/publish/ms_flag_checker)[下载求解器](https://rea.tools/showcase/ctf/solve.py) 终端 · 解决和运行 ``` python3 -m venv .venv .venv/bin/python -m pip install z3-solver .venv/bin/python solve.py chmod +x ms_flag_checker ./ms_flag_checker ``` 脚本打印候选标志；将其粘贴到程序的提示符处。 解决需要Python和 `z3-solver`. 运行原始可执行文件需要Linux x86-64。 [配置 REA 以配合你的编程助手](https://rea.tools/get-started/)