KCTF2026: 第九题：丑寅同墟·星海抉择-CTF对抗-看雪安全社区

KCTF2026: 第九题：丑寅同墟·星海抉择

发表于: 2026-8-22 12:58 41

KCTF2026: 第九题：丑寅同墟·星海抉择

Magic丶

2026-8-22 12:58

# ICTFForCausalLM —— 藏在模型权重里的后门校验器

> **题目类型**：AI / Misc（模型逆向）
> **附件**：`inference.py`、`model_def.py`、`ictf_model/{config.json, model.safetensors}`
> **Flag**：`flag{f1ag2026c7fa1666}`

---
很坏了，简单题不如不上 harness。（2m41s vs 11m vs 3m28s）
拆个外卖就已经 10+ 解完题了

---

## 0. 题目描述

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

一句话概括：这不是语言模型，是一个**被伪装成神经网络的口令校验器**。我们要做的是把「校验逻辑」从权重里解出来，再反解出唯一满足它的输入。

---

## 1. 读代码：这个「语言模型」根本不是语言模型

### 1.1 Tokenizer

```python
charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"   # 62 个字符
char2id = {c: i for i, c in enumerate(charset)}      # id 0..61
id2char[62] = "<success>"
id2char[63] = "<fail>"
vocab_size   = 64
pad_token_id = 0
```

两个关键点：

1. 词表里有两个**永远不可能被输入**的特殊 token —— `<success>` (62) 与 `<fail>` (63)。
   它们只能出现在**输出端**。这已经明示：模型的真实用途是「判对错」，不是「续写文本」。
2. 输入不足 16 字符时用 `pad_token_id = 0` 右填充，而 id 0 对应字符 `'0'`。
   也就是说 `"abc"` 和 `"abc0000000000000"` 在模型看来**完全等价**。

### 1.2 模型结构

```python
class ICTFForCausalLM(PreTrainedModel):
    def __init__(self, config):
        self.dense   = nn.Linear(16, 21, bias=True)     # max_position_embeddings -> hidden_size
        self.act     = nn.ReLU()
        self.lm_head = nn.Linear(21, 64, bias=True)     # hidden_size -> vocab_size

def forward(self, input_ids, **kwargs):
        x             = input_ids.float()               # ★ 没有 embedding！
        hidden_states = self.dense(x)
        hidden_states = self.act(hidden_states)
        logits        = self.lm_head(hidden_states)
        logits        = logits.unsqueeze(1)
        return {"logits": logits}
```

这里有三处「反常识」的设计，全是解题突破口：

| 反常识点 | 说明 |
| --- | --- |
| **没有 Embedding 层** | `input_ids.float()` 把 token **id 本身当成实数特征**直接喂进全连接层。于是整个网络对 id 向量 $x$ 是**分段线性**的，可以被精确求解。 |
| **没有 Attention / 位置编码** | `nn.Linear(16, 21)` 直接把「16 个位置」当成 16 维输入特征。序列维度被彻底拍平。 |
| **`logits.unsqueeze(1)`** | 输出形状变成 `[batch, 1, 64]`，所以 `inference.py` 里的 `logits[:, -1, :]` 取的就是那唯一一步的输出。整个模型**只输出一个 token**。 |

所以完整的数学形式极其简单（$x \in \mathbb{Z}^{16}$，$x_i \in [0, 61]$）：

$$
h = \mathrm{ReLU}(W_d x + b_d) \in \mathbb{R}^{21}_{\ge 0}, \qquad
\text{logits} = W_h h + b_h \in \mathbb{R}^{64}
$$

$$
\text{output} = \texttt{id2char}\big[\arg\max_k \text{logits}_k\big]
$$

---

## 2. 拆权重：找出后门判定式

`torch` 不是必需品 —— safetensors 是「8 字节小端头长度 + JSON 头 + 裸数据」的裸格式，用 `struct + numpy` 十几行就能解析：

```python
import json, struct, numpy as np

with open("model.safetensors", "rb") as f:
    blob = f.read()
hlen   = struct.unpack("<Q", blob[:8])[0]
header = json.loads(blob[8:8 + hlen])
body   = blob[8 + hlen:]

def tensor(name):
    m = header[name]; s, e = m["data_offsets"]
    return np.frombuffer(body[s:e], dtype=np.float32).reshape(m["shape"]).copy()

Wd, bd = tensor("dense.weight"), tensor("dense.bias")     # (21,16), (21,)
Wh, bh = tensor("lm_head.weight"), tensor("lm_head.bias") # (64,21), (64,)
```

### 2.1 `lm_head` —— 冒烟的枪

```
lm_head.weight (64, 21):
    第 62 行 = [ 1.0, -1e10, -1e10, ..., -1e10 ]     (1 个 +1，20 个 -1e10)
    其余 63 行 = 全 0                                 ★

lm_head.bias (64,):
    idx 0..61  = -10000.0   (全部普通字符)
    idx 62     = -376131.21875   (<success>)
    idx 63     =       0.4       (<fail>)
```

含义一目了然：

* **62 行以外的 `lm_head.weight` 全是 0** —— 62 个普通字符的 logit 恒为常数 `-10000`，`<fail>` 的 logit 恒为常数 `0.4`。它们**完全不受输入影响**。
* 只有 `<success>` 这一路是「活」的：

$$
\text{logit}_{62} \;=\; h_0 \;-\; 10^{10}\!\!\sum_{j=1}^{20} h_j \;-\; 376131.21875
$$

于是模型的行为坍缩成一个二元判定：**输出 `<success>` 当且仅当 $\text{logit}_{62} > 0.4$**，否则永远输出 `<fail>`。

### 2.2 把判定式拆成两个条件

因为 $h = \mathrm{ReLU}(\cdot) \ge 0$，那个 $-10^{10}$ 的巨大惩罚项是一道**硬闸门**：只要 $h_1..h_{20}$ 里有任何一个大于 0（最小非零增量是 1，因为权重全是整数），$\text{logit}_{62}$ 立刻掉到 $-10^{10}$ 量级，必然判 `<fail>`。

所以 `<success>` 需要**同时**满足：

**条件 A（20 条不等式）** —— 隐藏层第 1..20 维必须被 ReLU 全部压成 0：

$$
W_d[j] \cdot x + b_d[j] \;\le\; 0, \qquad j = 1, 2, \dots, 20
$$

**条件 B（1 条不等式）** —— 第 0 维必须足够大：

$$
h_0 = W_d[0]\cdot x + b_d[0] \;>\; 0.4 + 376131.21875 = 376131.61875
$$

代入 $b_d[0] = 311558.71875$：

$$
W_d[0]\cdot x \;>\; 64572.9
$$

而 $W_d[0]$ 与 $x$ **全是整数**，所以条件 B 等价于漂亮的整数形式：

$$
\boxed{\,W_d[0]\cdot x \;\ge\; 64573\,}
$$

>  **这里的 `.71875` / `.21875` / `.4` 三个小数是出题人故意留的「调音旋钮」**：
> 用它们把判定阈值卡死在 `64572.9` 这个非整数上，既保证唯一整数解通过，又让任何差 1 的邻近点被拒。

至此，"隐藏在模型中的秘密" 已经完全暴露：**这是一个 21 面体线性规划的可行性判定**。

---

## 3. 解法一：整数约束求解（严谨，可证唯一）

直接把条件 A + 条件 B 交给 SMT 求解器，并让它**穷举所有解**以证明唯一性：

```python
from z3 import Int, Solver, Sum, Or, sat

CHARSET = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
X = [Int(f"x{i}") for i in range(16)]
s = Solver()

for xi in X:                                     # 合法 token id 范围（含 pad=0）
    s.add(xi >= 0, xi <= 61)

for j in range(1, 21):                           # 条件 A: ReLU 全压到 0
    s.add(Sum([int(Wd[j][i]) * X[i] for i in range(16)]) + int(bd[j]) <= 0)

s.add(Sum([int(Wd[0][i]) * X[i] for i in range(16)]) >= 64573)   # 条件 B

while s.check() == sat:                          # 枚举全部解
    m = s.model()
    v = [m[X[i]].as_long() for i in range(16)]
    print("".join(CHARSET[i] for i in v))
    s.add(Or([X[i] != v[i] for i in range(16)])) # 排除已找到的解，继续找
```

输出：

```
f1ag2026c7fa1666
```

**只有这一个解**，第二轮 `s.check()` 直接返回 `unsat`。搜索空间 $62^{16} \approx 4.7\times10^{28}$ 被完整覆盖，因此这是**全局唯一**的口令，秒级出解。

---

## 4. 解法二：一眼看穿的线性方程组（更快）

拿到解之后回代，会发现一个漂亮的结构 —— 20 条不等式**全部取等号**：

```
j= 0  pre = 376131.71875      (只比阈值 376131.61875 高出 0.1)
j= 1  pre =      0.00000  <== 等号
j= 2  pre =      0.00000  <== 等号
...
j=20  pre =      0.00000  <== 等号
紧约束(取等)个数: 20 / 20，松弛约束: 0
```

这说明出题人是**先定 flag，再造权重**的：随机生成 $W_d[1..20]$（元素取值 $[-100, 100]$），然后令

$$
b_d[j] \;=\; -\,W_d[j]\cdot x^{*}, \qquad j = 1..20
$$

于是 $x^*$ 天然落在 20 个超平面的交点上。既然如此，我们完全可以**跳过不等式，直接当等式解**：

$$
W_d[1{:}21]\, x = -\,b_d[1{:}21] \quad\Longrightarrow\quad \text{20 个方程、16 个未知数}
$$

系数矩阵秩为 16（满列秩），超定但**相容**，因此解唯一：

```python
import numpy as np, sympy as sp

A = Wd[1:].astype(np.float64)      # (20, 16)
b = -bd[1:].astype(np.float64)     # (20,)
print("rank =", np.linalg.matrix_rank(A))          # -> 16

sol, *_ = np.linalg.lstsq(A, b, rcond=None)
print(np.round(sol))               # [15. 1. 10. 16. 2. 0. 2. 6. 12. 7. 15. 10. 1. 6. 6. 6.]
print("残差 =", np.linalg.norm(A @ sol - b))       # -> 1.4e-11 ≈ 0，说明方程组相容

# sympy 有理数精确求解，杜绝浮点误差质疑
Am = sp.Matrix([[sp.Integer(int(v)) for v in r] for r in Wd[1:]])
bm = sp.Matrix([sp.Integer(int(-v)) for v in bd[1:]])
print(sp.linsolve((Am, bm)))       # -> {(15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6)}
```

`sympy` 在**有理数域上精确求解**，结果是单点集，从代数上彻底排除浮点误差的可能。

解码：

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

$\Rightarrow$ **`f1ag2026c7fa1666`**（恰好 16 字符，无需 padding）

> ⚠️ 两条路径的严谨性不同：
> **解法二**建立在「不等式全取等」这个*猜测*上（先猜后验），跑得快但不自证唯一；
> **解法一**只使用题目给定的原始约束，在全空间上枚举，**证明了全局唯一性**。
> 两者结论完全一致，互为交叉验证。

---

## 5. 验证

不装 `torch` 也能验 —— 用 `numpy` 按 `model_def.py` 逐行复刻前向（`nn.Linear` 就是 $Wx+b$）：

```python
def forward(text, Wd, bd, Wh, bh):
    ids = [CHARSET.index(c) for c in text] + [0] * (16 - len(text))
    x   = np.asarray(ids, dtype=np.float32)
    h   = np.maximum(Wd @ x + bd, 0).astype(np.float32)     # dense + ReLU
    return (Wh @ h + bh).astype(np.float32)                 # lm_head
```

| 输入 | 预测输出 | `logit[62]` (`<success>`) | `logit[63]` (`<fail>`) |
|---|---|---:|---:|
| **`f1ag2026c7fa1666`** | **`<success>`** ✅ | **0.5000** | 0.4000 |
| `f1ag2026c7fa1665` (末位 −1) | `<fail>` | −6.47 × 10¹² | 0.4000 |
| `f1ag2026c7fa1667` (末位 +1) | `<fail>` | −3.53 × 10¹² | 0.4000 |
| `hello` | `<fail>` | −1.66 × 10¹⁴ | 0.4000 |
| `0000000000000000` (全 pad) | `<fail>` | −1.55 × 10¹⁴ | 0.4000 |

正确口令的胜出优势是 **0.5 vs 0.4 —— 仅仅 0.1**，而任何一位偏差都会让分数塌到 $-10^{12}$ 量级。这种「刀尖上的余量」正是人工构造后门的铁证，绝不可能来自训练。

也可以用官方的 `inference.py`（需 `torch` + `transformers`）验证：

```
$ python inference.py
[*] Loading tokenizer and Causal Language Model...
Enter your prompt: f1ag2026c7fa1666
<success>
```

---

## 6. Flag

```
flag{f1ag2026c7fa1666}
```

---

## 6.5 多解性分析：唯一解是被**证明**的，不是"没搜到"

`z3` 返回 `unsat` 只说明「在我给的那套约束下没找到别的」。可是那套约束（条件 A / 条件 B）是**我手工推导出来的** —— 万一推导本身有漏洞，枚举再干净也不算数。所以这里用六个互相独立的角度重新验证。

### ① 零手工推导：把完整模型原样塞进 SMT

不预设条件 A/B，把 `ReLU`、全部 64 路 logit、以及 `np.argmax` 的**平局取小下标**规则一起编码，用精确有理数求解：

```python
for j in range(21):                                   # ReLU 原样编码
    pre = Sum([RealVal(int(Wd[j][i])) * ToReal(X[i]) for i in range(16)]) + q(bd[j])
    s.add(H[j] == If(pre > 0, pre, RealVal(0)))

LOG = [Sum([q(Wh[k][j]) * H[j] for j in range(21)]) + q(bh[k]) for k in range(64)]
for k in range(62): s.add(LOG[62] >  LOG[k])          # 严格胜过 62 个字符
s.add(LOG[62] >= LOG[63])                             # 平局也算赢（argmax 取小下标）
```

```
找到解: f1ag2026c7fa1666
排除后再求解 -> unsat
==> 解的个数 = 1
```

同一问题再用**纯整数无损编码**跑一遍（把三个非整数常量放大 32 倍清分母）：

| 常量 | 精确值 | ×32 |
|---|---|---|
| `dense.bias[0]` | `9969879 / 32` | `9969879` ✔整数 |
| `lm_head.bias[62]` | `−12036199 / 32` | `−12036199` ✔整数 |
| `lm_head.bias[63]` | `13421773 / 2²⁵` | `12.8000001907…` → 取 `ceil` = `13` |

于是判定式化为一条纯整数不等式，且能反推出一个漂亮的闭式：

```
32·h₀ − 32·10¹⁰·S + (−12036199)  ≥  13          （S = Σ_{j≥1} h_j）

S = 0 时化简 =>  logit₆₂ = P₀ − 64572.5          （P₀ = W_d[0]·x）
```

代入 `P₀ = 64573` 得 `logit₆₂ = 0.5` —— 与实测**分毫不差**，反向印证了推导正确。整数编码同样给出：**解个数 = 1，排除后 unsat**。

### ② 惩罚项能不能被"补偿"掉？

我原先靠量级口算断言「`h[1..20]` 必须全为 0」。这一步交给求解器验：强制 `S ≥ 1`（至少一维没被压平），同时仍要求判定通过 —— 结果 **`unsat`**。

道理是硬的：`W_d` 全为整数 ⇒ `h_j` 的最小非零增量是 `1` ⇒ 罚分至少 `10¹⁰`；而 `h₀` 的**理论上限**只有 `≈ 2.1 × 10⁶`。差了四个数量级，无论如何补偿都翻不了盘。

### ③ Farkas 对偶证书：不依赖任何求解器的证明

前两条仍要相信 z3 的 `unsat`。这一条给出可手工复核的**构造性证明** —— 找一组 `λ_j ≥ 0` 使得：

```
Σ_{j=1..20} λ_j · W_d[j]  ==  W_d[0]
```

若存在，则对**任意**可行 `x`（连整数条件都不要）：

```
W_d[0]·x  =  Σ λ_j (W_d[j]·x)  ≤  Σ λ_j (−b_d[j])  =  常数
                  ↑ 可行性给出 W_d[j]·x ≤ −b_d[j]，且 λ_j ≥ 0
```

在有理数域上精确求解，证书确实存在，且：

| 复核项 | 结果 |
|---|---|
| `Σ λ_j·W_d[j] == W_d[0]` 精确成立 | ✔ |
| 所有 `λ_j ≥ 0` | ✔ |
| **LP 上界** `Σ λ_j·(−b_d[j])` | **64573** |
| `x*` 处实际取值 `W_d[0]·x*` | **64573** |
| 上界 == 取值 ⇒ `x*` 是 LP 最优 | ✔ |

关键在最后一步 —— **唯一性**。由互补松弛，任何达到上界的 `x` 必须在所有 `λ_j > 0` 的约束上取等号。而：

```
λ_j > 0 的约束集合 = [1,2,4,5,6,7,8,9,11,12,13,14,15,16,18,20]   共 16 条
该子集的秩 = 16 / 16                                            满秩
仅用这 16 条等式的解集 = {(15,1,10,16,2,0,2,6,12,7,15,10,1,6,6,6)}   单点
```

秩满 16 ⇒ 16 张超平面在 ℝ¹⁶ 中交于唯一点 ⇒ **最优面退化成一个点**。

> **这条结论的分量**：LP 上界 `64573` 与判定阈值 `≥ 64573` **恰好相等，一丝余量都不剩**。也就是说 —— 即使把整数条件**完全放开**、允许 `x` 取任意实数，能通过判定的点在整个 ℝ¹⁶ 里也只有 `x*` 这一个。整数域自然更不可能冒出第二解。
>
> 多解是被**数学排除**的，而不是搜索没找到。这份证明是纯线性代数，与 z3、与浮点实现都无关。

### ④ float32 会不会把结论算歪？

前面全在精确算术上推理，但模型真跑的是 `float32`。而 `logit₆₂` 的胜出余量只有 `0.1`，在 `376131` 量级上 ulp = `1/32 = 0.03125` —— **只有 3 个 ulp**。这么窄的余量必须验清楚舍入。

分区域论证（我最初那句"全程无舍入"说得太满，`h₀` 的精确性只在 `< 2¹⁹` 时成立，得分情形）：

| 步骤 | 结论 |
|---|---|
| `j=1..20` 的 `pre_j` | 全整数，\|部分和\| ≤ `61,498` < `2²⁴` → 对盒内**所有** `x` 无条件精确。⇒ `S` 是 0 还是 ≥1 被精确判定 |
| `P₀ = W_d[0]·x` | 整数，\|部分和\| ≤ `1,792,180` < `2²⁴` → 无条件精确 |
| `h₀` 情形 i：`h₀ < 2¹⁹` | ulp ≤ `1/32`，而 `.71875 = 23/32` → 精确 |
| `h₀` 情形 ii：`h₀ ≥ 2¹⁹` | `.71875` 可能舍入，但误差 ≤ `0.125`，而此时 `logit₆₂ ≥ 148157` → **判定不可能被翻转** |
| `logit₆₂` 合成（`S=0`） | `h₀` 与 `\|bh[62]\|` 比值≈1，Sterbenz 引理保证相减精确 → `logit₆₂ = P₀ − 64572.5` 精确 |

再做一次实证对拍：`float32` 前向 vs `Fraction` 精确前向，**5,001 组样本**（含 1,000 组刻意构造进舍入区、`P₀` 最高达 `1,432,811` 的样本）：

```
判定不一致的样本数 = 0
判定为 <success> 的样本 = ['f1ag2026c7fa1666']
```

### ⑤ Hamming 邻域穷举（真实 float32 前向）

不靠任何推理，直接暴力跑：

| 距离 | 穷举变体数 | 通过数 | 最高 `logit₆₂` | 最接近的变体 |
|---|---:|---:|---:|---|
| 1 | 976 | **0** | −2.72 × 10¹² | `f1ag2026c7fa1566` |
| 2 | 446,520 | **0** | −5.60 × 10¹¹ | `f1ag2025c7fa1566` |

44 万个近邻里，连一个够到 `0.4` 通过线的都没有 —— 最好的也还差 **11 个数量级**。

### ⑥ padding 歧义：会不会有第二个**字符串**映射到同一 id 向量？

这是个真实存在的坑：`pad_token_id = 0` 而 id 0 就是字符 `'0'`，所以若 `x*` 末尾带 0，那么短字符串和补零后的长字符串**都算对**，就会出现「多解」。

```
x*[15] = 6   （非 0）
x* 末尾连续 0 的个数 = 0
```

`x*` 末尾无 0 ⇒ 任何长度 `L < 16` 的输入都会补出至少一个尾随 0，与 `x*` 不符 ⇒ **恰好只有一个字符串**映射到 `x*`，长度必须是 16。此路不通。

### ⑦ 文件里还有没有第二处藏匿点？

```
文件大小 7,388 = 8 + 320(头) + 7,060(数据)      尾部多余字节 = 0
__metadata__ = {'format': 'pt'}                 头部无夹带字段
张量键 = 4 个，长度与 shape 全部吻合             无多余张量
NaN = 0   Inf = 0   次正规数 = 0                 无浮点编码花招
全模型非整数权重 = 3 个：
    dense.bias[0]    = 311558.71875
    lm_head.bias[62] = -376131.21875
    lm_head.bias[63] = 0.4000000059604645
```

那 3 个非整数就是阈值调音旋钮本身，此外文件内**无任何额外藏匿内容**。

> 顺带一个反过来的确认：`lm_head.weight` 前 62 行全零 ⇒ `logit[0..61] ≡ −10000`，而 `logit[63] ≡ 0.4 > −10000`。
> 所以 **`argmax` 永远落不到 `0..61` 上 —— 这个"语言模型"连一个字符都吐不出来**，输出只可能是 `<success>` / `<fail>`。从行为上它就不是 LM。

### 小结

| # | 角度 | 结论 |
|---|---|---|
| ① | 完整模型编码（有理数 + 整数两遍） | 解个数 = 1，排除后 `unsat` |
| ② | 强制 `S ≥ 1` 试图补偿 | `unsat`，差 4 个数量级 |
| ③ | **Farkas 对偶证书** | **实数域上 LP 上界 = 64573 = 阈值，最优面秩满 16 ⇒ 单点** |
| ④ | float32 舍入 | 分区域论证 + 5,001 组对拍，0 处不一致 |
| ⑤ | Hamming ≤2 邻域穷举 | 447,496 个变体，0 个通过 |
| ⑥ | padding 歧义 | `x*` 末尾无 0，字符串唯一 |
| ⑦ | 文件层面 | 无多余字节 / 张量 / NaN，无第二藏匿点 |

**`f1ag2026c7fa1666` 是唯一解。**

### 唯一一处仍属约定而非推导的地方

需要如实说明：模型能验证的**只有那 16 个字符**。charset 是 `[0-9a-zA-Z]`，**不含 `{`、`}`、`_`** —— 所以 `flag{...}` 这层包装**不可能**是模型校验的一部分，它来自 CTF 通用约定，而非从权重里推出来的。

如果平台的提交格式另有约定（例如直接交 16 位裸串、或换一个前缀），以平台为准。模型给出的硬事实只有一条：**`f1ag2026c7fa1666`**。

## 7. 复盘与要点总结

### 解题路线图

```
读 model_def.py
   └─ 发现无 embedding / 无 attention  ──►  模型对 token id 是分段线性的
   └─ 发现词表含 <success>/<fail>      ──►  这是校验器，不是 LM
        │
        ▼
解析 model.safetensors (struct + numpy，不需要 torch)
   └─ lm_head.weight 仅第 62 行非零   ──►  只有 <success> 一路是活的
   └─ 该行 = [1, -1e10 × 20]          ──►  -1e10 是硬闸门
        │
        ▼
判定式化简  logit62 = h0 - 1e10·Σh[1:] - 376131.21875 > 0.4
   ├─ 条件 A: h[1..20] == 0   ──►  20 条线性不等式
   └─ 条件 B: W_d[0]·x >= 64573
        │
        ├──► 解法一 z3 整数约束枚举  ──►  全局唯一解（严谨）
        └──► 解法二 观察到 20 条全取等 ──►  超定线性方程组 rank=16（快速）
        │
        ▼
                    f1ag2026c7fa1666
```

### 值得记住的几个点

1. **「没有 Embedding」是最大的红旗。** 正常的字符级 LM 一定有 `nn.Embedding`。把 `input_ids.float()` 直接送进 `Linear`，等于宣告「这个网络对输入是（分段）线性的」—— 而线性系统是可以被**精确求解**的，不需要梯度下降、不需要爆破。
2. **词表里的「不可输入 token」= 输出信道。** `<success>` / `<fail>` 在 `char2id` 里不存在，只在 `id2char` 里存在，这种不对称就是设计意图的签名。
3. **看权重的「形状」而不是「数值」。** 不必逐个数字细读 —— `lm_head.weight` 里 64 行有 63 行全 0、bias 里 62 个值完全相同，这种极端稀疏/常量结构一眼就能定位后门所在。真实训练出来的权重不会长这样。
4. **±1e10 是典型的「硬约束编码」手法。** 在神经网络里想表达「必须等于 0」，标准做法就是配一个巨大负权重，让违反者的 logit 直接爆炸。看到 `1e10` / `-1e9` 这类量级，基本可以断定是手工构造的约束而非训练产物。
5. **不必装 torch。** safetensors 格式极简（`u64 头长度 + JSON 头 + 裸 buffer`），`struct` + `numpy` 即可解析；`nn.Linear` 也就是一次 `W @ x + b`。手工复刻前向反而让每一步都完全透明、可控。
6. **善用「先猜后验」+「严谨证明」双路线。** 观察到结构规律（全取等）可以走捷径快速拿 flag；但要主张唯一性，还是得回到原始约束用 SMT/MILP 全空间枚举。两条路互相印证，才算真正做完。

### 附：一键复现

`solve.py` 与本文同目录，零依赖（`numpy` 必需，`sympy`/`z3` 可选）：

```bash
python3 solve.py                    # 默认读 ../题面/ictf_model
python3 solve.py /path/to/ictf_model
```

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

上传的附件：