flag：flag{v4_opaque_trace_2026}（26 字节）

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

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

check 是四段式：

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

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

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

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

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

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

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 为硬常量。

其余状态机：

对 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 的实际载入覆盖：

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

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

剥壳算法：按轮号 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 分钟墙钟。

一、「目标表是 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⁻³² 量级的巧合。

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

端到端验证输出：

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

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

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