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

## 题目描述

附件提供了一个简单的字符级"因果语言模型" `ICTFForCausalLM` 以及模型权重：

- 模型接受长度不超过 16 个字符的字符串作为输入
- 预测下一个输出字符
- 目标：分析模型代码与权重，找出隐藏的 flag

文件结构：
- `model_def.py` — 模型定义
- `inference.py` — 推理脚本（输入 prompt，打印预测字符）
- `ictf_model/config.json` + `model.safetensors` — 模型配置和权重
- `题目要求.txt`

## 初步分析

### 1. 字符集

`ICTFTokenizer`（[model_def.py#L6-L40](file:///C:/Users/admin/Downloads/题面/model_def.py#L6-L40)）：

```python
self.charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
```

只有 62 个字母数字字符，**没有 `{`、`}`、`_`、`-` 等符号**。因此 flag 只包含数字和大小写字母。

特殊 token：
- `id=62` → `<success>`（验证成功）
- `id=63` → `<fail>`（验证失败）

### 2. 模型结构 — "Causal LM"名不副实

查看 `forward` 函数（[model_def.py#L68-L74](file:///C:/Users/admin/Downloads/题面/model_def.py#L68-L74)）：

```python
def forward(self, input_ids, **kwargs):
    x = input_ids.float()                          # [batch, 16]
    hidden_states = self.dense(x)                   # Linear(16, 21)
    hidden_states = self.act(hidden_states)         # ReLU
    logits = self.lm_head(hidden_states)            # Linear(21, 64)
    logits = logits.unsqueeze(1)                    # [batch, 1, 64]
    return {"logits": logits}
```

**关键发现：没有词嵌入层！** `input_ids` 直接被转成 `float` 送入第一层。也就是说字符 ID（0~61 的整数）本身被当作**数值特征**使用，而不是作为索引去 lookup embedding。

这根本不是"因果语言模型"，而是一个两层 MLP 分类器：

```
x (16个字符ID) → Linear(16→21) → ReLU → Linear(21→64) → 输出64类logits
```

## 深度权重分析

使用 `safetensors` 加载权重，重点看输出层 `lm_head`：

```
Output[ 0..61] (字符): 所有权重=0, bias=-10000
Output[62]  <success>: w[0]=1.0,  w[1..20]=-10_000_000_000,  bias=-376131.22
Output[63]  <fail>:    所有权重=0,  bias=0.4
```

这是本题最核心的设计！解读如下：

| 输出 | 默认值 | 与隐藏层关系 |
|---|---|---|
| 普通字符 | -10000 | 永远不可能胜出 |
| `<fail>` | **0.4** | 与隐藏层无关，恒定输出 0.4 |
| `<success>` | -376131.22 | 仅 `hidden[0]` 贡献 +1×，其余 `hidden[1..20]` 每个贡献 **-100亿×** |

### 推导获胜条件

要让 `<success>` 成为 argmax，必须满足：

1. **隐藏层 1~20 的 ReLU 输出必须全部为 0**：
   - 否则任何一个 hidden[i]>0 都会让 success 减去 100 多亿
   - ReLU(h)=0 ⇨ 预激活值≤0：
     $$\sum_{j=0}^{15} W[i,j] \cdot x[j] + b[i] \le 0 \quad (i=1..20)$$

2. **隐藏层 0 的输出必须足够大**：
   - success logit = hidden[0] − 376131.22 > fail logit = 0.4
   - ReLU(h)=h（只需 h>0），即：
     $$\sum_{j=0}^{15} W[0,j] \cdot x[j] + b[0] \ge 376132$$

## 建模为约束满足问题（CSP）

把条件整理成标准形式，变量为 $x_0, x_1, \dots, x_{15}$（每个取值 0..61 的整数，对应字符 ID）：

$$
\begin{cases}
\sum_{j=0}^{15} W[i,j] \cdot x_j \le -b[i], & i=1..20 \quad (\text{20 条约束}) \\[6pt]
\sum_{j=0}^{15} W[0,j] \cdot x_j \ge 64574, & (\text{因为 } b_0 = 311558.72,\ 376132-311558.72 \approx 64573.3) \\[6pt]
x_j \in \{0,1,\dots,61\}, & j=0..15
\end{cases}
$$

暴力枚举 $62^{16} \approx 4.76 \times 10^{28}$ 不可行。使用 **Z3 SMT 求解器**（整数线性算术）在 0.58 秒内求解完成。

## Z3 求解脚本

```python
import numpy as np
from z3 import *

# dense_w[21,16], dense_b[21] 从 safetensors 导出
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)

# 20 条约束：hidden[1..20] 预激活 <= 0
for i in range(1, 21):
    expr = sum(int(round(dense_w[i,j])) * x[j] for j in range(16))
    s.add(expr + int(round(dense_b[i])) <= 0)

# success 阈值约束
expr0 = sum(int(round(dense_w[0,j])) * x[j] for j in range(16))
s.add(expr0 >= 64573)

print(s.check())     # sat
m = s.model()
x_vals = [m[x[j]].as_long() for j in range(16)]
print(x_vals)
# [15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6]
```

## 还原 Flag

```python
charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
flag = ''.join(charset[v] for v in x_vals)
print(flag)
```

逐字符映射：

| 位置 | x 值 | 字符 | 位置 | x 值 | 字符 |
|---|---|---|---|---|---|
| 0 | 15 | **f** | 8 | 12 | **c** |
| 1 | 1 | **1** | 9 | 7 | **7** |
| 2 | 10 | **a** | 10 | 15 | **f** |
| 3 | 16 | **g** | 11 | 10 | **a** |
| 4 | 2 | **2** | 12 | 1 | **1** |
| 5 | 0 | **0** | 13 | 6 | **6** |
| 6 | 2 | **2** | 14 | 6 | **6** |
| 7 | 6 | **6** | 15 | 6 | **6** |

## 验证

用完整的前向传播验证（16字符）：

```
input='f1ag2026c7fa1666' (len=16)
  → <success> logit: 0.5000
  → <fail>    logit: 0.4000
  → argmax: <success> ✅ 胜出 margin=0.1
```

任何长度小于 16 的前缀都会让大量约束神经元激活（预激活 > 0），导致 success logit 瞬间跌到 $-10^{14}$ 数量级，输出 `<fail>`。

```
input='f1ag2026c7fa166' (len=15) → <fail> (succ = -3.88e13)
input='f1ag2026c7fa16'  (len=14) → <fail> (succ = -5.28e13)
...
input='f'               (len=1)  → <fail> (succ = -1.41e14)
```

## Flag

```
f1ag2026c7fa1666
```

## 小结 / Lessons Learned

1. **名字会骗人**：看似 "Causal Language Model"，实际是个伪装成 LLM 的 MLP 分类器。不要先入为主按 NLP 思路想。
2. **看权重不看结构**：输出层的 `-10^10` 超大惩罚值是明显的解题钥匙 —— 意味着对应 hidden 必须"严格为0"。
3. **无词嵌入 = 特征工程**：字符 ID 直接当数值用，本质上就是把字符当离散数值特征，这使得线性约束非常直接。
4. **SMT 求解器是 CTF 神器**：遇到整数约束 / 方程 / 不等式系统，Z3 往往比手写回溯快几个数量级，且正确性有保障。

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

上传的附件：

code.7z （5.50kb，2次下载）