[原创] KCTF 2026 第九题-CTF对抗-看雪安全社区｜专业技术交流与安全研究论坛

# 0x01 模型分析

`model_def.py` 中定义的模型非常简单：

```python
class ICTFForCausalLM(PreTrainedModel):
    config_class = ICTFConfig

def __init__(self, config):
        super().__init__(config)
        self.dense = nn.Linear(config.max_position_embeddings, config.hidden_size, bias=True)
        self.act = nn.ReLU()
        self.lm_head = nn.Linear(config.hidden_size, config.vocab_size, bias=True)

def forward(self, input_ids, **kwargs):
        x = input_ids.float()
        hidden_states = self.dense(x)
        hidden_states = self.act(hidden_states)
        logits = self.lm_head(hidden_states)
        logits = logits.unsqueeze(1)
        return {"logits": logits}
```

模型的计算流程如下：

```text
输入字符串
    ↓
转换为字符 ID
    ↓
补齐为长度 16 的向量
    ↓
Linear(16 → 21)
    ↓
ReLU
    ↓
Linear(21 → 64)
    ↓
得到 64 个输出分数
    ↓
最终选择分数最高的 token    
```

Tokenizer 的字符表为：

```text
0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ
```

对应关系为：

```text
0-9  →  ID 0-9
a-z  →  ID 10-35
A-Z  →  ID 36-61
```

另外还有两个特殊 token：

```text
62 → <success>
63 → <fail>
```

输入长度不能超过 16。长度不足 16 时，会使用 token ID `0` （对应字符 `'0'`）进行右填充。
因此，模型最终处理的是一个长度为 16 的整数向量：

$$
x=(x_0,x_1,\dots,x_{15})
$$

其中每个元素满足：

$$
0\le x_i\le61
$$

---

# 0x02 权重分析

`model.safetensors` 中只有四组参数：

| 参数 | 形状 | 含义 |
|---|---:|---|
| `dense.bias` | `(21,)` | 第一层偏置 |
| `dense.weight` | `(21,16)` | 第一层权重 |
| `lm_head.bias` | `(64,)` | 输出层偏置 |
| `lm_head.weight` | `(64,21)` | 输出层权重 |

观察 `lm_head` 后，可以发现它几乎完全由人工构造的常数组成。

## 普通字符

对于 token `0` 到 `61`：

```text
weight 全部为 0
bias = -10000
```

因此这些 token 的分数始终为：

$$
\operatorname{logit}_k=-10000
$$

## <fail>

对于 token `63`：

```text
weight全部为 0
bias = 0.4
```

因此：

$$
\operatorname{logit}_{fail}=0.4
$$

## <success>

对于 token `62`：

```text
W_lm[62] = [1, -1e10, -1e10, ..., -1e10]
b_lm[62] = -376131.21875
```

因此：

$$
\operatorname{logit}_{success}
=
h_0
-10^{10}(h_1+h_2+\cdots+h_{20})
-376131.21875
$$

---

# 0x03 理论推导

第一层的输出为：

$$
z=Wx+b
$$

对于第 $i$ 个神经元：

$$
z_i=W_i\cdot x+b_i
$$

ReLU 的定义为：

$$
h_i=\operatorname{ReLU}(z_i)=\max(0,z_i)
$$

也就是说：

- 当 $z_i<0$ 时，$h_i=0$；
- 当 $z_i>0$ 时，$h_i=z_i$。

---

`<success>` 的分数为：

$$
\operatorname{logit}_{success}
=
h_0
-10^{10}(h_1+h_2+\cdots+h_{20})
-376131.21875
$$

由于 ReLU 的输出不会小于 0，所以：

$$
h_i\ge0
$$

对于 $i=1,\dots,20$，权重、偏置和输入 ID 都是整数，因此如果 $h_i>0$，则至少有：

$$
h_i\ge1
$$

这样就会产生至少一个惩罚项：

$$
-10^{10}h_i\le-10^{10}
$$

而第 0 个神经元的最大值只有大约 $1.79\times10^6$，远远小于 $10^{10}$。因此，只要 $h_1,\dots,h_{20}$ 中有任何一个大于 0，`<success>` 的分数就一定会低于 `<fail>`。

所以必须满足：

$$
h_1=h_2=\cdots=h_{20}=0
$$

根据 ReLU 的定义，这等价于：

$$
W_i\cdot x+b_i\le0,
\qquad i=1,\dots,20
$$

---

当后 20 个神经元全部关闭时：

$$
\operatorname{logit}_{success}
=
h_0-376131.21875
$$

要让 `<success>` 的分数超过 `<fail>` 的 `0.4`，需要：

$$
h_0-376131.21875>0.4
$$

因此：

$$
h_0>376131.61875
$$

第 0 个神经元的偏置为：

$$
b_0=311558.71875
$$

所以：

$$
W_0\cdot x+311558.71875>376131.61875
$$

整理得到：

$$
W_0\cdot x>64572.9
$$

因为 $W_0\cdot x$ 是整数，所以：

$$
W_0\cdot x\ge64573
$$

因此，成功条件可以总结为：

$$
\begin{cases}
W_i\cdot x+b_i\le0,
& i=1,\dots,20\\
W_0\cdot x\ge64573
\end{cases}
$$

---

# 0x04 求解输入

```python
import numpy as np
from safetensors.numpy import load_file
from z3 import Int, Or, Solver, sat

MODEL_PATH = "./model.safetensors"
CHARSET = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"

weights = load_file(MODEL_PATH)

dense_w = np.rint(weights["dense.weight"]).astype(int)
dense_b = np.rint(weights["dense.bias"]).astype(int)

x = [Int(f"x{i}") for i in range(16)]

solver = Solver()

for value in x:
    solver.add(value >= 0)
    solver.add(value <= 61)

for i in range(1, 21):
    expression = sum(
        int(dense_w[i, j]) * x[j]
        for j in range(16)
    ) + int(dense_b[i])

solver.add(expression <= 0)

target_expression = sum(
    int(dense_w[0, j]) * x[j]
    for j in range(16)
)

solver.add(target_expression >= 64573)

result = solver.check()
print("result:", result)

if result == sat:
    model = solver.model()

solution = [
        model.evaluate(value).as_long()
        for value in x
    ]

print("input IDs:", solution)

prompt = "".join(CHARSET[i] for i in solution)
    print("answer:", prompt)
```

运行结果为：

```text
result: sat
input IDs: [15, 1, 10, 16, 2, 0, 2, 6,
            12, 7, 15, 10, 1, 6, 6, 6]

answer: f1ag2026c7fa1666
```

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