签到题：辰时·钟鸣破晓

附件

https://pan.baidu.com/s/1N3YqHD0DZkMhNsmBUDxykQ?pwd=gy39 提取码: gy39

解压后阅读 PUBLIC_INFO.txt 可知：

KCTF 2026 - Rosetta Calibration

Final EXE SHA256:
caaa1c964b15d9b3250be0dc64412e5f64c29e297a971c226e8dd705d6b87e67

Public valid pair:
Name   : CAAA1C964B15D9B3
Serial : $/.;-):,(-#!%*-&?+@

Target:
Find the unique Serial for Name KCTF.

字符串侦察

提取 kctf_rosetta.exe 字符串

strings -n 5 kctf_rosetta.exe

只 import 了 GetStdHandle/ReadFile/WriteFile/ExitProcess —— 纯控制台 I/O，无网络、无反调试、无壳，可以放心静态分析；
Sixteen symbols. Sixteen meanings. 印证“16 符号 ↔ 16 数值”的映射设计；
三种失败提示对应三道关卡：Invalid name format（Name 格式）、The inscription cannot be translated（符号查表失败/重复）、Calibration rejected（最终比对失败）；
提示用 ReadFile 逐字符读入（后面反汇编可证实），Name 与 Serial 分别缓存在栈上不同区域。

完整反汇编与逐段分析

objdump -d -M intel kctf_rosetta.exe

main：读入 Name

程序用 GetStdHandle 拿到 stdin/stdout，打印横幅后提示 Name : ，随后逐字节 ReadFile 循环：

140001100:  movzx  eax, byte [rsp+0x30]      ; 读到的字符
140001105:  cmp    eax, 0xd                   ; '\r' → 丢弃继续读
14000110a:  cmp    eax, 0xa                   ; '\n' → 结束输入
14000110f:  lea    ecx, [r15+1]
140001113:  cmp    ecx, 0x27                  ; 上限 39
14000111b:  mov    [rsp+rdx+0x80], al         ; name_buf[r15++] = ch

Name 存到 [rsp+0x80]，长度上限 39；
遇 \r 忽略、遇 \n 结束（兼容 CRLF）。

Name 合法性校验

14000123e:  lea    eax, [rbx-0x21]   ; eax = len - 33
140001241:  cmp    eax, -0x20        ; 无符号比较 0xFFFFFFE0
140001244:  jae    ok                ; len-33 ∈ [-32,-1] 即 len∈[1,32] 才放行
             ; 否则打印 "[-] Invalid name format." 退出

140001270:  movzx  ecx, byte [rsp+rax+0x80]
140001278:  add    cl, -0x21
14000127b:  cmp    cl, 0x5e          ; (c-0x21) 无符号 < 0x5E
14000127e:  jae    invalid           ; → 每个字符必须是 0x21..0x7E（可打印 ASCII）

Name = 1~32 个可打印 ASCII 字符。KCTF（4 字符）合法。

Serial 结构解析：dash 位置由 `0x4210` 决定

140001295:  mov    ebp, 0x4210       ; 掩码
1400012c5:  cmp    r14d, 0xe         ; i <= 14 ?
1400012c9:  ja     translate_it
1400012cb:  bt     ebp, r14d         ; 测试掩码第 i 位
1400012cf:  jb     1400012b0

1400012b0:  cmp    byte [rsp+r14+0x50], 0x2d   ; '-' ?
1400012b6:  jne    reject            ; 掩码位必须 是 '-'

translate_it:
1400012d1:  movzx  ecx, byte [rsp+r14+0x50]
1400012d7:  call   0x140001520       ; translate(sym) → nibble
1400012dc:  cmp    eax, 0xf
1400012df:  ja     reject            ; 必须是合法符号（≤15）
1400012e6:  ...  bt edi, eax         ; 该 nibble 是否已用过？
1400012ed:  jb     reject            ; 重复 → 拒绝（"排列"约束）
1400012ef:  or     edi, edx          ; 记录到位图
1400012f7:  mov    [rsp+rcx+0x40], al; nibbles[n++] = v

140001304:  cmp    r15d, 0x10        ; 恰好 16 个 nibble
14000130a:  cmp    edi, 0xffff       ; 且 0..15 全部出现（排列！）

0x4210 = 0100_0010_0001_0000₂，置位的是第 4、9、14 比特。用公开样本验证：$/.;-):,(-#!%*-&?+@ 的第 4、9、14 位（0 起数）恰为 -,-,-。其余 16 个位置（0-3, 5-8, 10-13, 15-18）依次翻译成 nibble，必须构成 0–15 的排列。

translate()：符号 → nibble（含一个 XOR 陷阱）

0x140001520  translate(cl):
    bl = cl
    eax = base_lookup(cl)        ; 调 0x140001540
    ecx = (bl == 0x28) ? 1 : 0   ; 字符是 '(' ?
    return eax ^ ecx             ; ← 陷阱：'(' 的结果要异或 1

0x140001540  base_lookup(cl):
    cl -= 0x21
    if ((uint8)cl > 0x1f) return -1       ; 字符不在 0x21..0x40 → 非法
    return dword_table[cl]                ; 表在 0x140002000

derive()：Name → 期望的 16 个 nibble

0x1400013e0  derive(rcx=name, edx=len, r8=out16):
    state[16] = xmmword[0x140002080]      ; 初始状态（见 §5）
    if (len == 0) goto emit
    r9 = 0; acc = 0
    for (i = 0; i < len; i++) {
        a = i & 15
        c = name[i]
        v = (c >> 4) ^ c                  ; 高低半字节异或
        acc += v
        j = (v ^ r9) & 15
        swap(state[a], state[j])
        r9 += 3                           ; 每轮扭动的步进
    }
emit:
    out[k] = state[(acc + k) & 15], k = 0..15
    ; 其中 out[8] 写作 state[(acc&15)^8]、out[15] 写作 state[(acc-1)&15]，
    ; 但对 4 比特值 XOR 8 ≡ +8 (mod 16)、-1 ≡ +15 (mod 16)，
    ; 故统一为 out[k] = state[(acc+k) mod 16]

对应原始指令（节选，证明 +3 步进与异或细节）：

14000140e:  shr    edi, 4           ; c>>4
140001411:  xor    edi, esi         ; v = c ^ (c>>4)
140001413:  add    eax, edi         ; acc += v
140001415:  xor    edi, r9d         ; v ^= r9
140001418:  and    edi, 0xf         ; j = v & 15
140001420-140001428:                 ; swap(state[i&15], state[j])
14000142e:  add    r9d, 0x3         ; r9 += 3

最终判定：SSE 整块比较

140001312:  lea    rcx, [rsp+0x80]      ; name
14000131f:  mov    edx, ebx             ; len
140001321:  call   0x1400013e0          ; derive(name,len,[rsp+0x30])
140001326:  movdqa xmm0, [rsp+0x40]     ; Serial 解析出的 16 个 nibble
14000132c:  pcmpeqb xmm0, [rsp+0x30]    ; 与 derive 输出逐字节比较
140001332:  pmovmskb eax, xmm0
140001336:  xor    eax, 0xffff          ; 全等时为 0
14000133b:  jne    reject
             ; → "[+] Calibration accepted. Key correct!"

算法重建与唯一性论证

完整算法（伪代码）

serial_of(name):
    # 1) 交换混淆
    state = [0..15];  r = 0;  acc = 0
    for i, c in enumerate(name):
        v  = c ^ (c >> 4)          # 字节高低半字节异或
        acc = (acc + v) mod 2^32
        j  = (v ^ r) mod 16
        swap(state[i mod 16], state[j])
        r  = (r + 3) mod 2^32
    # 2) 轮转输出
    nibbles[k] = state[(acc + k) mod 16]     for k in 0..15
    # 3) nibble → 符号（§5 双射表），再在 4/9/14 位插入 '-'
    symbols = [inv_table[v] for v in nibbles]
    return symbols[0:4] + '-' + symbols[4:8] + '-' \
         + symbols[8:12] + '-' + symbols[12:16]

为什么 Serial 唯一

校验逻辑强制：长度 19、第 4/9/14 位为 -、其余 16 符号经双射表映射后必须是 0–15 的排列且逐位等于 derive(name)；
derive(name) 对给定 name 是确定性的（无随机、无时间、无环境依赖——import 表只有 I/O 四个函数可为证）；
符号表是双射：每个 nibble 值有且仅有一个符号表示。三者结合 → 对每个合法 Name，被接受的 Serial 存在且唯一。keygen 就是确定性正算，无需搜索/爆破。

Keygen 脚本

#!/usr/bin/env python3

TABLE = {
    '!': 4,  '#': 7,  '$': 12, '%': 1,  '&': 9,  '(': 2,   # '(' 查表 3 ^ 1 = 2
    ')': 11, '*': 14, '+': 6,  ',': 13, '.': 8,  '/': 10,
    ':': 15, ';': 5,  '?': 0,  '@': 3,
}
INV = {v: k for k, v in TABLE.items()}
DASH_AT = (4, 9, 14)

def derive(name: bytes):
    """0x1400013e0：交换混淆 + 轮转输出，返回期望的 16 个 nibble"""
    state = list(range(16))
    r, acc = 0, 0
    for i, c in enumerate(name):
        v = c ^ (c >> 4)
        acc = (acc + v) & 0xFFFFFFFF
        j = (v ^ r) & 0xF
        a = i & 0xF
        state[a], state[j] = state[j], state[a]
        r = (r + 3) & 0xFFFFFFFF
    return [state[(acc + k) & 0xF] for k in range(16)]

def serial_of(name: str) -> str:
    nibbles = derive(name.encode())
    assert sorted(nibbles) == list(range(16)), "内部错误：非排列"
    s = [INV[v] for v in nibbles]
    out, it = [], iter(s)
    for pos in range(19):
        out.append('-') if pos in DASH_AT else out.append(next(it))
    return ''.join(out)

if __name__ == "__main__":
    assert serial_of("CAAA1C964B15D9B3") == "$/.;-):,(-#!%*-&?+@"
    print("Name  : KCTF")
    print("Serial:", serial_of("KCTF"))

可得：

Name  : KCTF
Serial: &/@$-,*?:-!#)%-;+(.

第九题：丑寅同墟·星海抉择

附件

https://pan.baidu.com/s/1RoZmSSePCqE3EQQPM7ERmA?pwd=y7xf

附件分析

题目要求

附件提供一个字符级语言模型 ICTFForCausalLM 及其权重：

模型接受长度 ≤ 16 个字符的字符串作为输入，预测一个输出字符；
目标是分析模型代码与权重，找出隐藏在模型中的秘密，恢复正确的 flag。

模型结构（`model_def.py`）

class ICTFTokenizer:
    charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
    # id 0~61: 字符；id 62: <success>；id 63: <fail>

    def encode(self, text, ...):
        input_ids = [self.char2id[c] for c in text]   # 不做 embedding！
        input_ids.extend([0] * (16 - len(input_ids))) # 右侧补 0 至长度 16

class ICTFForCausalLM(PreTrainedModel):
    def __init__(self, config):                    # hidden_size=21
        self.dense = nn.Linear(16, 21, bias=True)  # Linear(16 → 21)
        self.act = nn.ReLU()
        self.lm_head = nn.Linear(21, 64, bias=True)# Linear(21 → 64)

    def forward(self, input_ids, **kwargs):
        x = input_ids.float()           # ← 关键：token id 直接当浮点数用
        hidden_states = self.dense(x)   # W1·x + b1
        hidden_states = self.act(hidden_states)  # ReLU
        logits = self.lm_head(hidden_states)     # W2·h + b2
        return {"logits": logits.unsqueeze(1)}

模型虽然套着 PreTrainedModel 的壳（伪装成因果语言模型），实际只是一个两层 MLP：x →(Linear+ReLU)→ h →(Linear)→ logits，对整个 16 维输入只产出一个 64 维 logits（推理时取 logits[:, -1, :]，由于 unsqueeze(1) 只有一个位置，等价于对整个输入做一次分类）。
没有 embedding 层——输入就是字符 token id 本身（0~63 的整数）转 float。这意味着模型对输入是逐维线性的，完全可以手工解方程，不需要任何神经网络攻击技巧。
字符集只有 [0-9a-zA-Z] 共 62 个字符 + <success>/<fail> 两个特殊 token。flag 本身就是那个让模型输出 <success> 的输入字符串。

推理脚本（inference.py）

outputs = model(input_ids)
next_token_id = torch.argmax(logits[:, -1, :], dim=-1)  # 取 argmax
predicted_char = tokenizer.id2char.get(next_token_id, "<unk>")

输入一个字符串，模型告诉你 <success> / <fail> / 某个字符。目标是让 argmax 落在 id 62（<success>）。

解题过程

解包权重

model.safetensors 只有 4 个张量，直接手工解析（不依赖 torch）：

张量	形状	说明
dense.weight (W1)	21×16	整数权重：第 0 行数值很大（数千），第 1~20 行是 ±100 内的整数
dense.bias (b1)	21	b1[0]≈311558，其余为 ±3500 内的整数
lm_head.weight (W2)	64×21	几乎全零！只有第 62 行非零
lm_head.bias (b2)	64	全部为 −10000，除了 b2[62]≈−376131、b2[63]=0.4

lm_head.weight 的第 62 行（对应 <success>）：

o62 = [1.0, -1e10, -1e10, -1e10, ..., -1e10]   # h0 系数 +1，h1~h20 系数 -1e10

其余 63 行全为零。这就是“隐藏在模型中的秘密”,输出层被人为构造成一个判决电路。

翻译成数学约束

设输入向量为 x（16 维，每维是 0~63 的 token id，右侧补 0），隐藏层 pre-activation 为 z = W1·x + b1，则各类的 logits 为：

id 0~61：logits = 0·h − 10000 = −10000（恒定）
id 63（<fail>）：logits = 0.4
id 62（<success>）：logits = z0⁺ − 10¹⁰·(z1⁺ + z2⁺ + … + z20⁺) − 376131.2，其中 zᵢ⁺ = max(zᵢ, 0)

要让 argmax = 62，需要 logits[62] > −10000 且 > 0.4，这要求同时满足：

$$ \begin{cases} z_j = W_1[j]\cdot x + b_1[j] \le 0, & j = 1, 2, \ldots, 20 \quad \text{（否则 } -10^{10}\text{ 的系数直接压死）}\[4pt] z_0 = W_1[0]\cdot x + b_1[0] > 366131.2 & \text{（使 } h_0 \text{ 足够大）} \end{cases} $$

对应题面“五人同时操作，任何一人出错都将导致系统重置”：16 个输入维度、20+1 个约束必须全部同时成立，任何一位字符错误都会让某个 z_j (j≥1) 变正而坠入 <fail>。“歧路之中，又有歧焉”。

为什么可以“解方程”而不是搜索

直接搜索是 64¹⁶ ≈ 8×10²⁸ 的空间，不可行。但注意两个特征：

b1[1:] 全是整数，而 W1[1:] 的元素也是整数——出题人构造时把偏置设成了在目标解处恰好取等（W1[j]·x_flag + b1[j] = 0），这样正解恰好卡在 ReLU 的拐点上，任何扰动都会向正方向越界；
于是 20 个不等式在解处全部退化为等式，得到一个 20×16 的超定线性方程组：

$$ W_1[1!:!21] \cdot x = -b_1[1!:!21] $$

直接做最小二乘即可：

import numpy as np

A = W1[1:]                 # (20, 16)
t = -b1[1:]                # (20,)
x, res, rank, sv = np.linalg.lstsq(A, t, rcond=None)

# 残差 ~5.5e-12 —— 完全一致，说明方程组相容，解就是设计点
xi = np.round(x).astype(int)
# [15  1 10 16  2  0  2  6 12  7 15 10  1  6  6  6]  全部落在 0~63

残差为 5.5e-12（即浮点精度内的零），四舍五入后得到精确整数解，且每一维都合法落在 0~63：

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

token id 映射回字符串

charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
''.join(charset[v] for v in xi)

得到：

f1ag2026c7fa1666

恰好 16 个字符（满长度输入，无 padding）。

验证

用 float32 精确复现 forward pass 验证（与 inference.py 中 torch 的计算完全等价）：

def predict(s):
    x = np.array([charset.index(c) for c in s] + [0]*(16-len(s)), dtype=np.float32)
    pre = W1 @ x + b1
    h = np.maximum(pre, np.float32(0)).astype(np.float32)
    logits = (W2 @ h + b2).astype(np.float32)
    return int(np.argmax(logits)), logits, pre

nid, logits, pre = predict('f1ag2026c7fa1666')

输出：

input   : f1ag2026c7fa1666
predict : <success> (id 62)
logit62 : 0.500    logit63: 0.400    max-other: -10000.000
hidden pre-activation: max(z1..z20) = 0.000000   # 20 个约束全部恰好取等

唯一性检验：对 16 个位置逐一做 ±1 的扰动（共 32 次测试），没有任何一个扰动后的输入仍输出 <success>——正解严格唯一，印证“歧路之中，又有歧焉，吾不知所之”。

完整 EXP

#!/usr/bin/env python3
import numpy as np, json, struct

# ---- 1. 手工解析 safetensors（无需 torch/transformers）----
with open('ictf_model/model.safetensors', 'rb') as f:
    data = f.read()
n = struct.unpack('<Q', data[:8])[0]
header = json.loads(data[8:8+n].decode())
base = 8 + n
def get(name):
    v = header[name]; s, e = v['data_offsets']
    return np.frombuffer(data[base+s:base+e], dtype='<f4').reshape(v['shape']).astype(np.float64)

W1, b1, W2, b2 = get('dense.weight'), get('dense.bias'), get('lm_head.weight'), get('lm_head.bias')

# ---- 2. 逆向约束 ----
# lm_head 仅第 62 行(<success>)非零: [1, -1e10 × 20]，b2 全 -10000（除 62/63）
# 故 argmax=62  ⟺  W1[j]·x + b1[j] ≤ 0 (j=1..20) 且 W1[0]·x + b1[0] > 366131.2
# b1 为整数构造，正解处全部取等 → 超定方程组直接最小二乘
x, res, *_ = np.linalg.lstsq(W1[1:], -b1[1:], rcond=None)
assert np.linalg.norm(W1[1:] @ x + b1[1:]) < 1e-9, '方程组不相容'
xi = np.round(x).astype(int)
assert all(0 <= v <= 63 for v in xi), '解不在 token id 范围内'

# ---- 3. id → 字符 ----
charset = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
flag = ''.join(charset[v] for v in xi)
print('[+] recovered:', flag)

# ---- 4. float32 复现 forward pass 验证 ----
W1f, b1f, W2f, b2f = (t.astype(np.float32) for t in (W1, b1, W2, b2))
xx = xi.astype(np.float32)
h = np.maximum(W1f @ xx + b1f, np.float32(0)).astype(np.float32)
logits = (W2f @ h + b2f).astype(np.float32)
nid = int(np.argmax(logits))
name = {62: '<success>', 63: '<fail>'}.get(nid) or charset[nid]
print('[*] argmax id:', nid, '->', name)
assert nid == 62
print('[+] FLAG:', flag)

运行结果：

[+] recovered: f1ag2026c7fa1666
[*] argmax id: 62 -> <success>
[+] FLAG: f1ag2026c7fa1666

看雪 2026 KCTF