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

发表于: 2天前 30

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

correy

2天前

看雪 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。

附件：

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

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 网络结构

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 就能读：

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 行非零：

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>：唯一依赖输入：

$logit [62] = 1 \cdot h_{0} - 1 0^{10} \sum_{i = 1}^{20} h_{i} - 376131.21875, h_{i} = ReLU (W_{i} \cdot x + b_{i})$

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

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

        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>)

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

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

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

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

(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。但真正漂亮的发现，是回代检查每条约束的松弛量：

约束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 ———

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

$W_{i} \cdot x = - b_{i} (i = 1, \dots, 20)$

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

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 个做最小二乘）直接解：

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，并用阻塞子句证明唯一性：

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 一致）精确复现：

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{} 包裹）：

flag{f1ag2026c7fa1666}

9. 复盘：这题在考什么

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

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

方法论上的关键点：

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

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

附：一键复现

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

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

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

收藏・0

免费・0

打赏