在一个 CTF 二进制文件中
找到 flag。

查找检查代码

题目附件是一个 15 KB 的可执行文件。它要求输入一个 flag，然后打印 Correct! 或 Incorrect!。先向你的编程助手发出一个简单的请求。

一个示例提示，题目已下载到本地，并连接了原生分析提供程序。

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 网格中。掩码决定哪些单元格参与求和。它的紧凑编码用负数跳过单元格，用正数选中它们。

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

{"address": "0x1040e0", "length": 624}
{"address": "0x104060", "length": 144}

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 中的同一条规则。

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

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;
}

指令来自求和辅助函数及其调用方。C 版本是一份说明性摘要：使用有意义的命名，并将二维遍历改写为遍历 36 个单元格的单层循环。

求解26个方程

大多数掩码会选中多个单元格。例如，第一次检查累加 16 个字符编码，要求总和等于 1441。这些相互重叠的选择构成方程，一个小型 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 个掩码及其目标值。

用原始程序检查答案

REA 的进程捕获记录了原始可执行文件接受已求得 flag 的过程。把某个被选中的字符从 z 改成 y，第一个总和就从 1441 变成 1440，程序随之拒绝该输入。

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

你自己试试吧

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

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。