丑寅同墟·星海抉择WriteUp

Flag：f1ag2026c7fa1666

一、题目

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

附件：

二、读代码：这不是"语言模型"

2.1 Tokenizer

self.charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"   # 62 个字符 -> id 0..61
self.id2char[62] = "<success>"
self.id2char[63] = "<fail>"
self.vocab_size = 64
self.pad_token_id = 0

两个关键点：

1. 词表里有 <success> / <fail> 两个特殊 token（id 62 / 63），但它们不在 charset 里 —— 即用户无法输入，只能被模型「输出」。这就是"隐藏的秘密"的入口：题目要找的显然是能让模型吐出 <success> 的那个输入。
2. pad_token_id = 0，而 id 0 对应的字符恰好是 '0'。所以「短输入 + padding」和「末尾补 '0' 的 16 字符输入」在模型看来完全一样。（好在最终 flag 末尾是 '6'，不存在长度歧义。）

2.2 前向过程

def forward(self, input_ids, **kwargs):
    x = input_ids.float()                 # (1,16) 的 id 序列，直接当浮点向量
    hidden_states = self.dense(x)         # Linear(16 -> 21) + bias
    hidden_states = self.act(hidden_states)   # ReLU
    logits = self.lm_head(hidden_states)  # Linear(21 -> 64) + bias
    return {"logits": logits.unsqueeze(1)}

没有 embedding、没有位置编码、没有注意力。「字符级 Causal LM」只是个包装，实质是一个把 16 维整数向量映射到 64 维 logits 的两层 MLP：

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

其中 $x\in \{0,1,\dots ,61{\}}^{16}$ 是字符 id 向量。注意 id 是被当作数值直接送进线性层的 —— 这意味着整个模型对输入是「算术」而非「查表」，为后面列方程铺平了道路。

三、读权重：后门全写在 lm_head 上

本机没装 safetensors / transformers，直接手工解析即可 —— safetensors 格式非常简单：8 字节小端头长度 + JSON 头 + 裸张量数据。

import json, struct, numpy as np

raw = open("ictf_model/model.safetensors", "rb").read()
n = struct.unpack("<Q", raw[:8])[0]
header = json.loads(raw[8:8+n].decode())
blob = raw[8+n:]
T = {k: np.frombuffer(blob[m["data_offsets"][0]:m["data_offsets"][1]],
                      dtype=np.float32).reshape(m["shape"]).copy()
     for k, m in header.items() if k != "__metadata__"}
# dense.weight (21,16)  dense.bias (21,)  lm_head.weight (64,21)  lm_head.bias (64,)

看到的权重完全不像训练出来的，而是手工构造的：

3.1 lm_head.weight (64×21)

64 行里只有第 62 行非零，其余 63 行全是 0：

lm_head.weight[62] = [1.0, -1e10, -1e10, -1e10, ..., -1e10]     # 首项 1，其余 20 项均为 -1e10
lm_head.weight[63] = [0, 0, ..., 0]
lm_head.weight[i]  = [0, 0, ..., 0]                             # i = 0..61

3.2 lm_head.bias (64)

bias[0..61] = -10000.0          （全部相同）
bias[62]    = -376131.21875     ← <success>
bias[63]    = 0.4               （精确值 0.4000000059604645，float32 的 0.4）

3.3 于是三类 logits 完全解耦

所以这个「模型」根本不预测字符：默认永远输出 <fail>（0.4 > -10000），只有当唯一的可变项 logit${}_{62}$ 超过 0.4 时才输出 <success>。 它是一个伪装成 LM 的 flag 校验器。

dense 层的 21 个隐藏单元也因此分工明确：

• 单元 0：贡献正向"分数"，权重量级达数千（如 3012, 1679, 5574, -3472, 3758）
• 单元 1~20：权重是 $[-100,100]$ 内的随机整数，作为校验位 —— 前面挂了 $-10^{10}$ 的巨大负系数

四、把"输出 <success>"翻译成数学约束

要求 $\arg \max =62$，即 ${\mathrm{logit}}_{62}>0.4$：

$h_0-10^{10}{\sum }_{i=1}^{20}{h}_i-376131.21875>0.4$

由于 ReLU 保证 $h_i\ge 0$，而系数是 $-10^{10}$，只要有任何一个 $h_i\ge 1$（$W$、$b$、$x$ 全为整数，$h_i$ 非零就必然 $\ge 1$），左边立刻变成 $-10^{10}$ 量级，绝无可能大于 0.4。于是条件精确拆成两部分：

(a) 20 条「ReLU 必须死掉」的不等式（$i=1,\dots ,20$）：

$h_i=0⟺W_d^{(i)}\cdot x+b_d^{(i)}\le 0⟺\underset{\text{整数系数线性不等式}}{\underbrace{W_d^{(i)}\cdot x\le -b_d^{(i)}}}$

(b) 1 条「分数必须过线」的不等式：

$h_0=W_d^{(0)}\cdot x+b_d^{(0)}>0.4+376131.21875$

代入 $b_d^{(0)}=311558.71875$：

$W_d^{(0)}\cdot x>0.4+376131.21875-311558.71875=64572.9$

因为 $W_d^{(0)}$ 与 $x$ 都是整数，等价于

$W_d^{(0)}\cdot x\ge 64573$

其中

$W_d^{(0)}=[3012,1679,78,-1143,1231,5574,2091,1452,-3472,1990,17,1987,109,3758,1295,-492]$

至此题目变成一个纯整数规划问题：求 $x\in \{0,\dots ,61{\}}^{16}$，满足 20 条线性不等式且 $W_d^{(0)}\cdot x\ge 64573$。

顺带说明为什么不能硬来：

• 爆破：搜索空间 $62^{16}\approx 4.8\times 10^{28}$，不可行。
• 梯度下降 / 对抗样本法：目标函数被 $-10^{10}$ 与 ReLU 死区切成一片平坦的悬崖，梯度几乎处处无信息，且要求整数解，实践中收敛不了。
• 只解 20 条不等式：不够。$Ax\le b$ 的可行域里存在大量整数点（实验中随手就能捞出几百个），必须叠加 (b) 那条门槛才能锁定唯一解。

五、求解：整数线性规划（ILP）

把 (b) 作为最大化目标、(a) 作为约束，用 scipy.optimize.milp（后端 HiGHS）求解：

import numpy as np
from scipy.optimize import milp, LinearConstraint, Bounds

CHARSET = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
dw, db = T["dense.weight"].astype(float), T["dense.bias"].astype(float)
hb = T["lm_head.bias"].astype(float)

c0 = dw[0]                              # 目标：最大化 dw[0] @ x
A, b = dw[1:], -db[1:]                  # 约束：A @ x <= b   (20 条)
THRESH = hb[63] - hb[62] - db[0]        # = 64572.9

res = milp(c=-c0,
           constraints=LinearConstraint(A, -np.inf, b),
           bounds=Bounds(0, 61),
           integrality=np.ones(16))     # 16 个变量全为整数

x = np.round(res.x).astype(int)
print(int(c0 @ x), (A @ x - b).astype(int))          # 64573  [0]*20
print("".join(CHARSET[i] for i in x))                # f1ag2026c7fa1666

输出：

status : Optimal
max dw[0]@x    = 64573.0            <- 门槛是 64572.9，刚好越线 0.1
20 条约束松弛量 = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]   <- 全部取等
ids   = [15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6]
flag  = f1ag2026c7fa1666

两个信号说明这就是出题人埋的那个点：

1. 最优值 恰好 64573，只比门槛 64572.9 高 0.1 —— 显然是构造出来的临界值；
2. 20 条不等式在最优点全部取等号，而 $\mathrm{rank}(A)=16$（满秩）—— 说明 $Ax=b$ 的实数解本就唯一，出题人是先定 flag，再反推 bias 让它落在所有 ReLU 的边界上。

手算核对 $W_d^{(0)}\cdot x^{\text{*}}$：

合计 64573 ✅，故 $h_0=64573+311558.71875=376131.71875$，${\mathrm{logit}}_{62}=376131.71875-376131.21875=0.5>0.4$ ✅

六、唯一性证明

最大值 = 64573，门槛 = 64572.9，因此任何成功解的 $W_d^{(0)}\cdot x$ 都必须恰好等于 64573。为了证明这样的点只有一个，对每个变量位 $j$、每个取值 $v\ne x_j^{\text{*}}$ 各解一次 MILP（共 16×61 = 976 次，几十秒）：

for j in range(16):
    for v in range(62):
        if v == x[j]: continue
        lo, hi = np.zeros(16), np.full(16, 61.0)
        lo[j] = hi[j] = v                      # 把第 j 位钉死在 v
        r = milp(c=-c0, constraints=LinearConstraint(A, -np.inf, b),
                 bounds=Bounds(lo, hi), integrality=np.ones(16))
        assert not (r.status == 0 and -r.fun > THRESH)     # 全部通不过门槛

976 次求解的最优值全部 ≤ 64572.9，即：把任意一位改成任意别的字符后，无论其余 15 位怎么取，都不可能再触发 <success>。

结论：在全部 $62^{16}\approx 4.8\times 10^{28}$ 种输入中，f1ag2026c7fa1666 是唯一能让模型输出 <success> 的输入。

七、验证

本机未装 transformers，无法直接跑 inference.py，于是用两个 nn.Linear 精确复刻 ICTFForCausalLM.forward（数值路径完全一致，float32）：

dense, head = nn.Linear(16, 21), nn.Linear(21, 64)
# ... 从 safetensors 拷入 4 个张量 ...
def predict(s):
    ids = [CHARSET.index(c) for c in s] + [0] * (16 - len(s))     # 与 tokenizer 的 padding 一致
    h = torch.relu(dense(torch.tensor([ids], dtype=torch.float32)))
    logits = head(h).unsqueeze(1)
    return int(torch.argmax(logits[:, -1, :], dim=-1))

注意第 2、3、4 行：h[0] 比正确答案还大，却依然失败 —— 因为破坏了某个校验位，$-10^{10}\sum h_i$ 项直接把 logit 打到 $-10^{12}$ 以下。这正说明 20 条校验约束才是主锁，h[0] 只是最后那把用来锁定唯一性的钳子。

浮点安全性：float32 对 $\le 2^{24}$ 的整数精确，h[0] ≈ 3.76e5 远在范围内；dense.bias[0] = 311558.71875 = 311558 + 23/32 是二进制精确值，故 logit62 = 0.5 无舍入误差，与 0.4 的判别稳健。

八、反推出题人的构造

从权重可以完整还原出题流程：

1. 定 flag $x^{\text{*}}$（16 个字符，id 向量 $[15,1,10,16,2,0,2,6,12,7,15,10,1,6,6,6]$）；
2. 随机生成 20 行 $[-100,100]$ 的整数权重 $W_d^{(\mathrm{1..20})}$，令 $b_d^{(i)}=-W_d^{(i)}\cdot x^{\text{*}}$ —— 这使 flag 恰好落在 20 个 ReLU 的零边界上（$h_i=0$），任何偏离都会顶起至少一个 $h_i$；
3. 随机生成量级更大的 $W_d^{(0)}$ 与 $b_d^{(0)}=311558.71875$，算得 $h_0(x^{\text{*}})=376131.71875$；
4. 令 lm_head.bias[62] = -(h_0(x^*) - 0.5) = -376131.21875，使正确输入的 logit62 恰为 0.5，压过恒定的 logit63 = 0.4，余量仅 0.1；
5. lm_head.weight[62] 设为 $[1,-10^{10},\dots ,-10^{10}]$ 把校验位放大成一票否决；其余行清零、bias 统一压到 −10000，让普通字符永不出头。

一句话："模型权重"就是被编码成线性代数的一道 flag 校验，而 ReLU 边界 + 巨大负系数把「校验失败」实现成了「不可能翻盘的 logit」。

九、Flag

f1ag2026c7fa1666

模型字符集为 [0-9a-zA-Z]，不含 {、}、_，故若平台要求包裹格式，提交 flag{f1ag2026c7fa1666}。

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