KCTF2026: 第三题：午时·永数囚笼 Writeup-CTF对抗-看雪安全社区

KCTF2026: 第三题：午时·永数囚笼 Writeup

发表于: 2026-8-13 00:43 763

KCTF2026: 第三题：午时·永数囚笼 Writeup

Magic丶

2026-8-13 00:43

763

# AntiAi — Writeup

**flag：`flag{v4_opaque_trace_2026}`**（26 字节）

```
$ printf 'flag{v4_opaque_trace_2026}' | ./AntiAi.exe
input flag: ok
$ printf 'flag{v4_opaque_trace_2027}' | ./AntiAi.exe     # 对照
input flag: no
```

样本：`AntiAi.exe`，PE32+ x64 console，18 432 B，`.vseal` 节魔数 `SEALVMTX`。
环境：WSL2 + unicorn 2.1.2 + capstone 5.0.7 + z3 + objdump（IDA、angr 均不可用）。

---

## 1. 程序结构

入口经 CRT 到真正的 main（`0x140002f2c`）：写提示串 → `ReadFile` 读 64 字节 → 去 CRLF →
`check@0x14000306c` → 按结果写 4 字节 `ok\r\n` / `no\r\n`。长度硬编码 26（`len ^ 0x1a` 须为 0）。

`check` 是四段式：

```
input[26] --expand_2ba0--> expanded[32]
          --block_330c(sel=0..3), 每个跑 32 轮 VM--> state[32] 各一份
          --lane finalize(ARX)--> out[sel]  (0x3c 字节 struct)
          --finalize_2940--> 4 dword  ==  TARGET
```

`TARGET = 892a48af b45dcd47 006c5ac3 b0b1062a`（`.text` 常量，输入无关）。
实机验证过成功条件本身：只把栈上 `out[]` 改成 TARGET，程序即输出 `ok\r\n`（edi=0）。

## 2. 三层防护

- **全 `.text` 自校验**：轮函数在 `0x140002780` / `0x1400027b9` 把 `0x140001000..0x140004bfb`
  （15 356 B）整段当数据读进哈希，一次 `check` 有 4096 + 512 次这样的读。任何 patch / 软件断点都会污染结果，
  包括目标常量表本身也被当普通代码字节吃进哈希。
- **全扩散**：改任一输入字节 → 四个 lane 的全部 state dword 与最终输出全变，GF(2) 上非仿射。
  无梯度、无爬山、无线性代数可用。
- **控制流伪装**：96% 的指令在一段输入无关的完整性扫描里；VM 分发看似数据相关，实际由 2 bit 选择子挑 4 个固定程序之一。

反调试与 rdtsc 探针在干净环境返回 0；仿真中 12 项完整性检查有 9 项恒为 0，说明节映射 / TEB / PEB / 种子忠实。

## 3. VM 还原：先定语义，再写反汇编器

**关键决策：不在 x86 层（约 170 万条指令）分析，先把每个 handler 的语义定死，写反汇编器把字节码翻成可读清单，再在清单上做数据流分析。**

结论：VM 只有 **4 个固定程序**，各 258 步 = 32 轮 × 8 步 + 2。选择子 `sel = (lane + ebx) & 3` 虽输入相关，
但输出槽 `out[sel]` 与目标行同步轮转、完全抵消 —— 程序 j 恒定产生 `out[j]`。
强制 sel 后，6 组不相干输入 × 4 lane 的逐步轨迹完全相同。

每轮固定骨架（`prog2.asm` 节选）：

```
; ==== round 2   pc=0x0188  r13=0xa9a2d15a  V34=0xc8fdf3c2  K=0x917e76bf ====
0188  op00  LOAD      A <- exp[P=0x08]                    ; P 由 (V34,r13,r12) 决定
0189  op10  CKSUM     cks = f(cks, K, pc, W)              ; 反篡改，无数据流
018a  op20  ALU20     A = rol8(A * 0x4d + 0xa7, 7) ^ RK   ; k1=7 M=0xa7 B=0x4d RK=0xc2
018b  op22  XORIN     A ^= rol8(exp[Q=0x03], 4)
018c  op13  STORE.RK  state[2] <- A ; r13 = rol32(LB*0x45d9f3b + r13 + (r12^0xa7), (r12%13)+5) ^ 0x9e3779b9
018e  op06  KEYREF    K,V34 <- refresh(K,V34,r13,r12,A)
018f  op07  JMP       pc <- 0x01a8 ; r12 -> 3
```

算子参数由取指字直接解码（`b1/b2/b3` 为取指字的三个字节）：

```
k1 = ((rol8(b3,2) ^ b1 ^ 0x9b) & 7) + 1
M  = ror8(b3,3) ^ b2 ^ 0xe1
B  = ((((b1^b3) * 2) ^ 0xb5) | 1)          # 恒为奇数 ⇒ mod 256 可逆
RK = ((r12*0x3d + 0x71) ^ r13 ^ (r13>>8) ^ (r13>>16)) & 0xff
```

| op | 前向 | 逆 |
|---|---|---|
| 18 | `A = rol8(A ^ RK, k1) + M` | `A = ror8(A - M, k1) ^ RK` |
| 19 | `A = ror8(A + M, k1) ^ RK` | `A = rol8(A ^ RK, k1) - M` |
| 20 | `A = rol8(A*B + M, k1) ^ RK` | `A = (ror8(A ^ RK, k1) - M) * B⁻¹` |
| 21 | `A = (ror8(A ^ RK, k1) - M) * B` | `A = rol8(A*B⁻¹ + M, k1) ^ RK` |
| 22 | `A ^= rol8(exp[Q], Qrot)` | 自逆 |

4 个程序共用同一组每轮常量 `alu/k1/M/B`；差异只在取指 pc 链、填充 op 和运行时状态。
XORIN 轮固定为 `r ∈ {2,3,12,13,14,15,22,23,24,25,26,27}`，`Q[2]=3, Q[3]=2, Q[22]=23, Q[23]=22` 为硬常量。

其余状态机：

```
r13' = rol32(LB*0x45d9f3b + r13 + (r12^0xa7), (r12 % 13) + 5) ^ 0x9e3779b9   # LB = 该轮载入的字节
K₀   = 0x31415926           # 只依赖编译期 seed，常量
r13₀ = 0xC0DEC0DE           # 常量
V34₀ = g(digest12(expanded))   # 唯一的输入耦合，只经 12 bit 摘要
```

## 4. 真正的机关

对 `r14`（错误累加器）逐个 OR 站点插桩后：在四个程序里，`r14` 的**唯一**非零来源是 `op0` 的
「重复 LOAD 下标」检查（`r14 |= seenP & (1<<P)`，掩码在 `rbp-0x69`）。即：

> **`r14 == 0` ⟺ 该 lane 的 32 次载入下标 `P[0..31]` 恰是 `0..31` 的一个排列。**

`P[r]` 由运行时状态 `(V34[r], r13[r])` 决定，随输入变化。400 个随机输入 × 4 lane 实测最好只覆盖 26/32 个槽；
随机撞上排列的概率 `32!/32³² ≈ 5×10⁻¹³`。这既是难点，也是反演时最强的剪枝。

真 flag 下四个 lane 的实际载入覆盖：

```
lane0 24/32   lane1 22/32   lane2 32/32 ✓   lane3 23/32
```

只有 lane 2 是完整排列 —— **另外三个 lane 是 decoy**（详见第 6 节）。

## 5. 反演

VM 每轮只 LOAD 一个 `expanded` 字节、STORE 一个 `state` 字节，中间全是可逆 8 bit 算子 ⇒
本质是「字节置换 + 逐字节可逆变换 + 12 处交叉 XOR」，可从目标 state 倒剥。三个支点：

1. **种子几乎全常量**：`r13₀` / `K₀` 是常量，唯一输入耦合 `V34₀` 只经 12 bit 摘要 ⇒ 枚举 4096。
2. **终态被钉死**：`r13_final` / `V34_final` 也是 `r14` 的组成项，通过态下必须等于静态表派生的每 lane 常量
   （`0x2160` / `0x2180` 派生）⇒ 直接 `finalize_inv` 得到 32 轮结束时的 raw state，
   **原本需要的 64 bit 不动点迭代被整个消掉**。
   ```
   sel : EXP_R13     EXP_V34
    0  : 0x17cac189  0xef8b64c2
    1  : 0x072183de  0xd520b1db
    2  : 0xe6a68d04  0x2e8c989c
    3  : 0x7247a3a0  0xecdc4e20
   lane2 raw state = 40e086d0ceff2d270de6e28bd49f57afbeb5316bd8322983820999bccb16ab1d
   ```
3. **expand 完全可逆且自带筛子**：前 24 字节直接进 E0..E5，E6 = `0xa55a0000 | b25<<8 | b24`，
   E7 = 常量 `0xc3d2e1f0`，之后 8 轮 ChaCha 式 QR 置换（全 `+/^/rot`，双射）。
   逆变换自带 **48 bit 合法性校验**（`E7 == 0xc3d2e1f0` 且 `E6>>16 == 0xa55a`），随机 32 字节 200/200 被拒。

**剥壳算法**：按轮号 0→31 前推，由 `(V34[r], r13[r])` 算 `P[r]/RK[r]/Q[r]`，
用 ALU 逆从 `state_raw[r]` 解出 `expanded[P[r]]`，再用该字节前推 `r13`、用累加器前推 `V34/K` —— 因果闭合，不循环。

唯一阻塞来自 `op22`：若 `exp[Q[r]]` 尚未解出，则一个方程两个未知；`Q[2]=3, Q[3]=2` 互指，阻塞是结构性的。
破法是**往回走**：`finalize_inv` 的 ARX 逆有一半与 `r13/V34` 无关，从被钉死的终态倒走过无 tap 的 31→28 轮，
只剩 **6 个候选**，每个候选一次性钉住 4 个 `expanded` 字节 + 一个 64 bit 锚点。

最终搜索用 C 实现（前向与 `vm_model.py` 位级一致）：4096 个 `d12` × 6 个候选，
排列约束 + 禁用槽掩码 + round-28 锚点剪枝，32 核约 45 M 节点/秒/核。
**在 `d12 = 272` 命中**，约 1.5×10¹² 节点、17 分钟墙钟。

```
expanded = f1b4801d0d18245b437c05da5b354020262485099321b50a6615bbd15e601d3f
unexpand → b'flag{v4_opaque_trace_2026}'
```

## 6. 两个被推翻的中间结论

**一、「目标表是 decoy」—— 错。**
某轮分析统计出「污染目标表的比较结果后，93.4% 的情况下最终输出不变」，据此判定该表是诱饵。
这把*结果*当成了*原因*：随机输入早在排列约束处已让 `r14` 饱和成 `0xffffffff`，比较表自然无影响。
后来用 z3 反解 `finalize_2940` 得到 TARGET 唯一要求的四个中间值
`REQ_Z = [1f1cc1bc, 1b7d21a2, 47d3d751, 27ff56e7]`，其中 lane 2 的通过态精确复现 `0x47d3d751`
—— 2⁻³² 巧合概率，反证该表为真。

**二、「四个 lane 都要通过」—— 也错。**
按此假设做四路同步剥壳（共享 `expanded`），在全部 4096 个 `d12` 上、带与不带排列约束，**0 解**（1.65 M 节点，53 秒）。
重新用 unicorn 从二进制直接抽取目标表确认表没抽错 ⇒ 只能是假设错。
**只有 lane 2 是真的**；真 flag 下另外三个 lane 的 `r14` 分别是 `0xd4a995a8 / 0x4aed2c39 / 0x0883d7a7`。
代价：失去三路互补 tap 字节的便利，单 lane 的 op22 阻塞让搜索空间从可枚举变成需要专门的 C 求解器。

> **教训**：在一个刻意设计成「随机输入永远失败」的目标上，任何基于随机输入统计的推断都天然有偏。
> 能定性的证据只有两种：从二进制直接抽取的常量，和 2⁻³² 量级的巧合。

## 7. 模型与脚本

| 文件 | 作用 | 验证 |
|---|---|---|
| `expand_model.py` | `input26 ↔ expanded[32]` 双向 | 44/44 对拍 · 200/200 往返 · 随机 200/200 被拒 |
| `vm_model.py` | `run_vm(expanded, sel) → state`；含 `finalize` / `finalize_inv` | 60 case / 1920 字节全等 · finalize 500/500 往返 |
| `full_model.py` | `full_check(input26) → 4 dword`（完整 oracle） | 13/13 组全等 · 780/780 struct dword |
| `vm_disasm.py` → `prog0..3.asm` | 字节码反汇编器与清单（各 257 条） | 与字节码逐字段 0 失配 |
| `vm_replay.py` | 纯字节码语义重放器（不依赖 unicorn） | 4 程序 state 与全部操作数复现 |
| `back.py` → `back28.json` | 从钉死的终态倒走 31→28 轮，产出 6 个候选锚点 | 合成数据验证通过 |
| `gen_c.py` → `vmtab.h`、`peel2.c` | C 剥壳求解器（前向与 vm_model 位级一致） | `d12=272` 命中 |
| `verify.py` | 端到端验证：模型 + 真实二进制 | 见下 |
| `emu.py` | unicorn 仿真骨架（1.3 ms/run），全部 ground truth 来源 | 12 项完整性检查 9 项恒 0 |

另有 `t7_*` / `t8_*` / `t9_*` / `t9b_*` / `t9c_*` 共约 40 个一次性探针脚本
（轨迹分类、语义拟合、常量抽取、r14 分解、z3 裁决）。

端到端验证输出：

```
$ python3 verify.py f1b4801d0d18245b437c05da5b354020262485099321b50a6615bbd15e601d3f
expanded f1b4801d0d18245b437c05da5b354020262485099321b50a6615bbd15e601d3f
  digest12 = 272
  sel0: state==E[0] False  r13f=0xcff5e248(False) V34f=0x97e220ec(False) perm=False
  sel1: state==E[1] False  r13f=0x2a976b99(False) V34f=0xc22cf1d0(False) perm=False
  sel2: state==E[2] True   r13f=0xe6a68d04(True)  V34f=0x2e8c989c(True)  perm=True
  sel3: state==E[3] False  r13f=0x68f3bb2b(False) V34f=0x70603c49(False) perm=False
  unexpand -> b'flag{v4_opaque_trace_2026}'
  full_check = ['0x892a48af','0xb45dcd47','0x6c5ac3','0xb0b1062a'] TARGET [...] MATCH
  ./AntiAi.exe -> b'input flag: ok\r\n'
```

## 8. 成本

主 agent 维护黑板状态（`BLACKBOARD.md`，39 条 fact / 10 个任务），8 个子 agent 并行执行。
下表为各子 agent 实测消耗（主 agent 自身 token 未被本次运行统计，故不计入）：

| 子任务 | tokens | 时长 |
|---|---:|---:|
| r14 操作数定位 + 目标表抽取（含追问） | 218 550 | 18.5 min |
| VM 分发轨迹分类（证明 4 个固定程序） | 159 549 | 21.0 min |
| expand 建模与求逆 | 69 391 | 7.9 min |
| VM 前向 Python 模型 + 对拍 | 196 677 | 24.5 min |
| 字节码反汇编器 + 数据流分析 | 168 441 | 26.3 min |
| `finalize_2940` + 完整 oracle + z3 裁决 | 177 442 | 24.0 min |
| 反演求解（Python 规划 + C 剥壳） | 419 869 | 135.7 min |
| 冗余反演（第二实现，命中后中止） | 未统计 | — |
| **合计（已统计部分）** | **1 409 919** | **257.8 min** |

| 口径 | 数值 |
|---|---:|
| 墙钟总时长（拿到样本 → 实机验证通过） | 约 7 h 07 min |
| 其中本次会话 | 约 4 h 14 min |
| 子 agent 累计计算时长（并行） | 约 4 h 18 min |
| 最终搜索规模 | 约 1.5 × 10¹² 节点 |
| 搜索吞吐 | 45 M 节点/秒/核 × 32 核 |
| 纯 Python 前向模型 | 0.45 ms / `run_vm` |
| unicorn 全量仿真 | 1.3 ms / `check` |

时间账里最贵的一段不是搜索，而是**推翻「四个 lane 都要通过」这个假设**：
假设成立时四路可互相补齐 tap 字节、剥壳近乎线性；假设一破，单 lane 的 op22 阻塞让搜索空间从可枚举
变成需要专门的 C 求解器。

登录后可查看完整内容

传递专业知识、拓宽行业人脉——看雪讲师团队等你加入！！

最后于 2026-8-13 00:44 被Magic丶编辑，原因：

上传的附件：