CTF逆向工程：DownUnderCTFflag 检查器-REA

查找检查代码

讲义是一个15KB可执行文件。它要求一面旗帜，然后打印 Correct! 或 Incorrect!. 从一个简单的请求开始给你的编程助手。

你的编程助手

使用REA分析ms_flag_checker并找到标志。解释检查是如何工作的，然后用原始程序验证答案。

一个示例提示，下载的质询在本地可用，并连接了原生分析提供程序。

按照输入提示到其函数

编程助手→ 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

引用为编程助手提供了一个调查的地方，即使可执行文件的原始函数名已被删除。

阅读检查器和它的两个助手

编程助手→ 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。 — 第七个检查只选择一个位置。打开图.

从二进制文件中读取掩码及其目标

编程助手→ 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 持有运行总和。

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是一个求解器，可以找到满足这些方程的值。此摘录使用提取的检查，并假定 DUCTF{…} 用字母，数字，下划线和大括号标记。完整的下载包括所有26个面具和目标。

下载完整的求解器

用原始程序检查答案

REA的进程捕获记录接受已解决标志的原始可执行文件。更改一个选定的字符 z 到 y 使第一和1440而不是1441，并且程序拒绝它。

输入	观察到的输出	退出代码
解算者之旗	`Correct!`	0
一个角色改变了	`Incorrect!`	255

显示恢复的标志和捕获的输出

REA · 原始程序输出

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

恢复的值还与组织者发布的挑战元数据中的标志相匹配，在解决二进制后检查。

来源、目标身份和分析详细信息

在2026年10月8日使用REA4.1.0和Ghidra12.1.4在Linux x64上进行新的分析和两个过程捕获。二进制文件是一个剥离的x86-64ELF，15,248字节。

原始可执行文件 · SHA-256

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

在阅读组织者的源代码或解决方案之前，对字符串引用，函数和常量进行了检查。 Python求解器和图表是根据REA结果构建的。

与主办方来源比较 · 挑战元数据和标志 · REA证据说明

你自己试试吧

将原始挑战和求解器下载到一个文件夹中。使用上面的提示与你的编程助手进行调查，或运行包含的脚本。

下载原始挑战下载求解器

终端 · 解决和运行

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与你的编程助手

找到国旗一个CTF二进制文件。