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二進位制檔案。