[分享]第九题：丑寅同墟·星海抉择-CTF对抗-看雪安全社区

[分享]第九题：丑寅同墟·星海抉择

发表于: 2026-8-22 12:18 38

[分享]第九题：丑寅同墟·星海抉择

correy

2026-8-22 12:18

# 看雪 KCTF 2026 — ICTFForCausalLM Writeup

> **方向**：Reverse / AI · **关键词**：字符级语言模型、safetensors、门控网络、超定线性方程组
> **Flag**：`flag{f1ag2026c7fa1666}`（模型内隐藏的明文秘密：`f1ag2026c7fa1666`）

---

## 0. 一句话结论（TL;DR）

题目给了一个"字符级语言模型" `ICTFForCausalLM` 和它的权重，让你找出让模型输出 `<success>` 的输入。

拆开权重会发现，这**根本不是什么语言模型，而是一把用神经网络伪装的锁**：

- 输出层是纯"门控"——**除 `<success>` 外，所有 logit 都是与输入无关的常数**，`<fail>` 恒等于 `0.4`，就是那条要被越过的横线；
- 隐藏层里 20 个"看似随机"的单元，其真身是一组**秩为 16 的线性方程**，把 flag 编码了进去；
- 于是"找到通关输入"退化成**解一个超定但相容的线性方程组** `W·x = b`，唯一解就是 flag。

不需要梯度、不需要训练，甚至不需要 z3——`numpy.linalg` 一步直解得到 `f1ag2026c7fa1666`，再用前向传播确认模型确实吐出 `<success>`。

---

## 1. 题目与真值来源

题面（`题目要求.txt`）：

> 附件中提供了一个简单的字符级语言模型 `ICTFForCausalLM` 及其模型权重。模型接受长度不超过 16 个字符的字符串作为输入，并预测一个输出字符。你的目标是分析给出的模型代码与权重，找出隐藏在模型中的秘密，并恢复正确的 flag。

附件：

```text
inference.py            # 加载模型 + 交互测试（读输入 → 打印预测字符）
model_def.py            # tokenizer / config / 模型结构
ictf_model/
├── config.json         # hidden_size=21, vocab_size=64, max_position_embeddings=16, dtype float32
└── model.safetensors   # 权重 —— 本题真值来源
```

**真值来源**：`model.safetensors` 的权重字节 + `model_def.py` 的前向传播。没有远程服务，纯静态分析——只要能**逐位精确复现前向计算**，就掌握了这道题的 oracle。定下策略：读权重 → 抽约束 → 求解 → 用真实前向验证收口。

---

## 2. 读代码：模型到底在算什么

### 2.1 Tokenizer

```python
charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"  # 62 个字符
char2id: '0'->0 ... 'Z'->61
id2char[62] = "<success>"     # 目标输出
id2char[63] = "<fail>"
vocab_size = 64
pad_token_id = 0              # 不足 16 个，用 id 0 右侧补齐
```

一个小坑：pad 用的 id 0 与字符 `'0'` 的 id 相同，所以恢复出的 id 序列**直接按 `id2char` 解码**即可，无需区分"哪些是 padding"。

### 2.2 网络结构

```python
self.dense   = nn.Linear(16, 21, bias=True)   # 16 -> 21
self.act     = nn.ReLU()
self.lm_head = nn.Linear(21, 64, bias=True)   # 21 -> 64

def forward(self, input_ids):
    x = input_ids.float()             # (16,)  ★ 直接把 token id 当浮点特征喂进去
    h = self.act(self.dense(x))       # (21,)  ReLU
    logits = self.lm_head(h)          # (64,)
    return {"logits": ...}            # 推理端取 argmax 作为预测字符
```

**决定性的一点**：这里**没有 embedding 层**，token id 被当作原始浮点数直接参与线性运算。这让整个网络对输入是**分段线性**的——这正是它能被当成线性方程/约束系统求解的根本原因。

目标随之明确：**让 `argmax(logits) == 62`（`<success>`）。**

---

## 3. 侦察：手工解析权重

`safetensors` 格式极简：`8 字节小端头长 + JSON 头 + 原始张量字节`。环境里没装 torch，但根本不需要——纯 Python 就能读：

```python
import struct, json, numpy as np
data = open("ictf_model/model.safetensors", "rb").read()
n   = struct.unpack("<Q", data[:8])[0]
hdr = json.loads(data[8:8+n]); base = 8 + n
def get(name):
    o = hdr[name]["data_offsets"]
    return np.frombuffer(data[base+o[0]:base+o[1]], "<f4").reshape(hdr[name]["shape"])
```

四个张量：

| 张量 | 形状 | 值域 |
|------|------|------|
| `dense.weight` | (21, 16) | 全整数，−3472 … 5574 |
| `dense.bias` | (21,) | 大多整数；`b[0]=311558.71875` 巨大 |
| `lm_head.weight` | (64, 21) | 出现 `±1e10` 量级 |
| `lm_head.bias` | (64,) | 大量 `-10000`，个别异常 |

`±1e10` 和 `-10000` 这种"人造魔数"一眼就不是训练出来的，是**手工构造的门控**。顺着这条线拆。

---

## 4. 拆穿伪装（一）：输出层是纯门控

`lm_head.bias`（64 维）几乎全 `-10000`，只有两个例外：

| id | 含义 | bias |
|----|------|------|
| 0–61 | 普通字符 | `-10000` |
| 62 | `<success>` | `-376131.21875` |
| 63 | `<fail>` | **`0.4`** |

`lm_head.weight`（64×21）更极端——**只有第 62 行非零**：

```text
row 62 (<success>) = [ 1, -1e10, -1e10, ..., -1e10 ]   # h0 系数=1，h1..h20 系数=-1e10
row 63 (<fail>)    = [ 0, 0, ..., 0 ]                   # 全零
其余所有行         = 全零
```

**推论**：除 `<success>` 外的每个 logit 都是常数——

- id 0–61：`logit = -10000`（永远垫底）；
- id 63 `<fail>`：`logit = 0.4`（恒定，这就是"及格线"）；
- id 62 `<success>`：唯一依赖输入：

$$
\mathrm{logit}[62] \;=\; 1\cdot h_0 \;-\; 10^{10}\!\sum_{i=1}^{20} h_i \;-\; 376131.21875,\qquad h_i=\mathrm{ReLU}(\mathbf{W}_i\!\cdot x + b_i)
$$

所以 "预测 `<success>`" ⟺ `logit[62] > 0.4`（其他对手全 ≤ 0.4）。

**结构可视化**（这就是一把"与门锁"）：

```text
        16 位输入 x  ─────────────────────────────────┐
              │                                        │
   ┌──────────┴───────────┐                            │
   ▼                      ▼ (×20)                       ▼
 h0 = ReLU(W0·x + b0)   h1..h20 = ReLU(Wi·x + bi)   (其余 logit = 常数)
 「通关能量」           「20 个校验开关」            0-61: -10000
   │  ×1                  │ 每个 ×(-1e10)             63 <fail>: 0.4  ← 及格线
   ▼                      ▼
   └──────►  logit[62] = h0 - 1e10·Σhi - 376131.21875  ──► 需 > 0.4
                          ▲
        任一 hi>0 → 减去 1e10 → 直接判负(<fail>)
```

由于 $-10^{10}$ 系数极大，**只要任意一个 $h_i(i\ge1)$ 稍大于 0，`logit[62]` 立刻塌成天文级负数**。要通关只有唯一可能：

1. **$h_1..h_{20}$ 全部为 0**（20 条 ReLU 的输入 ≤ 0）；
2. 此时 `logit[62] = h0 - 376131.21875`，还需 `> 0.4`，即 `h0 > 376131.61875`。

---

## 5. 拆穿伪装（二）：约束在解处全部取等 → 其实是线性方程组

把 ReLU 展开成线性不等式，问题变成整数线性可行性：

```text
(i=1..20)  dense.W[i]·x + dense.b[i] <= 0
(i=0)      dense.W[0]·x + dense.b[0] >  376131.61875   ⟺  dense.W[0]·x >= 64573
每个 x_j   ∈ {0,1,...,61}
```

丢给 z3 求解，得到唯一整数解 `f1ag2026c7fa1666`。但真正漂亮的发现，是**回代检查每条约束的松弛量**：

```text
约束0  dense.W[0]·x = 64573              松弛 0   ← 取等
约束1  dense.W[1]·x = 3473  (上界 3473)  松弛 0   ← 取等
约束2  dense.W[2]·x = -996  (上界 -996)  松弛 0   ← 取等
 ...                                      ...
约束20 dense.W[20]·x= 1047  (上界 1047)  松弛 0   ← 取等
——— 20 条约束全部松弛 = 0 ———
```

**全部取等**意味着作者的真实构造根本不是"不等式区域"，而是一组**线性方程**

$$
\mathbf{W}_i\cdot x = -b_i\quad(i=1,\dots,20)
$$

这是 **20 个方程、16 个未知数**的超定系统。验证其系数矩阵 `dense.W[1:21]`：

```python
A = dense.W[1:21]          # (20, 16)
print(np.linalg.matrix_rank(A))   # -> 16   （满列秩！）
```

**秩 = 16 = 未知数个数**，所以该线性系统的解（若相容）**唯一**。这解释了为什么 z3 只找到一个解：那 20 行"看似随机"的小整数权重，是精心构造的一组约束，把解在整个 `62¹⁶` 空间里**锁死到唯一一点**。

> **作者的构造逆推**：先选定 flag `x*`，为第 1..20 行生成随机小整数权重 `W_i`，再令 `b_i = -W_i·x*`，使每个方程在 `x*` 处成立；第 0 行的 `b_0` 则标定 `h0`，使 `logit[62]` 在 `x*` 处恰为 `0.5`（仅比及格线 `0.4` 高 `0.1`，卡得极紧）。

---

## 6. 求解：两条路，殊途同归

### 方法 A —— 线性代数直解（最优雅，无需 z3）

既然是相容超定线性系统，任取 16 个方程（或对全部 20 个做最小二乘）直接解：

```python
A = dense.W[1:21].astype(np.float64)   # (20,16), rank 16
b = -dense.bias[1:21].astype(np.float64)
x = np.rint(np.linalg.lstsq(A, b, rcond=None)[0]).astype(int)
assert np.abs(A @ x - b).max() == 0    # 残差恰好为 0 → 相容
print("".join(charset[c] for c in x))  # -> f1ag2026c7fa1666
```

甚至只用前 16 行组成方阵 `np.linalg.solve(W[1:17], -b[1:17])`，得到同一解，且剩下 4 个方程残差为 0——超定系统完全相容。

### 方法 B —— z3 约束求解（鲁棒兜底）

不用意识到"其实是等式"，直接把不等式交给 SMT，并用阻塞子句证明唯一性：

```python
from z3 import Int, Solver, Sum, Or, sat
x = [Int(f"x{j}") for j in range(16)]; s = Solver()
for j in range(16): s.add(x[j] >= 0, x[j] <= 61)
s.add(Sum([int(dw[0][j])*x[j] for j in range(16)]) >= 64573)
for i in range(1, 21):
    s.add(Sum([int(dw[i][j])*x[j] for j in range(16)]) <= int(round(-db[i])))
# 求解后加 Or([x[j]!=v[j]]) 再求 → UNSAT，证明解唯一
```

两法结果完全一致：`f1ag2026c7fa1666`。

---

## 7. 真值验证：用前向传播收口

求出的字符串必须让**真实模型**吐出 `<success>` 才算数。前向传播就是两次矩阵乘 + 一次 ReLU，用 numpy（float32，与 `dtype: float32` 一致）精确复现：

```python
def forward(s):
    ids = [char2id[c] for c in s] + [0]*(16-len(s))
    x = np.array(ids, np.float32)
    h = np.maximum(dw.astype(np.float32) @ x + db.astype(np.float32), 0)
    logits = lw.astype(np.float32) @ h + lb.astype(np.float32)
    return int(np.argmax(logits)), logits[62], logits[63]
```

| 输入 | 预测 | logit62 | logit63 |
|------|------|---------|---------|
| **`f1ag2026c7fa1666`** | **`<success>` (62)** | **0.500** | 0.400 |
| `f1ag2026c7fa1665`（末位 −1） | `<fail>` | −6.47e12 | 0.400 |
| `flag` | `<fail>` | −1.6e14 | 0.400 |
| `0000000000000000` | `<fail>` | −1.5e14 | 0.400 |

正确解的 `logit62 = 0.5`，仅高出及格线 `0.4` 整整 `0.1`；**任意一位改动都会点亮某个校验开关，被 `-1e10` 砸成天文负数，立刻 `<fail>`**。

至此三重独立互证闭合：**线性代数直解 = z3 唯一解 = 前向传播实测通关**。

---

## 8. Flag

- 模型中隐藏的明文秘密：`f1ag2026c7fa1666`
- 提交（看雪常规 `flag{}` 包裹）：

```text
flag{f1ag2026c7fa1666}
```

---

## 9. 复盘：这题在考什么

**核心把戏**：把一个哈希校验/口令锁伪装成神经网络。

- 输入直接当浮点特征（无 embedding）→ 网络对输入**分段线性**；
- `ReLU + 巨大负系数` = "硬约束开关"（一旦被激活即判负），是 AI-CTF 里"用网络编码逻辑门"的经典手法；
- 输出层退化为常数，`<fail>=0.4` 就是及格线；
- 隐藏层 20 行是**秩满的线性方程组**，唯一解即 flag——一个可被 SMT 秒解、更可被线性代数一步直解的系统。

**方法论上的关键点：**

1. **先读权重，再动手**。看到 `lm_head` 只有第 62 行非零、`<fail>` 恒 `0.4`，立刻明白"只有 `<success>` 依赖输入"，`62¹⁶` 的搜索空间瞬间塌缩——若一上来盲目交互猜输入则毫无希望。
2. **不迷信框架**。torch 缺失反而逼出更透彻的路径：手工解析 safetensors + numpy 复现前向，把计算彻底看穿。
3. **回代看松弛量**。z3 出解后检查每条约束是否取等，才发现"不等式区域"其实是"线性方程组"，从而获得比 z3 更优雅、更快的线性代数解法，并从数学上解释了唯一性（秩 = 16）。
4. **真值验证收口**。用与题目一致的 float32 前向复现，确认模型真的输出 `<success>` 才定稿——只有真正产出且被 oracle 确认的 flag 才算赢。

> **一句话**：所谓"字符级语言模型"是障眼法，本质是一组秩满线性方程锁死的口令锁——读懂权重，解方程（或交给 z3），前向验证，收工。

---

## 附：一键复现

同目录 `solve.py`：解析 safetensors → 线性代数直解 + z3 互证 → numpy 前向验证 → 打印 flag。

```bash
$ python3 solve.py
[A] 线性代数直解: f1ag2026c7fa1666
[B] z3 唯一解  : f1ag2026c7fa1666
[+] 真值验证: 模型预测 id=62 -> <success>  (logit62=0.5000 > logit63=0.4000)
[+] FLAG: flag{f1ag2026c7fa1666}
```

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

收藏・0

点赞・0

打赏