本帖最后由 FZZZP 于 2026-7-31 15:28 编辑
下载下来之后他是没有后缀的，用win hex查看，文件前面的标识是elf文件，我在Windows平台没法运行，只能静态分析
elf标识
用ida-pro打开，搜索字符串，字符串也不多，可以看到有flag的格式，以及错误和正确的字符串，双击Right！然后交叉引用看一下
字符串
可以看到Right上面直接跟了一个_memcmp函数，两个值分别是s2跟s，其中一个应该就是跟flag相关的值，再往上看s2的值是两个8位的16进制串，实际上这里是把这两个串在栈里拼起来了
因为在
[Asm] 纯文本查看 复制代码
mov [rbp+s2],rax
mov [rbp+var_98],rdx
这里，这两个在栈上是相连的，而且下面的call指令edx的寄存器压入的值是10h，也就是十进制的16，刚好就是这两个串加起来的大小。
这两个值上面的函数是md5_final，推测应该是真正flag的md5值，跟我们输入的flag的md5值进行对比。接着往上找
交叉引用
还是md5相关的函数，继续往上找
md5
这里有flag的格式了，就是将4个值拼成这个格式，var_70是拼接之后的缓冲区地址，上面的四个地址应该就是我们的输入的地址了
flag格式
这块可以看到，我们的输入在var_104这个地方，然后把输入放进checker4这个函数，通过之后就到下面的拼接flag的函数了，所以类似的这个checker函数应该还有1、2、3，继续往上找
checker4
checker1
checker1
checker2跟3
checker2、3
现在主函数的脉络就清晰了，分别获取四个输入，然后进入对应的checker函数，如果符合输入就下一步，不符合就直接退出了，接下来就是检查这四个checker，看一下里面是怎么验证的
点进checker1，可以看到逻辑还是比较简单的，输入减去0x5294b771等于0x956438b9，这个逆着计算还是很好计算的
checker1内部
到checker2就稍微复杂一点了，但是分析还是挺好分析，这里就不细写了，感兴趣的可以看图里面的注释
checker2内部
然后就到checker3了，这个逻辑就复杂的多了，我只分析了一部分，后面就没往下看了，checker4更复杂，这样分析的话效率就太慢了
checker3内部-1
checker3内部-2
checker3内部-3
这里是反编译的结果，逻辑就是前面分析的那样，四个输入，检查完之后拼接起来计算MD5，然后用MD5的值进行比较输出，重点是四个checker函数的反编译，checker1跟checker2刚才通过汇编代码已经分析完了，但是checker3跟checker4还是太复杂了，所以看一下反编译之后的，能节省我们分析的时间
反编译1
反编译2
checker1的反编译：
checker1反编译
checker2的反编译：
checker2反编译
checker3的反编译：
checker3反编译
checker4的反编译：
checker4反编译
ida-pro已经帮我们把运算的逻辑理清了，我们的目标就是根据这些运算来求解出我们输入的未知数
下面是python代码：
[Python] 纯文本查看 复制代码
from z3 import Solver, BitVec, ULE, sat
def solve_checker1():
"""
┌──────────────────────────────────────────────────────────────┐
│ IDA 反编译: │
│ if ( a1 - 1385478001 == -1788593991 ) return 0; │
│ │
│ 纯算术，一步解出。这里用 Z3 仅作演示，实际手动算也行： │
│ a1 = 1385478001 + (-1788593991) │
│ = -403115990 → unsigned: 0xE7F8F02A │
└──────────────────────────────────────────────────────────────┘
"""
a1 = BitVec('a1', 32) # 32 位符号变量
# C 语言中 int 常量 -1788593991 在与 unsigned 比较时，
# 会隐式转为无符号：取低 32 位 → & 0xFFFFFFFF
target = (-1788593991) & 0xFFFFFFFF
s = Solver() # 新建求解器
s.add(a1 - 1385478001 == target) # 照抄反编译的等式
if s.check() == sat: # 有解
val = s.model()[a1].as_long() # 取出 a1 的值
print(f"[Checker1] a1 = {val} (0x{val:08x})")
return val
else:
print("[Checker1] UNSAT!") # 无解（不应出现）
return None
def solve_checker2():
"""
┌──────────────────────────────────────────────────────────────┐
│ IDA 反编译: │
│ if ( 3 * (a1 & 0x52E3F96B) │
│ - (a1 | 0xAD1C0694) │
│ - a1 │
│ == -477662227 ) return 0; │
│ │
│ 注意: 0xAD1C0694 == ~0x52E3F96B │
│ 编译器把 ~M 计算成了编译时常量，直接写死在指令里。 │
│ │
│ 这个 checker 其实也可以逐位分析手动解（见本文档末尾注释）， │
│ 但 Z3 直接求解更省事。 │
└──────────────────────────────────────────────────────────────┘
"""
a1 = BitVec('a1', 32)
M = 0x52E3F96B # 掩码
notM = 0xAD1C0694 # = ~M，编译时常量
target = (-477662227) & 0xFFFFFFFF # 有符号 → 无符号
s = Solver()
# 直接翻译反编译的表达式，Z3 的位运算符和 C 一模一样
s.add(3 * (a1 & M) - (a1 | notM) - a1 == target)
if s.check() == sat:
val = s.model()[a1].as_long()
print(f"[Checker2] a1 = {val} (0x{val:08x})")
# --- 验证：用 Python 原生运算重新计算一遍，确保无误 ---
# Z3 内部是位精确的，这里用 Python 的 & | 和 32 位掩码验证
actual = (3 * (val & M) - (val | notM) - val) & 0xFFFFFFFF
assert actual == target, f"验证失败: 0x{actual:08x} != 0x{target:08x}"
print(f" 验证通过 ✅")
return val
else:
print("[Checker2] UNSAT!")
return None
def solve_checker3():
"""
┌──────────────────────────────────────────────────────────────┐
│ IDA 反编译（Hex-Rays 把多条指令合并成了下面这个复杂表达式）: │
│ │
│ if ( a1 > 0x10000000 ) return -1; │
│ if ( -3 * (~a1 | 0xD68E3FE9) │
│ + 3 * ~(a1 | 0xD68E3FE9) │
│ + 4 * ((~a1 & 0xD68E3FE9) + 2 * ~(~a1 | 0xD68E3FE9)) │
│ + 10 * (a1 & 0xD68E3FE9) │
│ - (a1 ^ 0xD68E3FE9) │
│ == 622576829 ) return 0; │
│ │
│ 反汇编中大约是 50 条指令，编译器把 -3*(...) 展开成 │
│ shl + sub 的组合。这里直接用 Hex-Rays 合并后的式子即可。 │
└──────────────────────────────────────────────────────────────┘
"""
a1 = BitVec('a1', 32)
M = 0xD68E3FE9 # 唯一的掩码
target = 622576829 # 正数，无需转换
# 表达式 ─── 照抄反编译，括号对齐避免优先级错误 ───
expr = (-3 * (~a1 | M)
+ 3 * ~(a1 | M) # ~(a | M): 对或的结果取反
+ 4 * ((~a1 & M) + 2 * ~(~a1 | M)) # (~a&M): 取反后与
+ 10 * (a1 & M)
- (a1 ^ M)) # ^ 是 XOR
s = Solver()
s.add(ULE(a1, 0x10000000)) # 反汇编 0x12b4: jbe → a1 ≤ 0x10000000
s.add(expr == target) # 反汇编 0x1337: cmp + jnz → 表达式必须等于 target
if s.check() == sat:
val = s.model()[a1].as_long()
print(f"[Checker3] a1 = {val} (0x{val:08x})")
return val
else:
print("[Checker3] UNSAT!")
return None
def solve_checker4():
"""
┌──────────────────────────────────────────────────────────────┐
│ IDA 反编译 — 最复杂的一个，4 个不同的掩码参与运算: │
│ │
│ if ( a1 > 0x10000000 ) return -1; │
│ if ( 11 * (a1 ^ 0xAE7C284F) │
│ + 4 * (a1 & 0xAE7C284F) │
│ - (6 * (a1 & 0x5183D7B0) + 12 * ~(a1 | 0x5183D7B0)) │
│ - 5 * a1 │
│ - 2 * ~(a1 | 0x4EDA6B7C) │
│ - (a1 | 0xB1259483) │
│ + 3 * (a1 & 0x4EDA6B7C) │
│ + 4 * (a1 & 0xB1259483) │
│ - (-2 * (a1 | 0xB1259483)) │
│ == -639151222 ) return 0; │
│ │
│ ⚠️ 关键：这个约束在 a1≤0x10000000 范围内有 2 个解！ │
│ 需要结合 MD5 才能确定哪一个是真正的 flag。 │
│ │
│ 为什么会有多个解？类比哈希碰撞——不同的输入经过复杂运算 │
│ 后碰巧得到相同的 32 位结果。MD5 在这里充当了"二次验证"。 │
└──────────────────────────────────────────────────────────────┘
"""
a1 = BitVec('a1', 32)
M1 = 0xAE7C284F
M2 = 0x5183D7B0
M3 = 0x4EDA6B7C
M4 = 0xB1259483
target = (-639151222) & 0xFFFFFFFF # 负数 → 无符号 32-bit
# 表达式 ─── 照着反编译逐项翻译 ───
expr = (11 * (a1 ^ M1)
+ 4 * (a1 & M1)
- (6 * (a1 & M2) + 12 * ~(a1 | M2)) # 嵌套括号，注意外层是减法
+ (-5 * a1) # Python 里写 -5 * a1 也行，这里加括号防歧义
- 2 * ~(a1 | M3)
- (a1 | M4)
+ 3 * (a1 & M3)
+ 4 * (a1 & M4)
- (-2 * (a1 | M4))) # -(-2 * x) = +2*x，但保持和反编译一致
s = Solver()
s.add(ULE(a1, 0x10000000)) # 范围约束
s.add(expr == target) # 等式约束
# ─── 获取所有解 ───
# .check() 只返回一个解。想要全部解，需要"排除已找到的，再搜"。
solutions = []
while s.check() == sat and len(solutions) < 20: # 20 是安全上限，防止死循环
val = s.model()[a1].as_long()
solutions.append(val)
s.add(a1 != val) # 关键: 把已找到的值从解空间排除
print(f"[Checker4] {len(solutions)} 个解: {[f'0x{v:08x}' for v in solutions]}")
return solutions # 返回列表，让 main() 用 MD5 筛
# =============================================================================
# main — 组装 flag + MD5 筛选
# =============================================================================
def main():
import hashlib
c1 = solve_checker1()
c2 = solve_checker2()
c3 = solve_checker3()
c4_list = solve_checker4() # 可能多个解！
# 从 IDA 反编译 main() 的 0x15f5 处提取的期望 MD5:
# s2[0] = 0xCEC174DE78F9D5F2LL → 字节序: F2 D5 F9 78 DE 74 C1 CE
# s2[1] = 0xD23FCA6134F59F7ALL → 字节序: 7A 9F F5 34 61 CA 3F D2
# 合并: F2D5F978DE74C1CE7A9FF53461CA3FD2
expected_md5 = "f2d5f978de74c1ce7a9ff53461ca3fd2"
print()
print("=" * 50)
for c4 in c4_list:
flag = f"flag{{{c1:08x}-{c2:08x}-{c3:08x}-{c4:08x}}}"
actual = hashlib.md5(flag.encode()).hexdigest()
if actual == expected_md5:
print(f"✅ FLAG: {flag}")
print(f" MD5: {actual} ← 匹配程序内硬编码的期望值")
return flag
else:
print(f"❌ 淘汰: {flag} (MD5 不匹配)")
print("未找到匹配的 flag!")
return None
if __name__ == "__main__":
main()
通过网盘分享的文件：rechall.zip
链接: https://pan.baidu.com/s/1KtcbwB0CSj_d5NayyPMVIg?pwd=vjet 提取码: vjet | 
发表于 2026-7-31 15:25
|
发表于 2026-8-2 09:15
