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

[原创]KCTF2026 第八题：亥子合辰·塔影迷楼

发表于: 2026-8-21 16:39 16

[原创]KCTF2026 第八题：亥子合辰·塔影迷楼

shuax

2026-8-21 16:39

# 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!@#
```

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

冰与火的战歌：Windows内核攻防实战高级班！从零到实战，融合AI与Windows内核攻防全技术栈，打造具备自动化能力的内核开发高手。

收藏・0

点赞・3

打赏