[原创]第六题：酉时·书院迷局从双分支耦合到代数逆推-CTF对抗-看雪安全社区

[原创]第六题：酉时·书院迷局从双分支耦合到代数逆推

发表于: 2026-8-18 16:19 399

[原创]第六题：酉时·书院迷局从双分支耦合到代数逆推

Kazusa

2026-8-18 16:19

399

题目给出一个 Android APK。界面上只有一个输入框和一个 `VERIFY` 按钮，目标是找到
一组合法输入，使未修改的原版程序提示：

```text
Correct! Flag accepted.
```

这题真正麻烦的地方不是某一个算法特别复杂，而是 native 层同时布置了多套状态机、
opaque helper、完整性检查和真假分支。输入又被拆成奇偶两组：odd 分支决定 even 的
目标，even 分支反过来决定 odd 的 salt。只看任意一边，都会得到一个无法独立验证的
“半成品答案”。

最终没有修改 APK，也没有绕过返回值。整个解法是先确定程序的真实正向数据流，再从
odd 的终端约束逆出 odd25，随后求出 even 的状态参数，最后把两组字节重新交织回原始
50 字节输入。

求解顺序可以概括为：

```text
odd 终端约束 -> odd25 -> selector -> even 目标摘要
                                 -> even 参数 -> salt
                                 -> odd/even 同时回验
```

## 0x00 Java 层：输入格式

入口在 `com.autorun.kctf.MainActivity`。Java 层先规范化输入，然后调用 JNI：

```java
normalized = input.trim().toLowerCase(Locale.ROOT);
if (!input.equals(normalized)) fail();

byte[] raw = hexDecode(input);   // 必须正好 100 hex -> 50 bytes
if (nativeProcessInput(raw) == 1)
    show("Correct! Flag accepted.");
```

因此输入有三个直接约束：

- 必须正好 100 个十六进制字符；
- 必须全部小写；
- 前后不能有空格或换行。

JNI 校验对象是十六进制字符串解码得到的 50 个字节，不要求这些字节本身可打印。

## 0x01 运行时材料 `K`

native 会通过 Java 方法读取 APK/ELF 中的 `.kctfguard` 元数据。Java 先用
`nativeShareMask` 遮罩前 16 字节，native 再用相同掩码恢复。

对未修改 APK，真实运行时材料为：

```text
K = 870573e5f5c63d52862dbd05ab3d9494
```

后面的 guard 校验值、地址和长度只是完整性材料，不是隐藏 flag。

## 0x02 总体验证结构

50 字节输入通过三次 ARM64 `VLD2` 按下标奇偶拆成两个 25 字节数组：

```python
even[j] = input[2*j]
odd[j]  = input[2*j+1]
```

两支不是独立的：odd 先决定 even 的摘要目标，even 再决定传给 odd 最终校验器的
salt。

下面这张图只描述 `MainActivity.nativeProcessInput(byte[50])` 内部的主校验数据流。
even25 完成可逆预处理后会写入一个 25 字节中间缓冲区，后续四个 stage 都从这里
读取状态。

![真实验证链流程图](upload/attach/202608/844648_A7S4VVRUECNCZC8.webp)

看起来像环形依赖，但方向是确定的：

- 先解 odd，得到 `selector`；
- selector 固定 even 的目标摘要；
- 再解 even，并要求它自然产生 odd 所需 salt。

## 0x03 去混淆：先确定 helper 的真实语义

native 中有大量 opaque helper 和伪分支。通过静态化简、Unicorn/angr 与真机动态
回归，可归纳为：

| helper | 真实语义 |
|---|---|
| `sub_2CBC` | 恒返回 `1` |
| `sub_2D70` | 恒返回 `0` |
| `sub_2E2C` | 恒返回 `0` |
| `sub_10800` | 恒返回 `0` |
| `sub_E818(a,b,noise)` | `a ^ b` |
| `sub_EE90(a,b,...)` | `a + b` |
| `sub_F004(a,b,...)` | `a - b` |
| `sub_E960(x,...)` | `x == 0 ? 0 : 0xffffffff` |
| `sub_EB6C(x,...)` | 返回值低字节等于 `x` 的低字节 |

这一步很重要：如果保留所有伪分支直接符号执行，状态空间会迅速爆炸；化简后真正的
根返回门只有 `even_ok` 和 `odd_ok`。

## 0x04 odd 分支

### 4.1 12 轮 ARX

`odd[0:25]` 后补 7 个 `0x5a`，组成 32 字节并解释成四个小端 64 位字。
`sub_5FE8` 的单轮可写成：

```python
MASK = (1 << 64) - 1

def round_fwd(state, i):
    a, b, c, d = state
    p  = ((ror(a, 8) + b) & MASK) ^ i
    nb = ror(b, 61) ^ p
    q  = ((ror(c, 8) + d) & MASK) ^ (i + 4)
    nd = ror(d, 61) ^ q
    return p ^ nd, nb, q ^ nb, nd
```

跑满 12 轮后得到 96 字节派生状态 `O`。用于 even 目标变换的 selector 是：

```text
selector = O[60] ^ O[80] ^ ROL8(O[95], 1) ^ 0x5d
```

### 4.2 `sub_8F90` 的真实必要条件

odd 最终校验器的调用形式为：

```text
sub_8F90(odd25, K, salt)
```

尾部虽然很长，但返回 1 实际要求以下检查同时成立：

- 两次 `advance` 后的 `C,D` 等于固定 16 字节目标；
- 由 `A`、salt、目标与 `K` 派生的 8 字节 tag 相等；
- 46 位布尔 mask 等于固定值；
- 两组 `sub_7400` tag 相等；
- 8 字节 salt/check 相等；
- `v509 == 0`；
- 最后一级 byte-MAC 相等；
- 输入无关的完整性项 `v525 == 0`。

其中一组 `sub_7400` tag 的目标变换对 salt 可逆，已经足以唯一确定：

```text
salt = 0xd7
```

另一组给出同一结果，是冗余校验。固定 `salt=0xd7` 后，tag 与 mask 约束可用
Z3/PySAT 反解 `A,B`，再逆 12 轮 ARX 得到 odd25。

最终 odd 候选为：

```text
odd25 = 7ae31b94d256f80c41b7298e63a5df104bc8723d960fe458ad
```

具体回归值：

```text
A       = 58b67a47304291c1
B       = 9eb09ed6e443b907
target  = 9f73be24a1dd6c96b90723bba7cdfdc9
tag689  = fd521311dd1b1725
mask46  = 16eff8c39c23
```

该 odd 候选在真机上强制 `salt=d7` 时，`sub_8F90` 返回 1。

### 4.3 selector 和 even 目标

对该 odd25：

```text
O[60] = d9
O[80] = 9f
O[95] = c9

selector = d9 ^ 9f ^ ROL8(c9,1) ^ 5d = 88
```

native 先生成基础目标：

```text
baseTarget = e6a03b9e75425736e63343bc6cc2309f
```

再执行 `sub_EDCC`：

```python
s = selector ^ 0xa1
for i in range(16):
    s = (61*s + 113 + 19*i) & 0xff
    expected[i] ^= s ^ (s >> 3)
```

得到最终 even 目标：

```text
expectedDigest = d6ced48b4a6f314d11f654f72956c20e
```

## 0x05 even 预处理

even25 先经过一个严格可逆的逐字节置换，生成 25 字节中间缓冲区。下面简记为
`buf[25]`：

```python
perm = [7,2,19,0,14,23,5,11,21,3,17,8,24,
        1,12,6,20,10,4,22,15,9,18,13,16]

state = K[7] ^ 0xc3
for i in range(25):
    r = ROL8((state + 49*i + K[(1+7*i)&15]) & 0xff, i)
    buf[i] = ((even[perm[i]] - r) & 0xff) ^ K[(3+5*i)&15]
    state = ((buf[i] + r) & 0xff) ^ ((90+35*i) & 0xff)
```

这层只是双射，不参与成功判定。因此可以先求出中间缓冲区，再按相反顺序逐字节逆回
even25。

## 0x06 even 的四个 stage

### 6.1 Stage 的真实作用

Stage 1～4 的局部检查 **不是最终返回门**：

- Stage 1 失败会改变 S-box 初态或 `stage1State`；
- Stage 2 失败会把 S-box 回退为 identity；
- Stage 3 失败只会执行 `delta ^= 1`；
- Stage 4 失败只会令 `rotation = 0`。

所以不能从控制流上断言“四个 stage 必须全过”。正确做法是把全通过路径作为一个候选
构造，求解后再检查最终摘要和 salt。事实证明本题的预期解确实位于这条自然路径上。

### 6.2 Stage 1 和 Stage 2

Stage 1 的自然通过前缀为：

```text
buf[0:13] = 0200000001832dbd05c70573e5
stage1State = 0x0001058c
```

Stage 2 以 `0xe57305c7` 为 xorshift32 seed，生成并散布 256 字节流。自然路径的
S-box 前 16 字节为：

```text
852627dbc4a5730a3646d3ab9987c8eb
```

因此 `sbox[0] = 0x85`。

### 6.3 Stage 3

Stage 3 从中间缓冲区读取两个 32 位参数：

```text
delta_source = u32(buf + 13)
seed0        = u32(buf + 17) ^ 0x85858585
```

LCG 为：

```python
seed = (seed * 0x0019660d + 0x3c6ef35f) & 0xffffffff
```

连续生成 32 个 key，再对三组明文做 16 轮 TEA-like ARX：

```text
(00000001,00000002) -> (7cf2c5a2,1410ee09)
(deadbeef,cafebabe) -> (c094c7f3,5c08eeea)
(12345678,9abcdef0) -> (18cf95e0,8c30c302)
```

自然路径取标准 TEA delta：

```text
delta = 0x9e3779b9
```

此时只剩 32 位 seed0。通用 64 位 QF_BV 求解很慢，因此使用 CUDA 完整枚举
`2^32` 个 seed，只用第一组向量筛选，再用另外两组独立回验：

```cuda
seed = seed0;
total = delta;
for (int round = 0; round < 16; ++round) {
    seed = seed * 0x0019660d + 0x3c6ef35f;
    x += ((((y << 4) ^ (y >> 5)) + y) ^ (total + seed));

seed = seed * 0x0019660d + 0x3c6ef35f;
    y += ((((x << 4) ^ (x >> 5)) + x) ^ (total + seed));
    total += delta;
}
```

枚举命中结果为：

```text
delta=9e3779b9 seed0=5b28455b
00000001 00000002 -> 7cf2c5a2 1410ee09
deadbeef cafebabe -> c094c7f3 5c08eeea
12345678 9abcdef0 -> 18cf95e0 8c30c302
```

于是：

```text
seed0              = 0x5b28455b
u32(buf + 17)      = seed0 ^ 0x85858585
                   = 0xdeadc0de
key0               = LCG(seed0)
                   = 0xaeffbafe
```

`0xdeadc0de` 也印证这是预期构造值，而不是偶然碰撞。

### 6.4 Stage 4

Stage 4 的 8 个等式可直接用 Z3 求出：

```text
rotation = 7
aux      = 0x371342
width    = 16 + (key0 >> 28) = 26
```

对应中间缓冲区尾部：

```text
buf[21]    = 07
buf[22:25] = 421337        # 0x371342 的小端表示
```

## 0x07 even 核心 `sub_126B8`

核心初始四个 32 位字固定为：

```text
deadbeef cafebabe 8badf00d feedface
```

共执行 **12 轮**，两条 lane 分别使用偶数和奇数 key。单条 lane 的轮函数为：

```python
total = (round + 1) * delta
f = (((right << 4) ^ (right >> 5)) + right) & 0xffffffff
new_left = left + (f ^ (key + total))

r  = ROL32(new_left, rotation)
mk = key & ((1 << width) - 1)
g  = (mk + (r >> 5)) ^ ((mk >> 12) + (r << 4))
g ^= (key + total) ^ r
new_right = right + g
```

完成前 10 轮后、进入第 11 轮前，四个 word 各执行：

```python
word ^= sbox[word & 0xff]
```

代入求出的参数：

```text
delta    = 9e3779b9
key0     = aeffbafe
rotation = 7
width    = 26
```

得到：

```text
coreDigest = d6ced48b4a6f314d11f654f72956c20e
```

与 odd selector 产生的 `expectedDigest` 完全一致。

## 0x08 even 产生 odd salt

even 还必须自然产生 `salt=0xd7`，否则已解出的 odd25 仍不能通过。

```python
t = stage1State ^ key0 ^ aux
t ^= (rotation << 24) ^ (0x01010101 * sbox[0])
t ^= t >> 16
t = (0x045d9f3b * t) & 0xffffffff
t ^= t >> 15
t ^= t >> 8
salt = (t ^ 0x2a) & 0xff
```

代入：

```text
stage1State = 0001058c
key0        = aeffbafe
aux         = 00371342
rotation    = 7
sbox[0]     = 85
```

得到：

```text
salt = d7
```

至此 even 摘要和 odd salt 两条耦合约束同时闭合。

## 0x09 重建完整输入

完整的 25 字节中间缓冲区为：

```text
0200000001832dbd05c70573e5b979379edec0adde07421337
```

按第 6 节的字节关系逆变换，恢复出 even25：

```text
even25 = a77a78ffc894367d1bf5bb3faab6e2f4db0070533de8b73443
odd25  = 7ae31b94d256f80c41b7298e63a5df104bc8723d960fe458ad
```

按 `even[0], odd[0], even[1], odd[1], ...` 交织：

```python
flag_bytes = bytes(sum(zip(even25, odd25), ()))
flag = flag_bytes.hex()
```

最终得到：

```text
a77a7ae3781bff94c8d2945636f87d0c1b41f5b7bb293f8eaa63b6a5e2dff410db4b00c87072533d3d96e80fb7e4345843ad
```

## 0x0A 验收

### 10.1 JNI 直接验收

在未修改 APK 中被动观测摘要、salt 与 odd 返回值，同时直接调用
`MainActivity.nativeProcessInput(byte[50])`。

成功结果：

```json
{
  "core": "d6ced48b4a6f314d11f654f72956c20e",
  "expected": "d6ced48b4a6f314d11f654f72956c20e",
  "computed": "d6ced48b4a6f314d11f654f72956c20e",
  "salt": 215,
  "oddResult": 1,
  "result": 1
}
```

### 10.2 UI 冷启动验收

停止 Frida，彻底冷启动应用，输入 100 字符并点击真实 `VERIFY` 按钮，Toast 显示：

```text
Correct! Flag accepted.
```

这排除了“模型正确但真机路径不一致”、hook 修改寄存器、APK 被修改等情况。

![原始 APK 冷启动验收](upload/attach/202608/844648_MNSVXP24VZX5QDR.webp)

题目 APK 与设备安装包的 SHA-256 均为：

```text
21f932aa6222a37ffc4183861017794c45c3e07a5eb88a7b9050e044256e763f
```

## 0x0B 总结

这题的难点不在某一个轮函数，而在于 odd 和 even 两条分支之间存在双向依赖，同时
四个 stage 的局部检查又只负责选择后续状态，并不直接决定 JNI 返回值。把 opaque
helper 和伪分支化简后，真正的成功条件可以收束为两项：even 生成的 16 字节摘要必须
等于 odd 决定的目标摘要，odd25 还必须在 even 自然生成的 salt 下通过 `sub_8F90`。

求解时先从 odd 尾部约束逆出 odd25，由此得到 `selector=0x88` 和
`expectedDigest=d6ced48b4a6f314d11f654f72956c20e`，同时确定 odd 校验所需的
`salt=0xd7`。随后处理 even 分支，恢复 Stage 1～4 所需的状态参数，使
`sub_126B8` 生成相同的 16 字节摘要，并验证最终 salt 正好为 `0xd7`。最后逆掉
even25 的字节预处理，与 odd25 重新交织，得到完整的 50 字节输入。

最终候选先通过 JNI 直接调用，随后又在未修改、无 hook 的原始 APK 中完成冷启动验收，
界面明确显示 `Correct! Flag accepted.`。至此静态分析、代数求解、原生执行结果和
最终 UI 行为能够相互闭合，完整验证链也就全部成立。

登录后可查看完整内容

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

收藏・0

点赞・1

打赏