[原创]KCTF 2026 第九题：丑寅同墟·星海抉择 WriteUp-CTF对抗-看雪安全社区

[原创]KCTF 2026 第九题：丑寅同墟·星海抉择 WriteUp

发表于: 2026-8-22 13:40 205

[原创]KCTF 2026 第九题：丑寅同墟·星海抉择 WriteUp

neilwu

2026-8-22 13:40

205

这题乍一看是 AI 题，给了个叫 `ICTFForCausalLM` 的语言模型和权重，要求找出触发 `<success>` 的 16 字符 flag。但扒开代码一看，其实是一道纯粹的白盒逆向/密码学题。

## 0x01 分析

第一步肯定是看源码 `model_def.py`。这根本不是什么 Transformer 结构，就是一个极简的两层多层感知机（MLP）。

梳理一下核心逻辑：
1. **输入限制**：长度最多 16 个字符。字符集 62 个（`0-9`, `a-z`, `A-Z`），对应 ID `0-61`。
2. **目标条件**： `<success>` 的 ID 是 62。我们需要构造输入，让模型预测输出的 64 个 logits 中，第 62 号位置的值最大。
3. **数据流向**：
   - 输入的 integer ID 直接强转为 float：`x = input_ids.float()`
   - 经过第一层全连接：`H = X @ W1.T + b1`
   - 经过激活函数：`H_relu = max(0, H)`
   - 经过输出层：`Logits = H_relu @ W2.T + b2`

## 0x02 思路

爆破空间是 $62^{16}$，直接算肯定不现实。

既然整个前向传播的逻辑非常清晰，而且模型权重完全在手（白盒），这本质上就是一个多元一次方程组的求解问题。直接把网络里的矩阵乘法和 ReLU 翻译成数学约束，丢给 SMT 求解器（比如 Z3）硬算就行。

## 0x03 构造 Z3 约束求解

写 EXP 的核心就是把 PyTorch 的计算图用 Z3 的 API 重新手搓一遍。代码如下，关键点写了注释：

```python
import torch
from z3 import *
from model_def import ICTFForCausalLM, ICTFTokenizer

print("[*] Loading model weights...")
tokenizer = ICTFTokenizer()
model = ICTFForCausalLM.from_pretrained("./ictf_model")

# Extract the fixed weights and biases
W1 = model.dense.weight.detach().numpy()
b1 = model.dense.bias.detach().numpy()
W2 = model.lm_head.weight.detach().numpy()
b2 = model.lm_head.bias.detach().numpy()

print("[*] Building Z3 constraints...")
solver = Solver()

# Define our 16 input characters as integers
X_int = [Int(f'x_{i}') for i in range(16)]

# Constraint: Valid token IDs fall within the 62-character charset (0 to 61)
for i in range(16):
    solver.add(X_int[i] >= 0, X_int[i] <= 61)

# Cast to Real for Z3's continuous math calculations
X_real = [ToReal(x) for x in X_int]

# Layer 1: Dense + ReLU
H_relu = []
for j in range(21): # hidden_size is 21
    # H_j = sum(X_i * W1[j, i]) + b1[j]
    node_val = Sum([X_real[i] * float(W1[j, i]) for i in range(16)]) + float(b1[j])
    # ReLU: max(0, node_val)
    H_relu.append(If(node_val > 0, node_val, RealVal(0)))

# Layer 2: lm_head (We only care about logits for valid chars + success token)
logits = []
for k in range(64): # vocab_size is 64
    logit_val = Sum([H_relu[j] * float(W2[k, j]) for j in range(21)]) + float(b2[k])
    logits.append(logit_val)

# Constraint: The logit for <success> (ID 62) must be the absolute maximum
success_logit = logits[62]
for k in range(64):
    if k != 62:
        solver.add(success_logit > logits[k])

print("[*] Solving for the flag...")
if solver.check() == sat:
    m = solver.model()
    flag_ids = [m[X_int[i]].as_long() for i in range(16)]
    flag = tokenizer.decode(flag_ids)
    print(f"\n[+] Success! Flag recovered: {flag}")
else:
    print("\n[-] UNSAT: Could not find a valid input sequence.")
```

环境对了就能直接跑出 flag。

```
[*] Loading model weights...
[*] Building Z3 constraints...
[*] Solving for the flag...

[+] Success! Flag recovered: f1ag2026c7fa1666
```

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

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

收藏・0

点赞・3

打赏

最新回复 (1)
mb_fabrnyzx 雪币： 200 能力值： ( LV1，RANK：0 ) 在线值：发帖 0 回帖 5 粉丝 0 关注私信	mb_fabrnyzx 2 楼 6 2026-9-7 16:48 0
	游客登录 \| 注册方可回帖回帖表情雪币赚取及消费高级回复

neilwu

发帖

170

回帖

224

RANK

关注

私信

他的文章

关于我们

联系我们

企业服务

看雪公众号

专注于PC、移动、智能设备安全研究及逆向工程的开发者社区