DownUnderCTF / REA / EN
Turn a flag checker into solvable constraints
ENGLISH SUMMARY
Turn a flag checker into solvable constraints
Find checking functions in an introductory CTF binary, translate masks and sums into equations, and verify the result with the original program.
The question
Which constraints must an input satisfy to pass the checker?
The workflow
- Locate input handling and flag-checking functions.
- Derive constraints from masking and sum operations.
- Solve for an input and confirm it with the original program.
Findings & output
The official walkthrough follows function analysis through constraint solving to checking the resulting flag in the original binary.
Evidence scope
The result is limited to one introductory challenge, not a demonstration of automatically solving arbitrary complex programs.
中文摘要
把 flag 检查逻辑，变成可求解的约束
分析一个入门 CTF 程序，找到检查函数，把掩码与求和逻辑改写成方程，再用原程序核对答案。
调查的问题
检查器接受的输入必须满足哪些条件？
怎么做的
- 定位输入与 flag 检查函数。
- 根据掩码和求和运算构建约束。
- 求解输入，再交给原程序确认。
发现与产出
官方案例展示从函数分析到约束求解，并在原程序中验证得到的 flag。
证据范围
案例范围是一个特定入门挑战，不能作为任意复杂程序自动求解的证据。
Original sources / 原始来源
Checked / 核对 2026-10-12 · Official investigation / 官方调查