[原创]第九题：丑寅同墟·星海抉择 Writeup-CTF对抗-看雪安全社区

[原创]第九题：丑寅同墟·星海抉择 Writeup

发表于: 2026-8-22 20:12 59

[原创]第九题：丑寅同墟·星海抉择 Writeup

wufake

2026-8-22 20:12

题目描述

附件提供了一个简单的字符级"因果语言模型" ICTFForCausalLM 以及模型权重：

模型接受长度不超过 16 个字符的字符串作为输入
预测下一个输出字符
目标：分析模型代码与权重，找出隐藏的 flag

文件结构：

model_def.py — 模型定义
inference.py — 推理脚本（输入 prompt，打印预测字符）
ictf_model/config.json + model.safetensors — 模型配置和权重
题目要求.txt

初步分析

1. 字符集

ICTFTokenizer（model_def.py#L6-L40）：

self.charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"

只有 62 个字母数字字符，没有 {、}、_、- 等符号。因此 flag 只包含数字和大小写字母。

特殊 token：

id=62 → <success>（验证成功）
id=63 → <fail>（验证失败）

2. 模型结构 — "Causal LM"名不副实

查看 forward 函数（model_def.py#L68-L74）：

def forward(self, input_ids, **kwargs):
    x = input_ids.float()                          # [batch, 16]
    hidden_states = self.dense(x)                   # Linear(16, 21)
    hidden_states = self.act(hidden_states)         # ReLU
    logits = self.lm_head(hidden_states)            # Linear(21, 64)
    logits = logits.unsqueeze(1)                    # [batch, 1, 64]
    return {"logits": logits}

关键发现：没有词嵌入层！ input_ids 直接被转成 float 送入第一层。也就是说字符 ID（0~61 的整数）本身被当作数值特征使用，而不是作为索引去 lookup embedding。

这根本不是"因果语言模型"，而是一个两层 MLP 分类器：

x (16个字符ID) → Linear(16→21) → ReLU → Linear(21→64) → 输出64类logits

深度权重分析

使用 safetensors 加载权重，重点看输出层 lm_head：

Output[ 0..61] (字符): 所有权重=0, bias=-10000
Output[62]  <success>: w[0]=1.0,  w[1..20]=-10_000_000_000,  bias=-376131.22
Output[63]  <fail>:    所有权重=0,  bias=0.4

这是本题最核心的设计！解读如下：

输出	默认值	与隐藏层关系
普通字符	-10000	永远不可能胜出
`<fail>`	0.4	与隐藏层无关，恒定输出 0.4
`<success>`	-376131.22	仅 `hidden[0]` 贡献 +1×，其余 `hidden[1..20]` 每个贡献 -100亿×

推导获胜条件

要让 <success> 成为 argmax，必须满足：

隐藏层 1~20 的 ReLU 输出必须全部为 0：
- 否则任何一个 hidden[i]>0 都会让 success 减去 100 多亿
- ReLU(h)=0 ⇨ 预激活值≤0：
  $\sum_{j = 0}^{15} W [i, j] \cdot x [j] + b [i] \leq 0 (i = 1..20)$
隐藏层 0 的输出必须足够大：
- success logit = hidden[0] − 376131.22 > fail logit = 0.4
- ReLU(h)=h（只需 h>0），即：
  $\sum_{j = 0}^{15} W [0, j] \cdot x [j] + b [0] \geq 376132$

建模为约束满足问题（CSP）

把条件整理成标准形式，变量为 $x_{0}, x_{1}, \dots, x_{15}$ （每个取值 0..61 的整数，对应字符 ID）：

$⎩ ⎨ ⎧ \sum_{j = 0}^{15} W [i, j] \cdot x_{j} \leq - b [i], \sum_{j = 0}^{15} W [0, j] \cdot x_{j} \geq 64574, x_{j} \in {0, 1, \dots, 61}, i = 1..20 (20 条约束) (因为 b_{0} = 311558.72, 376132 - 311558.72 \approx 64573.3) j = 0..15$

暴力枚举 $6 2^{16} \approx 4.76 \times 1 0^{28}$ 不可行。使用 Z3 SMT 求解器（整数线性算术）在 0.58 秒内求解完成。

Z3 求解脚本

import numpy as np
from z3 import *

# dense_w[21,16], dense_b[21] 从 safetensors 导出
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)

# 20 条约束：hidden[1..20] 预激活 <= 0
for i in range(1, 21):
    expr = sum(int(round(dense_w[i,j])) * x[j] for j in range(16))
    s.add(expr + int(round(dense_b[i])) <= 0)

# success 阈值约束
expr0 = sum(int(round(dense_w[0,j])) * x[j] for j in range(16))
s.add(expr0 >= 64573)

print(s.check())     # sat
m = s.model()
x_vals = [m[x[j]].as_long() for j in range(16)]
print(x_vals)
# [15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6]

还原 Flag

charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
flag = ''.join(charset[v] for v in x_vals)
print(flag)

逐字符映射：

位置	x 值	字符	位置	x 值	字符
0	15	f	8	12	c
1	1	1	9	7	7
2	10	a	10	15	f
3	16	g	11	10	a
4	2	2	12	1	1
5	0	0	13	6	6
6	2	2	14	6	6
7	6	6	15	6	6

验证

用完整的前向传播验证（16字符）：

input='f1ag2026c7fa1666' (len=16)
  → <success> logit: 0.5000
  → <fail>    logit: 0.4000
  → argmax: <success> ✅ 胜出 margin=0.1

任何长度小于 16 的前缀都会让大量约束神经元激活（预激活 > 0），导致 success logit 瞬间跌到 $- 1 0^{14}$ 数量级，输出 <fail>。

input='f1ag2026c7fa166' (len=15) → <fail> (succ = -3.88e13)
input='f1ag2026c7fa16'  (len=14) → <fail> (succ = -5.28e13)
...
input='f'               (len=1)  → <fail> (succ = -1.41e14)