[原创]KCTF2026 第八题：亥子合辰·塔影迷楼-CTF对抗-看雪安全社区

# kctf2026 CrackMe08 Writeup

## 结论

正确输入：

```text
kanxue@2o26o8!@#
```

已经用原始未修改样本验证：

```text
EXIT=0
STDOUT:
Input:correct
```

输入长度为 16 字节，字符和为：

```text
sum("kanxue@2o26o8!@#") = 0x500
```

---

## 环境和文件说明

主样本是：

```text
kctf2026_CrackMe08.exe
```

最终使用的关键脚本：

- `audit_semantics.py`：轻量 Unicorn/Capstone 审计脚本。
- `field_probe.py`：确认大整数乘法归约块语义。
- `init_poly_model.py`：验证初始化段是有限域 Horner 多项式。
- `high_model.py`：验证两段 20 轮高层模型。
- `invert_model.py`：从 final sink 目标反推第一段入口状态。
- `solve_roots.py`：求有限域五次方程根并恢复输入。

---

## 输入处理

程序要求输入长度为 16。

主 checker 入口在：

```text
0x140004380
```

开头检查字符和：

```text
sum(input) & 0xffffff == [0x14000A010]
[0x14000A010] = 0x500
```

所以必须有：

```text
sum(input) = 0x500
```

输入字符域是 printable：

```text
0x21 <= ch <= 0x7e
```

随后按 base94 折叠成 128-bit 整数：

```python
N = 0
for ch in input:
    digit = ch - 0x21
    N = N * 94 + digit
```

即：

```text
digit[i] = input[i] - 0x21
N = (((digit[0])*94 + digit[1])*94 + ... + digit[15])
```

---

## Final Sink

最终校验位于：

```text
0x14000646D..0x14000665F
```

clean timing 下，最终需要满足的四个核心状态是：

```text
[rbp+0x30] = 0xB8FD0694401D3D03
[rbp-0x68] = 0x0C14DB1C20DD97A8
[rsp+0x70] = 0xACA5240A53FB78A6
r14        = 0x9A2789B6DE31C2DC
```

final sink 还计算两个 FNV-1a：

```python
def fnv_qwords(words):
    h = 0xCBF29CE484222325
    p = 0x100000001B3
    for word in words:
        for i in range(8):
            h = ((h ^ ((word >> (8 * i)) & 0xff)) * p) & 0xffffffffffffffff
    return h
```

其中：

```text
FNV_qwords([r12, r10, rbx, r14]) == 0xBC1E5EBE1E4EC0D4
FNV_qwords([n_lo, n_hi, r12, r10, rbx, r14]) == 0x6CD601B3049AA32C
```

但 clean timing 下，如果前四个核心状态命中，上面的 FNV4 自动成立。

同时 FNV6 可以化成一个必要条件：

```text
FNV_qwords([n_lo, n_hi]) == 0xC8A68671C59DD0AD
```

这个条件可以用来审计自洽性，但直接用 Z3 求这个前像很慢，不是最终突破口。

---

## 重要反调试/动态污染坑

一开始遇到过一个很关键的假矛盾：

污染环境下 RHS 是：

```text
rhs38=0x225DFB2792241AAB
rhs40=0x83F24099E13F956E
rhs48=0x3605D9B981C25F0E
rhs50=0x15C112331FD3C01A
rhs58=0xE3309A36C578A1EA
rhs60=0x26BEA30DCC77E77C
```

这时：

```text
FNV4(rhs38,rhs40,rhs48,rhs50) != rhs60
```

看起来像程序无解或建模错了。

真正原因是 `rdtsc` timing 检测污染：

```text
0x4675..0x46E9 使用 rdtsc 做时间差检查
0x46E9: or rbx, 0x20
```

Unicorn 执行太慢，会让这个 timing flag 被置位。`rbx` 后续进入表生成逻辑，导致 final RHS 整体污染。

处理方式：

```text
在 0x1400046ED 强制 rbx = 0
```

clean timing 后 RHS 变成：

```text
rhs38=0xB8FD0694401D3D03
rhs40=0x0C14DB1C20DD97A8
rhs48=0xACA5240A53FB78A6
rhs50=0x9A2789B6DE31C2DC
rhs58=0x6CD601B3049AA32C
rhs60=0xBC1E5EBE1E4EC0D4
```

并且：

```text
FNV4(rhs38,rhs40,rhs48,rhs50) == rhs60
```

这个修正非常关键。后续所有动态分析都必须使用 clean timing。

---

## 初始化段：N 到 Y

`0x4EE9..0x5900` 最终被化简为模有限域的 Horner 多项式。

模数：

```text
p = 2^127 - 39
```

常量：

```text
C0 = 0x21b3bde1acf9adfa471fb28461a53bb5
C1 = 0x191a3870ad3d941105f15a9c38aae874
C2 = 0x40c190e211322caa2f01797348f02c97
C3 = 0x1df732140b8a3ef758fd09bde0058a37
C4 = 0x3f0cb8512c6f88e47e5f164fb478aab5
```

语义：

```python
p = (1 << 127) - 39

Y = (C0 + N) % p
Y = (Y * N + C1) % p
Y = (Y * N + C2) % p
Y = (Y * N + C3) % p
Y = (Y * N + C4) % p
```

也就是：

```text
Y = (((((C0 + N)*N + C1)*N + C2)*N + C3)*N + C4) mod p
```

然后拆成第一段 20 轮入口：

```text
r9  = high64(Y)
r12 = low64(Y)
```

这个模型用多个输入对拍通过，例如：

```text
PPPPPPPPPPPPPPPP:
Y = 0x0cfe76e7f9f9568e8140229e9b40ed1f

QQQQQQQQQQQQQQQA:
Y = 0x43a9a1f40a6686e31492c28d56c690ee
```

---

## 20 轮状态机化简

两段 20 轮都使用同一个核心结构。

先确认了大量看似复杂的乘法归约块其实是：

```text
(A * B) mod (2^127 - 39)
```

其中固定乘数：

```text
A = 0x4d8a9e9343d415cb83a0a488ec8523fe
```

核心函数可以写成：

```python
MASK = (1 << 64) - 1
p = (1 << 127) - 39

def ror(x, n):
    return ((x >> n) | ((x << (64 - n)) & MASK)) & MASK

def subst(sbox, x):
    out = 0
    for shift in [56, 48, 40, 32, 24, 16, 8, 0]:
        out = ((out << 8) | sbox[(x >> shift) & 0xff]) & MASK
    return out

def F(sbox, a_hi, a_lo, b_hi, b_lo, xor_key):
    prod = ((((a_hi << 64) | a_lo) % p) * (((b_hi << 64) | b_lo) % p)) % p
    hi, lo = prod >> 64, prod & MASK
    t = ror(hi, 47) ^ b_lo ^ lo
    return (ror(t, 51) ^ subst(sbox, t) ^ xor_key) & MASK
```

虽然 `[rbp+0x60]` 的 256-byte S-box 不是置换，只有 166 个不同输出，但第一段整体是 Feistel 型可逆结构。

第一段每轮可以抽象为：

```text
R' = H(R, msg) ^ L
L' = H(R', msg ^ golden) ^ R
```

其中：

```text
golden = 0x9e3779b97f4a7c15
```

所以给定最终 `(L', R')` 可以倒推出上一轮 `(L, R)`。

---

## 从 Final Sink 反推入口 Y

final sink 要求第一段最终输出：

```text
L20 = [rbp+0x30] = 0xB8FD0694401D3D03
R20 = [rbp-0x68] = 0x0C14DB1C20DD97A8
```

利用第一段 20 轮的可逆结构，从 `(L20, R20)` 反推第一段入口：

```text
L0 = 0x1489375bba3fb8de
R0 = 0x4be831b0ad3a2d36
```

因此：

```text
Y = R0 || L0
  = 0x4be831b0ad3a2d361489375bba3fb8de
```

把这个入口再正向跑第二段，自动得到：

```text
[rsp+0x70] = 0xACA5240A53FB78A6
r14        = 0x9A2789B6DE31C2DC
```

这说明 final 四个目标闭合，不需要再分别求第二段。

---

## 求 N 和输入

现在只剩一个有限域五次方程：

```text
poly(N) = Y mod p
```

其中：

```text
Y = 0x4be831b0ad3a2d361489375bba3fb8de
```

用 SymPy 在有限域 `GF(p)` 上分解：

```text
poly(N)-Y
```

得到一个合法线性根：

```text
N = 0x00000174a5e1d4cf4f146e72f70092ac
```

把 `N` 转回 16 位 base94 digit，再加回 `0x21`：

```text
kanxue@2o26o8!@#
```

校验：

```text
digits_sum = 752
sum(chars) = digits_sum + 16 * 0x21
           = 752 + 528
           = 1280
           = 0x500
```

---

## 最终验证

用原始 exe，通过 stdin 输入：

```text
kanxue@2o26o8!@#
```

输出：

```text
Input:correct
```

退出码：

```text
0
```

---

## 弯路和耗时点

这题耗时主要不在最终数学难度，而在被动态污染和复杂指令形态误导。

### 1. 误信静态反编译视图

一开始过度相信静态视图里能直接看到完整校验逻辑，但真实 checker 是运行时解密出来的。仅靠静态反编译视图容易漏掉真实执行语义。

后面改成直接从原始 exe 解密 stage1/stage2，并用 Unicorn 跑真实路径，才避免继续被静态视图缺失误导。

### 2. 把 prehash 当主约束

`sub_140001070` 一度看起来像主校验的一部分。实际它只是另一个 16 字节 rolling hash，命中 `0x1111111111111111` 时改写 `[0x140008000]`。

曾经求到两个 prehash 命中样本：

```text
FDP\-ijif8b&h@?A
[Hu_Z!M9;NzM{'V@
```

其中第二个甚至满足 `sum=0x500`，但原始 exe 仍返回失败。原因是 `[0x140008000]` 和主 checker 使用的 `[0x14000A000/0x14000A008/0x14000A010]` 不是同一条关键链。

这个方向后来判定为诱导/环境 seed，不是最终约束。

### 3. `rdtsc` timing 污染

这是最大坑。

Unicorn 下 `rdtsc` 时间差异常，导致：

```text
0x46E9: or rbx, 0x20
```

被执行，污染后续表生成和 final RHS。

污染 RHS 下甚至出现：

```text
FNV4(rhs38,rhs40,rhs48,rhs50) != rhs60
```

这个矛盾容易让人误判为：

- 程序无解；
- final sink 理解错；
- 还有隐藏路径；
- FNV 模型错。

最终通过在 `0x46ED` 强制 `rbx=0`，clean RHS 变得自洽。

### 4. 固定 trace guided symbolic 是弯路

曾经尝试用 `P*16` 的 concrete block trace 引导符号执行，例如 `second_phase_guided.py`。

问题是不同输入会在中间分叉：

```text
0x5035/0x5038
0x5295/0x5298
0x538b/0x539f
...
```

所以 `P*16` trace 只是局部路径，不能当作全局路径约束。继续沿这个方向会让 solver 越来越大，而且语义假设不稳。

### 5. 直接 SMT 指令海不划算

`0x5930..0x646D` 看起来是大量 ARX/MBA/查表/乘法/条件跳转。直接把指令级 AST 喂给 Z3，60 秒仍没有有效输出。

真正原因是这里有明显高层语义：

```text
mod (2^127 - 39) 的有限域乘法
Feistel 型 20 轮结构
```

一旦识别出这些结构，问题从“大 SMT”变成：

```text
反推 20 轮 Feistel
解一个有限域五次方程
```

复杂度直接降下来了。

### 6. S-box 非置换造成误判

`[rbp+0x60]` 的 256-byte 表不是置换：

```text
len(set(sbox)) = 166
```

这会让人以为整轮不可逆。实际第一段是 Feistel 型，内部函数不需要可逆，整体仍然可以反推。

---

## 复盘结论

这个题不是靠暴力 solver 解出来的，关键是按 final sink 反推并做语义坍缩：

```text
input
  -> base94 N
  -> finite-field polynomial Y
  -> Feistel-like 20 rounds
  -> final sink compare
```

最终有效路线：

1. 找 final sink。
2. 修正 `rdtsc` timing 污染。
3. 化简 final RHS。
4. 识别 `mod (2^127-39)` 域乘法。
5. 抽出两段 20 轮高层模型并对拍。
6. 利用第一段可逆性反推入口 `Y`。
7. 解有限域五次方程 `poly(N)=Y`。
8. 转回 base94 输入。
9. 原始 exe 验证。

最终答案：

```text
kanxue@2o26o8!@#
```

正确输入：

已经用原始未修改样本验证：

输入长度为 16 字节，字符和为：

主样本是：

最终使用的关键脚本：

程序要求输入长度为 16。

主 checker 入口在：

开头检查字符和：

所以必须有：

输入字符域是 printable：

随后按 base94 折叠成 128-bit 整数：

即：

最终校验位于：

clean timing 下，最终需要满足的四个核心状态是：

final sink 还计算两个 FNV-1a：

其中：

但 clean timing 下，如果前四个核心状态命中，上面的 FNV4 自动成立。

同时 FNV6 可以化成一个必要条件：

这个条件可以用来审计自洽性，但直接用 Z3 求这个前像很慢，不是最终突破口。

一开始遇到过一个很关键的假矛盾：

污染环境下 RHS 是：

这时：

看起来像程序无解或建模错了。

真正原因是 rdtsc timing 检测污染：

Unicorn 执行太慢，会让这个 timing flag 被置位。rbx 后续进入表生成逻辑，导致 final RHS 整体污染。

处理方式：

clean timing 后 RHS 变成：

并且：

这个修正非常关键。后续所有动态分析都必须使用 clean timing。

0x4EE9..0x5900 最终被化简为模有限域的 Horner 多项式。

模数：

常量：

语义：

也就是：

然后拆成第一段 20 轮入口：

这个模型用多个输入对拍通过，例如：

两段 20 轮都使用同一个核心结构。

先确认了大量看似复杂的乘法归约块其实是：

其中固定乘数：

核心函数可以写成：

虽然 [rbp+0x60] 的 256-byte S-box 不是置换，只有 166 个不同输出，但第一段整体是 Feistel 型可逆结构。

第一段每轮可以抽象为：

其中：

所以给定最终 (L', R') 可以倒推出上一轮 (L, R)。

final sink 要求第一段最终输出：

利用第一段 20 轮的可逆结构，从 (L20, R20) 反推第一段入口：

因此：

把这个入口再正向跑第二段，自动得到：

这说明 final 四个目标闭合，不需要再分别求第二段。

现在只剩一个有限域五次方程：

其中：

用 SymPy 在有限域 GF(p) 上分解：

得到一个合法线性根：

把 N 转回 16 位 base94 digit，再加回 0x21：

校验：

用原始 exe，通过 stdin 输入：

输出：

退出码：

这题耗时主要不在最终数学难度，而在被动态污染和复杂指令形态误导。

一开始过度相信静态视图里能直接看到完整校验逻辑，但真实 checker 是运行时解密出来的。仅靠静态反编译视图容易漏掉真实执行语义。

后面改成直接从原始 exe 解密 stage1/stage2，并用 Unicorn 跑真实路径，才避免继续被静态视图缺失误导。

sub_140001070 一度看起来像主校验的一部分。实际它只是另一个 16 字节 rolling hash，命中 0x1111111111111111 时改写 [0x140008000]。

曾经求到两个 prehash 命中样本：

其中第二个甚至满足 sum=0x500，但原始 exe 仍返回失败。原因是 [0x140008000] 和主 checker 使用的 [0x14000A000/0x14000A008/0x14000A010] 不是同一条关键链。

这个方向后来判定为诱导/环境 seed，不是最终约束。

这是最大坑。

Unicorn 下 rdtsc 时间差异常，导致：

被执行，污染后续表生成和 final RHS。

污染 RHS 下甚至出现：

这个矛盾容易让人误判为：

最终通过在 0x46ED 强制 rbx=0，clean RHS 变得自洽。

曾经尝试用 P*16 的 concrete block trace 引导符号执行，例如 second_phase_guided.py。

问题是不同输入会在中间分叉：

所以 P*16 trace 只是局部路径，不能当作全局路径约束。继续沿这个方向会让 solver 越来越大，而且语义假设不稳。

0x5930..0x646D 看起来是大量 ARX/MBA/查表/乘法/条件跳转。直接把指令级 AST 喂给 Z3，60 秒仍没有有效输出。

真正原因是这里有明显高层语义：

一旦识别出这些结构，问题从“大 SMT”变成：

复杂度直接降下来了。

[rbp+0x60] 的 256-byte 表不是置换：

这会让人以为整轮不可逆。实际第一段是 Feistel 型，内部函数不需要可逆，整体仍然可以反推。

回复或点赞可查看完整内容

[招生]科锐逆向工程师培训(2026年11月13日实地，远程教学同时开班, 第57期)