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

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 模型结构

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}

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

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

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

$\text{output}=\text{id2char}\left[\arg {\max }_k{\text{logits}}_k\right]$

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

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

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,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 求解器，并让它穷举所有解以证明唯一性：

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\times 10^{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[\mathrm{1..20}]$（元素取值 $[-100,100]$），然后令

$b_d[j]=-W_d[j]\cdot x^{\ast },j=\mathrm{1..20}$

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

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

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

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 在有理数域上精确求解，结果是单点集，从代数上彻底排除浮点误差的可能。

解码：

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

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

5. 验证

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

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

正确口令的胜出优势是 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 的平局取小下标规则一起编码，用精确有理数求解：

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

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

关键在最后一步 —— 唯一性。由互补松弛，任何达到上界的 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¹⁹ 时成立，得分情形）：

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

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

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

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

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。

小结

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 可选）：

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

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