前言

本题由 Claude Opus 5 (xhigh effort) + CC 完成, 用时约 2 分钟

权重里的后门

KCTF · ICTFForCausalLM 题解

flag: f1ag2026c7fa1666

一个只有 1,765 个参数的字符级"语言模型"，没有 embedding，没有 attention。
它把 flag 藏在 lm_head 的第 62 行和一组线性不等式里 —— 整道题的本体，
是一道解唯一最优的线性规划。

1. 这个模型里没有"语言模型"

model_def.py 的前向传播只有三行有效逻辑，而第一行就足够反常：

def forward(self, input_ids, **kwargs):
    x = input_ids.float()                     # <- token id 直接当浮点特征
    hidden_states = self.dense(x)             # Linear(16 -> 21)
    hidden_states = self.act(hidden_states)   # ReLU
    logits = self.lm_head(hidden_states)      # Linear(21 -> 64)
    return {"logits": logits.unsqueeze(1)}

没有 embedding 层。input_ids 被 .float() 直接当成浮点向量喂进全连接层 ——
token id 本身的数值就是特征。于是整个网络退化成 16 维整数格点上的一个分段线性函数：

h      = ReLU(Wd @ x + bd)        # Wd: 21x16   bd: 21
logits = Wl @ h  + bl             # Wl: 64x21   bl: 64
pred   = argmax(logits)

输入是长度 16 的字符串（不足则用 id 0，也就是字符 0 右填充），字符集 62 个，
所以 x ∈ {0,…,61}^16。目标是让 argmax 落在 id 62，也就是 <success>。

2. lm_head 的 64 行里，只有一行是活的

把 model.safetensors 解析开（8 字节小端长度 + JSON 头 + 裸 float32，不装 torch 也能读），
lm_head 的结构一眼就露馅了：

64 行里有 63 行权重全零 —— 它们的 logit 是常数，跟输入毫无关系。
普通字符恒为 −10000，<fail> 恒为 0.4。唯一随输入变化的只有第 62 行。
于是整道题坍缩成一个标量比较：

logit[0..61] = -10000                                   # 常数
logit[63]    = 0.4                                      # 常数, <fail>
logit[62]    = h0 - 1e10 * (h1 + h2 + ... + h20) - 376131.21875

# <success> 胜出  <=>  logit[62] > 0.4

3. 把 argmax 翻译成不等式

ReLU 保证 h >= 0，而 h1…h20 前面挂着 −1e10 的系数。这两件事一撞，条件就被逼死了：
只要任何一个 hj 取到哪怕最小的正数，logit 就会被打到 −1e10 量级，永无翻身之日。于是：

条件 A（可行性） —— 20 个隐藏单元必须被 ReLU 全部压成 0：

W[j] · x + b[j] <= 0        (j = 1…20)

条件 B（最优性） —— 第 0 个单元必须够大，盖过 <fail> 的 0.4：

h0 = W[0] · x + b[0] > 0.4 + 376131.21875 = 376131.61875

这里已经能闻到线性规划的味道了：20 条线性约束 + 1 个线性目标。
出题人把可行性写进了 −1e10，把最优性写进了那个脏兮兮的 bias 常数。

4. 20 个方程，16 个未知数，残差 1.2e−11

先赌一把最干净的可能：条件 A 全部取等。dense.weight[1:] 是 20×16 的整数矩阵
（值域 ±100），秩为 16 —— 超定方程组。超定方程组一般无解，但最小二乘一跑，
残差是 1.24 × 10⁻¹¹：

A, b = Wd[1:], bd[1:]                  # 20x16, 20
x = np.linalg.lstsq(A, -b, rcond=None)[0]
# residual = 1.2373599e-11
x = np.round(x).astype(int)
# array([15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6])
assert np.all(A @ x + b == 0)          # 精确成立

完全相容。这说明出题人是先选定 flag、再反算 bias 的。
解出来的 16 个分量全是 0–61 的整数，按字符集 0123456789abc…XYZ 一映射：

[15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6]
  f  1   a   g  2  0  2  6   c  7   f   a  1  6  6  6

21 个隐藏单元的计算结果

下面 20 行的 Σw·x + b 精确等于 0 —— 不是约等于，是二进制意义上的 0，ReLU 输出全灭。
而 h0 冲到 376131.71875，刚好越过 376131.61875 的门槛，余量只有 0.1：

完整的 21×16 权重矩阵

注意 h0 那一行：数值比其余 20 行大两个数量级 —— 它不是特征提取器，是目标函数。

          [0]   [1]   [2]   [3]   [4]   [5]   [6]   [7]   [8]   [9]  [10]  [11]  [12]  [13]  [14]  [15]
 char       f     1     a     g     2     0     2     6     c     7     f     a     1     6     6     6
 id        15     1    10    16     2     0     2     6    12     7    15    10     1     6     6     6
-------------------------------------------------------------------------------------------------------
 h0      3012  1679    78 -1143  1231  5574  2091  1452 -3472  1990    17  1987   109  3758  1295  -492
 h1        61    23   -13    90    58     0    47    62    -6   -89    67    41    13    64    -8   -71
 h2       -58   -33   -90   -58    44  -100    54    -7   100     9    43    -9    81    -3     2   -52
 h3       -37   -58    19     6   -92    76   -37    56   -20    29   -93   -27    80   -55   -17   -28
 h4       -51    96   -81    12     9    31    21   -91    -6   -90    22   -15   -58    83   -37   -24
 h5        91    37    18   -14   -32    84    86   -70    48    77     3    44    65   100   -21    18
 h6       -47    49   100   -72    10    42    42    67     9   -23    61    35    53    35   -35   -14
 h7        40   -85     4   -12    51    52   -36    -9   -95    68   -95    55   -70   100    22    39
 h8        63    48    25   -69    69    87     5    65    14    52   -50    80   -45   -24    58   100
 h9        38    75   -33   -45    74   100   -50    99   -93   -42   -23   -52    45    14   -19   -57
 h10      -94    84   -38   -15   -57    84    70    50     2   -39   -17   -79     1     1    -8   -95
 h11      -68   -50    24   -89   -36     0    19    22    -1    86    89   -43   -35   -15    60   -74
 h12      -73    18    93    92    12    -4   -28     8   -53    56    34    70    42    36   -99   -92
 h13      -92    -2    43    91    70   -16   -18    51   -87   -73   -28    45    63     1   -32    59
 h14       68   -35   -70    13    -5    89   -41   -35   -98    65   -82    68  -100    54    -4   -18
 h15       79    77   -14   -31    11    20    71   -71   -98     6    20    29   -18    94    95    78
 h16       39   -57    61   -73   -56    49    32    12    10    59   -58    31    52   -44    41     5
 h17       91   -40    -9    18    20   -85   -68    26   -82   -24   -91    60    58    92   -74   -91
 h18       97   -12   -20   -64    45    44    79    59    96    80    58   -61    69   -40    55   -27
 h19      -78   -79    19    12   -13    87   -46    -5   -62    16    49   -25    69    92   -76    54
 h20       68    74   -54    30   -91    86    61    85   -20   -29    75  -100   -41   -91    82    -4

5. 唯一性：这其实是一道线性规划

到这里很容易犯一个错 —— "20 个约束、秩 16、实数解唯一，所以 flag 唯一"。
这个论证是错的。 条件 A 是 <= 0 而不是 = 0，可行域是一个 16 维多面体，不是一个点。
逐坐标跑 LP 量一下它的尺寸：

for i in range(16):
    lo = linprog( e_i, A_ub=A, b_ub=-b, bounds=[(0,61)]*16).fun
    hi = linprog(-e_i, A_ub=A, b_ub=-b, bounds=[(0,61)]*16).fun

# 逐维跨度 max(hi - lo) = 31.145  ->  可行域是实心多面体, 不是单点

最宽的一维跨度有 31.1，多面体里塞着大量整点。真正把解锁死的，是被忽略的条件 B：

再用 MILP 把 16 个坐标 × 61 个取值共 976 种情况逐一固定做可行性测试，另解数量：0。

回头看那两个丑陋的常数就通透了：dense.bias[0] = 311558.71875 和
lm_head.bias[62] = -376131.21875 不是训练出来的，是手工配的 ——
专门把判定门槛卡在 64572.9，让唯一的整数可行解恰好压线通过。
这个模型从头到尾没"学"过任何东西，它是一台被硬编码的约束求解器。

6. 完整脚本

不需要 torch，也不需要 transformers：

import json, struct, numpy as np

def load(path):
    with open(path, 'rb') as f:
        n    = struct.unpack('<Q', f.read(8))[0]
        hdr  = json.loads(f.read(n))
        blob = f.read()
    out = {}
    for k, v in hdr.items():
        if k == '__metadata__':
            continue
        s, e = v['data_offsets']
        out[k] = np.frombuffer(blob[s:e], dtype=np.float32).reshape(v['shape'])
    return out

W = load('ictf_model/model.safetensors')
Wd, bd, bl = W['dense.weight'], W['dense.bias'], W['lm_head.bias']

A,  b  = Wd[1:], bd[1:]      # 条件 A: 这 20 个单元必须被 ReLU 压成 0
w0, b0 = Wd[0],  bd[0]       # 条件 B: 这个单元必须盖过 <fail>

x = np.round(np.linalg.lstsq(A, -b, rcond=None)[0]).astype(int)
assert np.all(A @ x + b == 0)
assert w0 @ x + b0 > bl[63] - bl[62]

charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
print("".join(charset[i] for i in x))      # -> f1ag2026c7fa1666

验证

用 float32 精确复现原模型前向。留意相邻输入的失败方式 ——
h0 未必不够大，往往是条件 A 先崩，两个条件必须同时成立：

直接跑官方的 inference.py 也可以：

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

Flag

f1ag2026c7fa1666

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