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

# 丑寅同墟·星海抉择 Writeup

## 模型结构

分词器使用如下 62 个字符，并把字符直接映射为其下标：

```text
0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ
```

输入长度固定为 16，较短的输入会在末尾补编号 0。模型没有词嵌入层，16 个字符编号会作为浮点数直接进入两层全连接网络：

```text
z = W1 · x + b1
h = ReLU(z)
logits = W2 · h + b2
```

其中 `x` 有 16 维，隐藏层 `h` 有 21 维，输出层有 64 维。输出编号 62 对应 `<success>`，编号 63 对应 `<fail>`。

## 分析输出层

检查输出层权重可以发现，0 至 61 号普通字符的权重均为 0，偏置均为 `-10000`。`<fail>` 的权重也全部为 0，偏置为 `0.4`。只有 `<success>` 使用了隐藏层：

```text
W2[62] = [1, -10^10, -10^10, ..., -10^10]
b2[62] = -376131.21875
```

所以成功类别的分数为：

```text
logit_success = h[0] - 10^10 · (h[1] + ... + h[20]) - 376131.21875
```

隐藏层第 1 至 20 行的权重、偏置都是整数，输入编号也是整数。一旦这些行中有正数，经过 ReLU 后至少为 1，成功分数就会被减去至少 `10^10`，不可能成为最大值。因此正确输入必须让 20 个拒绝单元全部关闭：

```text
W1[i] · x + b1[i] <= 0,  i = 1, 2, ..., 20
```

这 20 行就是模型中保存秘密的主体。进一步观察可见，它们构造了 20 个经过目标点的超平面。令所有拒绝单元恰好位于 ReLU 的分界点，得到整数线性方程组：

```text
W1[1:21] · x = -b1[1:21]
```

系数矩阵为 `20 × 16`，秩为 16，因此该方程组在实数范围内也只有一个解。使用整数精确运算求解得到：

```text
x = [15, 1, 10, 16, 2, 0, 2, 6, 12, 7, 15, 10, 1, 6, 6, 6]
```

代回全部 20 个方程后，左侧都严格等于 0。所有编号也都位于分词器的合法范围内。按字符表还原为：

```text
f1ag2026c7fa1666
```

其中编号 0 位于字符串中间，对应字符 `0`。由于它后面仍有非零编号，该位置不是末尾补位。

## 模型验证

把恢复出的编号送回完整模型后，第 1 至 20 个隐藏单元全部为 0，输出分数为：

```text
logit_success = 0.5
logit_fail    = 0.4
```

最终最大输出编号为 62，解码结果为 `<success>`。

## Exp

```python
#!/usr/bin/env python3

import sys

import numpy as np
import sympy as sp
from safetensors.numpy import load_file

CHARSET = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
SUCCESS_ID = 62

def main():
    if len(sys.argv) != 2:
        raise SystemExit("usage: python exp.py <model.safetensors>")

state = load_file(sys.argv[1])

weights = state["dense.weight"][1:]
    biases = state["dense.bias"][1:]
    assert np.array_equal(weights, np.rint(weights))
    assert np.array_equal(biases, np.rint(biases))

matrix = sp.Matrix(weights.astype(np.int64).tolist())
    target = sp.Matrix((-biases).astype(np.int64).tolist())
    assert matrix.rank() == 16

solutions = sp.linsolve((matrix, target))
    assert len(solutions) == 1
    exact = next(iter(solutions))
    assert all(value.q == 1 for value in exact)

ids = np.array([int(value) for value in exact], dtype=np.int64)
    assert np.all((0 <= ids) & (ids < len(CHARSET)))
    assert matrix * sp.Matrix(ids.tolist()) == target

x = ids.astype(np.float32)
    hidden = np.maximum(
        state["dense.weight"] @ x + state["dense.bias"],
        0.0,
    )
    logits = state["lm_head.weight"] @ hidden + state["lm_head.bias"]
    assert np.all(hidden[1:] == 0)
    assert int(np.argmax(logits)) == SUCCESS_ID

flag = "".join(CHARSET[index] for index in ids)
    print(flag)

if __name__ == "__main__":
    main()
```

# flag
```text
f1ag2026c7fa1666
```

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