SUCTF2026_flumel&West

SU_flumel

首先给各位做这个题的师傅们道个歉，第一次给XCTF分站赛这么大型的赛事出题，力求不出问题的最后还是出问题了。在与infobahn的师傅们交流该题的时候发现附件存在部分设计失误，故选择更换附件，很抱歉给各位师傅带来了不好的体验。

​

这个题目总体来说是比较传统的安卓逆向，AI浪潮的到来让我思考如何能在不增加人工解题难度的同时有效抑制AI agent对题目的解出，所以这次出题也是一个尝试，但是好像有些弄巧成拙了。

题目整体逻辑是dart层+Hermes字节码层+Native层进行验证

flutter用了dart vm 3.11.1，blutter恢复符号之后，关于flag的逻辑验证在ctfverify.dart中

整体逻辑是先进行RC4的密钥生成，然后进行自定义的RC4 Warp函数加密，之后传入bundles里的cache.snap.bundle到Native层的qk9v进行验证

build RC4 key还原逻辑如下：

def build_rc4_key():
    arr = [0x1f, 0x3b, 0x3f, 0x03, 0x00, 0x0a, 0xcf,
           0xe5, 0xe7, 0xe8, 0xca, 0xcc, 0xd2]
    out = []
    for i, v in enumerate(arr):
        mask = (9 * i + 0x4b) & 0xff
        out.append(v ^ mask)
    return ''.join(chr(x) for x in out)

还原之后的key是：TobeorNottobe

然后是去还原RC4 warp的逻辑，使用blutter提供的addNames.py还原libapp.so的符号，结合ctfverify.dart还原出大致逻辑如下：

int j = 0;
int rot = 0xc3;   

for (int i = 0; i < 256; i++) {
  int k1 = key[(5 * i + 1) % key.length];
  int k2 = key[(3 * i + 7) % key.length];

  rot = ((rot << 1) | (rot >> 7)) & 0xff;   

  j = (j + S[i] + k1 + (k2 ^ rot) + i) & 0xff;
  swap(S[i], S[j]);
}

List<int> process(List<int> input) {
  List<int> out = [];
  int i = 0;
  int j = 0;
  int extra = 157;

  for (int idx = 0; idx < input.length; idx++) {
    int b = input[idx];

    i = (i + 1) & 0xff;
    int si = S[i];

    j = (j + si + 11 * i) & 0xff;
    swap(S[i], S[j]);

    int t1 = (S[i] + si + i + j) & 0xff;
    int a  = S[t1];

    int t2 = (a ^ extra) & 0xff;
    int b2 = S[t2];

    int extraRot = ((extra << 3) | (extra >> 5)) & 0xff;

    int outByte = (b ^ b2 ^ S[(b2 ^ extraRot) & 0xff] ^ ((13 * i) & 0xff)) & 0xff;

    out.add(outByte);
    extra = extraRot;
  }
  return out;
}

Native层的逻辑在qk9v这个函数里，然后对于Hermes字节码的有一个加载调用，但只是运行，并没有传参进去，我在编译最后的apk的时候没有把这段预先设计好的加密链路设计到整个的加密流程中，不过对于这个Hermes字节码我们可以看一下。

使用https://github.com/bongtrop/hbctool进行反汇编，这里我们的hbc字节码是hbc90，该仓库的pull requests里提供了90的反编译源码，把其加入到仓库里编译就好了。

反汇编出来的hasm有大概44w行，其实是加了一些静态的无用业务逻辑，形如

function f0(v) {
  var t = ((v + 7) ^ 13) & 0xffff;
  return (t * 4 + 17) & 0xffff;
}
if (false) { p = f0(p); }
function f1(v) {
  var t = ((v + 36) ^ 44) & 0xffff;
  return (t * 41 + 58) & 0xffff;
}
if (false) { p = f1(p); }
function f2(v) {
  var t = ((v + 65) ^ 75) & 0xffff;
  return (t * 78 + 99) & 0xffff;
}
if (false) { p = f2(p); }
function f3(v) {
  var t = ((v + 94) ^ 106) & 0xffff;
  return (t * 115 + 140) & 0xffff;
}
if (false) { p = f3(p); }
function f4(v) {
  var t = ((v + 123) ^ 137) & 0xffff;
  return (t * 152 + 181) & 0xffff;
}

在诸多无用业务逻辑中是能看到一段真实的加密的，还原出来大概是

(function (global) {
  function aa(value) {
    value = value >>> 0;
    value ^= (value << 13) >>> 0;
    value ^= value >>> 17;
    value ^= (value << 5) >>> 0;
    return value >>> 0;
  }

  function bb() {
    var obf = [
      0x25, 0x17, 0x05, 0x11, 0xe4, 0xf5, 0xa6, 0xd2, 0xd8, 0xca, 0xb2, 0xe2,
      0xc5, 0xc1, 0xc4, 0x82, 0x87, 0x81, 0xae, 0xbc, 0xb9, 0xb3, 0xa9, 0xa0,
      0xa3, 0x86, 0x9a, 0xb9, 0x9c, 0x92, 0x2e, 0x3a, 0x3d, 0x20, 0x21
    ];
    var out = new Array(obf.length);
    for (var i = 0; i < obf.length; i++) {
      out[i] = (obf[i] ^ ((0x6d + i * 5) & 0xff)) & 0xff;
    }
    return out;
  }

  function cc(size, key) {
    var sbox = new Array(size);
    var stream = new Array(size * 2);
    var seed = 0x6d5a56b9;
    var i;

    for (i = 0; i < key.length; i++) {
      seed = aa(seed ^ ((key[i] + i * 131) >>> 0));
    }

    for (i = 0; i < size * 2; i++) {
      seed = aa((seed + 0x9e3779b9 + i * 17) >>> 0);
      stream[i] = seed >>> 0;
    }

    for (i = 0; i < size; i++) {
      sbox[i] = i;
    }
    for (i = size - 1; i >= 1; i--) {
      var idx = stream[i] % (i + 1);
      var tmp = sbox[i];
      sbox[i] = sbox[idx];
      sbox[idx] = tmp;
    }
    return { sbox: sbox, stream: stream };
  }

  function asa(bytes) {
    var out = "";
    for (var i = 0; i < bytes.length; i++) {
      var h = (bytes[i] & 0xff).toString(16);
      if (h.length === 1) {
        h = "0" + h;
      }
      out += h;
    }
    return out;
  }

  function tbp(block) {
    var key = bb();
    var tables = cc(16, key);
    var sbox = tables.sbox;
    var stream = tables.stream;
    var shuffled = new Array(16);
    var out = new Array(16);
    var n;

    for (n = 0; n < 16; n++) {
      shuffled[n] = block[sbox[sbox[n]]] & 0xff;
    }

    var first = stream[16];
    out[0] = (shuffled[0] ^ (first & 0xff) ^ key[0] ^ 0x42) & 0xff;

    for (n = 1; n < 16; n++) {
      var val = stream[16 + n];
      var spice = (val >>> ((n & 3) * 8)) & 0xff;
      var k = key[(n * 7 + 3) % key.length];
      out[n] = (out[n - 1] ^ shuffled[n] ^ spice ^ k ^ ((n * 29) & 0xff)) & 0xff;
    }

    return asa(out);
  }

  global.__j1 = function (input) {
    if (!input || input.length !== 16) {
      return "";
    }
    var block = new Array(16);
    for (var i = 0; i < 16; i++) {
      block[i] = input[i] & 0xff;
    }
    return tbp(block);
  };
})(this);

这其实是一个用固定 key 派生一个固定sbox和固定伪随机流，然后对 16 字节输入做双置换重排，再做链式异或混合的自定义算法。但是题目设计并没有将其加入最终的加密验证链路之中。

我们去到q9kv函数中分析Native逻辑，首先可以看到大量的反调试，如果尝试动态hook后面的runtime派生出的真正的AES的key和IV的话就需要过一下。

后面是一个标准的AES-128 CBC加密，并没有魔改

可以看到初始化了key和iv，但并不是真正最后参与运算的，这里最后的key和iv是和Hermes bundle runtime绑定，传入对应的bundle进行key和iv的派生

最后的派生公式是

key0="youknowwhatImean"
iv0="itsallintheflow!"
key[i] = bundle[(11 + 17 * i) % n] ^ ((fnv + i) & 0xff) ^ key0[i]
iv[i] = bundle[(7 + 29 * i) % n] ^ (((crc32_bundle >> 8) + 3 * i) & 0xff) ^
iv0[i]

得到最后真正的key和iv分别是：

key=9ae9908d89879e9981ca199e82cd1783

iv = dcd9c3d2daca55dca4af2aafa63aa3e9

然后就可以进行AES和RC4 Warp的解密，密文是AES padding后的48字节

0x56, 0x96, 0x70, 0xde, 0x6d, 0x7e, 0x27, 0x0e, 0x7e, 0x27, 0xa1, 0x89, 0xce, 0xc7, 0x08, 0x2b,
0xa1, 0x88, 0x3f, 0x69, 0x79, 0x66, 0x31, 0xad, 0xbd, 0x7c, 0x6d, 0x0f, 0xea, 0x9f, 0x28, 0x1d,
0x60, 0xf9, 0xd1, 0x27, 0x7f, 0x1b, 0x00, 0x7c, 0x36, 0xd6, 0x31, 0x72, 0x77, 0x53, 0xed, 0xcf

老附件的逻辑是在后面对于传进去的rc4加密后的密文和bundle继续混合做运算，然后用四个常量约束作为检验，但是好像对于Z3的负担过重，理论上是可以解出的，但是对于那一系列约束也没有更好更快的办法了，故而最后换成了密文的直接校验。

最终exp如下：

from pathlib import Path
from typing import Tuple

from Crypto.Cipher import AES

K_AES_KEY = b"youknowwhatImean"
K_AES_IV = b"itsallintheflow!"
K_CIPHER_TARGET = bytes(
    [
       0x56, 0x96, 0x70, 0xde, 0x6d, 0x7e, 0x27, 0x0e, 0x7e, 0x27, 0xa1, 0x89, 0xce, 0xc7, 0x08, 0x2b,
        0xa1, 0x88, 0x3f, 0x69, 0x79, 0x66, 0x31, 0xad, 0xbd, 0x7c, 0x6d, 0x0f, 0xea, 0x9f, 0x28, 0x1d,
        0x60, 0xf9, 0xd1, 0x27, 0x7f, 0x1b, 0x00, 0x7c, 0x36, 0xd6, 0x31, 0x72, 0x77, 0x53, 0xed, 0xcf
    ]
)

RC4_KEY = b"TobeorNottobe"


def u32(x: int) -> int:
    return x & 0xFFFFFFFF


def rotl8(v: int, s: int) -> int:
    return ((v << s) | (v >> (8 - s))) & 0xFF


def rotr8(v: int, s: int) -> int:
    return ((v >> s) | (v << (8 - s))) & 0xFF


def xorshift32(v: int) -> int:
    v = u32(v)
    v ^= (v << 13) & 0xFFFFFFFF
    v ^= v >> 17
    v ^= (v << 5) & 0xFFFFFFFF
    return u32(v)


def fnv1a32(data: bytes) -> int:
    h = 2166136261
    for b in data:
        h ^= b
        h = u32(h * 16777619)
    return h


def crc32_custom(data: bytes) -> int:
    table = []
    for i in range(256):
        c = i
        for _ in range(8):
            c = (0xEDB88320 ^ (c >> 1)) if (c & 1) else (c >> 1)
        table.append(c & 0xFFFFFFFF)

    crc = 0xFFFFFFFF
    for b in data:
        crc = table[(crc ^ b) & 0xFF] ^ (crc >> 8)
    return u32(~crc)


def derive_runtime_key_iv(bundle: bytes) -> Tuple[bytes, bytes]:
    n = len(bundle)
    salt_k = fnv1a32(bundle) & 0xFF
    salt_i = (crc32_custom(bundle) >> 8) & 0xFF

    rk = bytearray(16)
    riv = bytearray(16)
    for i in range(16):
        kb = bundle[(i * 17 + 11) % n]
        ib = bundle[(i * 29 + 7) % n]
        rk[i] = K_AES_KEY[i] ^ kb ^ ((salt_k + i) & 0xFF)
        riv[i] = K_AES_IV[i] ^ ib ^ ((salt_i + i * 3) & 0xFF)
    return bytes(rk), bytes(riv)


def pkcs7_unpad(data: bytes, block_size: int = 16) -> bytes:
    pad = data[-1]
    return data[:-pad]


def rc4warp_process(key: bytes, data: bytes) -> bytes:
    s = list(range(256))
    j = 0
    salt = 0xC3

    for i in range(256):
        k0 = key[(i * 5 + 1) % len(key)]
        k1 = key[(i * 3 + 7) % len(key)]
        salt = rotl8(salt, 1)
        j = (j + s[i] + k0 + ((k1 ^ salt) & 0xFF) + i) & 0xFF
        s[i], s[j] = s[j], s[i]

    i = 0
    j = 0
    twist = 0x9D
    out = bytearray(len(data))

    for n, b in enumerate(data):
        i = (i + 1) & 0xFF
        j = (j + s[i] + ((i * 11) & 0xFF)) & 0xFF
        s[i], s[j] = s[j], s[i]

        idx = (s[i] + s[j] + ((s[(i + j) & 0xFF] ^ twist) & 0xFF)) & 0xFF
        k = s[idx]
        twist = rotl8(twist, 3)
        spice = s[(k ^ twist) & 0xFF]
        out[n] = (b ^ k ^ spice ^ ((i * 13) & 0xFF)) & 0xFF

    return bytes(out)


def recover_flag(bundle_path: Path) -> str:
    bundle = bundle_path.read_bytes()
    rk, riv = derive_runtime_key_iv(bundle)

    stage1_padded = AES.new(rk, AES.MODE_CBC, riv).decrypt(K_CIPHER_TARGET)
    stage1 = pkcs7_unpad(stage1_padded)
    flag_bytes = rc4warp_process(RC4_KEY, stage1)
    return flag_bytes.decode("utf-8")


def main() -> None:
    bundle_path = Path("cache.snap.bundle")
    flag = recover_flag(bundle_path)
    print(flag)


if __name__ == "__main__":
    main()

flag：SUCTF{w311_d0n3_y0u_kn0w_h3rm35_n0w}

作为对抗AI agent的一次出题尝试，并没有取得想要的效果，有点失败。

SU_West

这是一个auto re题目，设计成了81层，整体逻辑不算很复杂，每层都是单层可逆的。

进入主函数首先看到简单的反调试和主验证逻辑：

nt __fastcall main(int argc, const char **argv, const char **envp)
{
  unsigned __int8 v6; // [rsp+37h] [rbp-2B1h] BYREF
  unsigned __int64 v7; // [rsp+38h] [rbp-2B0h] BYREF
  _QWORD v8[85]; // [rsp+40h] [rbp-2A8h] BYREF

  if ( (unsigned __int8)sub_140001100(0, 0, 0, 1595750129, 0x510E527FADE682D1LL, 1) )
  {
    puts("debugger detected");
  }
  else
  {
    memset(v8, 0, 0x288u);
    if ( (unsigned __int8)sub_1400012C0((unsigned int)argc, argv, v8) )
    {
      puts("all inputs collected, starting verification...");
      v7 = 0;
      v6 = 0;
      if ( sub_1400013B0((__int64)v8, &v7, &v6) )
      {
        puts("correct");
        return 0;
      }
      sub_140013140("incorrect at round %zu (layer %u)\n", v7 + 1, v6 + 1);
    }
    else
    {
      puts("input format error");
    }
  }
  return 1;
}

sub_1400013B0循环 81 轮，每轮使用order[round]作为层ID并调度函数指针表，实现了以NOR为中心的虚拟机。

sub_140012480是Festiel的 ARX 混频器，等效形式为：

lo, hi = low32(seed), high32(seed)
for i in range(rounds):
    k = table_key(i) ^ rolling_sum ^ round_mix
    t = rol32((k_lo ^ lo), rot_a)
    lo_new = (hi ^ (t + (lo ^ k_hi))) ^ (k_lo + ror32(lo, rot_b))
    hi, lo = lo, lo_new

sub_140012630是64位ARX组合器

大概逻辑是：

v9 = v16 + ROL64(k ^ acc ^ v9, rot)

sub_140012F10是SplitMix64 风格的生成器,等效逻辑是：

state -= 0x61C8864680B583EB
z = (state ^ (state >> 30)) * 0xBF58476D1CE4E5B9
z = (z ^ (z >> 27)) * 0x94D049BB133111EB
out = z ^ (z >> 31)

sub_140012F60其实就是NOR VM的主要逻辑

return ~(a2 | a1);

然后动态执行NOR VM，每层实现常量的改变：

每一个layer的整体模板如下：

v5  = sub_140012480(x, s0, r, table_L, L);
v8  = sub_140012630(v5, s0, r, table_L, L);
v9  = sub_140012780(v8, v5, s0, r, table_L);
v10 = sub_140012940(v8, r, table_L);
if (v10 != TARGET[L]) return 0;

v18 = sub_140012B90(v8, v9, s0, r, table_L);
sub_140012C00(flag_buf, v18, r);
s0 = sub_140012CA0(v8, v9, s0, v5, r, table_L, L);

return !sub_140001100(...);

每层的本质抽象出来其实是一个很复杂的z3约束表达式，最后都能变成

f(input)== target

这样的形式，所以可以直接抄出来函数模板，提取参数求解即可

然后验证顺序和输入顺序的对应是：

[1, 76, 32, 47, 53, 72, 28, 58, 2, 26, 41, 68, 43, 11, 65, 17, 67, 50, 4, 46, 5, 3, 73, 44, 19, 77, 49, 22, 78, 61, 66, 64, 71, 48, 40, 80, 24, 60, 51, 6, 62, 8, 79, 63, 52, 30, 45, 75, 16, 25, 15, 33, 81, 56, 57, 69, 36, 74, 38, 54, 70, 7, 37, 29, 14, 39, 18, 27, 34, 9, 23, 55, 12, 10, 35, 31, 20, 42, 13, 59, 21]

然后可以自行使用ida python提取数据得到每层的模板常量，最后z3求解

最后exp如下：

#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""
Embedded-data solver generated from nor_data.json.
"""

from pathlib import Path

from z3 import (
    BitVec,
    BitVecVal,
    Concat,
    Extract,
    RotateLeft,
    RotateRight,
    Solver,
    UGE,
    ULE,
    sat,
)

MASK64 = (1 << 64) - 1
MASK32 = (1 << 32) - 1
MIN_INPUT = 10**15
MAX_INPUT = 10**16 - 1

TARGETS = [6040087155136277484, 9201116228787473754, 7068932625840448529, 9476222914721073742, 4550939852980439947, 7734561545438768643, 7964698121417019100, 10509118525619401086, 17615085397720373336, 14611903247921449779, 2066196783878451842, 15607432893771337849, 12473128424334533832, 10436403565184595342, 8876599175175189165, 6793016066092516416, 14479696017691775528, 2593443532932739211, 11255952701596308893, 8471887947084729269, 9876612649506518045, 16345867032764440756, 6715637112867701104, 597061433647103176, 17445718982131792120, 10562135586074669028, 1745472262260777316, 10683720445547295292, 2830463888371475582, 13234341561532310772, 1894073144278499488, 6953454056964678212, 16729707659877353186, 2297340739241129463, 10964921407242951940, 11392184854014901610, 3253043749380286428, 1153079155751826343, 4554980065482054616, 550286893004902160, 6568496224468840284, 4611133985206358274, 15425901754125075079, 2831108722465973894, 16768371922173895810, 11893276319691879391, 3656808813463636218, 16300655179691407460, 15015642930763445757, 881580021203168745, 15776649945110701686, 13624096800217442891, 11565628122504704716, 6776197135622248955, 5656393725326876182, 16477772474784513495, 18101248358484275654, 5961302722566256568, 14891136393745771744, 12289539200023291951, 13466185976065733189, 5657131116485898253, 8861200533157845042, 5311348217105755617, 764636234253878848, 8027874530608372071, 10090691210395521926, 14118940675977983829, 1385393016008008677, 3236431817507649544, 17384799683318401971, 7758714120444656511, 17017672162990226334, 11247888034296168731, 8162242962937050896, 17349960648628492336, 16173042233776091426, 3570188166719577318, 594636820152070292, 425071086454441469, 15630137654329865421]
ORDER = [0, 75, 31, 46, 52, 71, 27, 57, 1, 25, 40, 67, 42, 10, 64, 16, 66, 49, 3, 45, 4, 2, 72, 43, 18, 76, 48, 21, 77, 60, 65, 63, 70, 47, 39, 79, 23, 59, 50, 5, 61, 7, 78, 62, 51, 29, 44, 74, 15, 24, 14, 32, 80, 55, 56, 68, 35, 73, 37, 53, 69, 6, 36, 28, 13, 38, 17, 26, 33, 8, 22, 54, 11, 9, 34, 30, 19, 41, 12, 58, 20]
S0_INIT = 0x669e1e61279d826e
S2_INIT = 0xa03ab9f27c4c6bfb
FLAG_SEED_HEX = ""
DEFAULT_FLAG_SEED_HEX = "8f129c59d5e29d23988f2bd108f36af0634a3710306f3397c6d2c07b722582ffcf5b9109c7141c78"

RAW_HEX_LIST = []

BLOB_HEX_LIST = []

EMBEDDED_TABLES = [
    {"raw_hex": raw_hex, "blob_hex": blob_hex}
    for raw_hex, blob_hex in zip(RAW_HEX_LIST, BLOB_HEX_LIST)
]

def u64(x: int) -> int:
    return x & MASK64


def u32(x: int) -> int:
    return x & MASK32


def rol64_i(x: int, n: int) -> int:
    n &= 63
    x &= MASK64
    return ((x << n) | (x >> (64 - n))) & MASK64 if n else x


def rol32_i(x: int, n: int) -> int:
    n &= 31
    x &= MASK32
    return ((x << n) | (x >> (32 - n))) & MASK32 if n else x


def ror32_i(x: int, n: int) -> int:
    n &= 31
    x &= MASK32
    return ((x >> n) | (x << (32 - n))) & MASK32 if n else x


def ror8_i(x: int, n: int) -> int:
    n &= 7
    x &= 0xFF
    return ((x >> n) | ((x << (8 - n)) & 0xFF)) & 0xFF if n else x


def rol64_bv(x, n: int):
    return RotateLeft(x, n & 63)


def rol32_bv(x, n: int):
    return RotateLeft(x, n & 31)


def ror32_bv(x, n: int):
    return RotateRight(x, n & 31)


class TableObj:
    def __init__(self, raw: bytes, blob: bytes):
        if len(raw) < 0xC0:
            raise ValueError("table raw length < 0xC0")
        self.raw = raw
        self.blob = blob

    def b(self, off: int) -> int:
        return self.raw[off]

    def q(self, off: int) -> int:
        return int.from_bytes(self.raw[off:off+8], "little")

    def blob_d(self, off: int) -> int:
        if off + 4 > len(self.blob):
            return 0
        return int.from_bytes(self.blob[off:off+4], "little")

    def blob_q(self, off: int) -> int:
        if off + 8 > len(self.blob):
            return 0
        return int.from_bytes(self.blob[off:off+8], "little")


def sub_12f60_i(a1: int, a2: int) -> int:
    return u32(~(a2 | a1))


def sub_12e30_i(a1: int, a2: int, a3: int, a4: int, a5: int, a6: int) -> int:
    v10 = u32(a3 + a1)
    v11 = rol32_i(a1 ^ a2, a4)
    v12 = sub_12f60_i(v11, v10)
    if a5 & 1:
        res = u32(v12 + (a2 ^ ror32_i(a1, ((a4 + a6 + 7) % 0x1F) + 1)))
    else:
        res = u32(v12 ^ rol32_i(a1 ^ a3, ((a4 + a6 + 11) % 0x1F) + 1))
    if a5 & 2:
        res = u32(sub_12f60_i(a1, a2 ^ a3) ^ res)
    return res


def splitmix64_next(state: int):
    state = u64(state - 0x61C8864680B583EB)
    z = u64((state ^ (state >> 30)) * 0xBF58476D1CE4E5B9)
    z = u64((z ^ (z >> 27)) * 0x94D049BB133111EB)
    return state, u64(z ^ (z >> 31))


def sub_12d50_i(tbl: TableObj, seed_in: int):
    n = tbl.q(184)
    if n > 0x1E4:
        return 0, []
    cnt = n // 5
    seed = u64(seed_in)
    out = []
    for i in range(cnt):
        base = 40 * i
        seed, r = splitmix64_next(seed)
        b0 = (tbl.blob_d(base + 0) ^ r) & 0xFF
        seed, r = splitmix64_next(seed)
        b1 = (tbl.blob_d(base + 8) ^ r) & 7
        seed, r = splitmix64_next(seed)
        b2 = (tbl.blob_d(base + 16) ^ r) & 7
        seed, r = splitmix64_next(seed)
        b3 = (tbl.blob_d(base + 24) ^ r) & 7
        seed, r = splitmix64_next(seed)
        qv = u64(tbl.blob_q(base + 32) ^ r)
        out.append((b0, b1, b2, b3, qv))
    return cnt, out


def sub_12480_i(x: int, s0: int, rnd: int, tbl: TableObj, layer: int) -> int:
    v5 = u64(tbl.q(40) ^ x)
    v6 = 0xA24BAED4963EE407
    v8 = tbl.b(162)
    v20 = v8 + rnd + 7
    v9 = v8 + rnd + 6
    v10 = v8 + rnd
    v19 = rnd + v8 + 1
    v23 = u64(tbl.q(0) ^ u64(0xD6E8FEB86659FD93 * layer) ^ s0 ^ u64(0x9E3779B97F4A7C15 - 0x61C8864680B583EB * rnd))
    rounds = tbl.b(161) + 6

    lo = v5 & MASK32
    hi = (v5 >> 32) & MASK32
    for i in range(rounds):
        old_hi = hi
        old_lo = lo
        v14 = 31 * (v10 // 31)
        v15 = v20 - 31 * ((v9 - v14) // 31) - v14
        v16 = u64(tbl.q(8 + 8 * (i & 3)) ^ v6 ^ v23)
        r1 = (i + v19 - v14) & 0xFF
        r2 = (i + v15) & 0xFF
        x1 = rol32_i((u32(v16) ^ old_lo), r1)
        v17 = u32(old_hi ^ u32(x1 + u32(old_lo ^ u32(v16 >> 32))))
        lo = u32(v17 ^ u32(u32(v16) + ror32_i(old_lo, r2)))
        hi = old_lo
        v6 = u64(v6 - 0x5DB4512B69C11BF9)
        v9 += 1
        v10 += 1
    return u64((hi << 32) | lo)


def sub_12630_i(a1: int, s0: int, rnd: int, tbl: TableObj, layer: int) -> int:
    v18 = tbl.b(163) + rnd + layer + 1
    v19 = tbl.b(163)
    v6 = rnd + v19
    v7 = u64(0x6B2FB644ECCEEE15 * rnd)
    v8 = 0xBF58476D1CE4E5B9
    v9 = u64(s0 ^ tbl.q(40) ^ u64(0xA24BAED4963EE407 * layer) ^ a1 ^ u64(0x9E3779B97F4A7C15 - 0x61C8864680B583EB * rnd))
    rounds = tbl.b(160) + 2
    v11 = layer + v6
    v12 = u64(0x94D049BB133111EB - v7)
    v13 = 0
    v14 = v12
    for _ in range(rounds):
        v16 = u64(s0 ^ v8 ^ tbl.q(88 + 8 * (v13 & 3)))
        rot = (v18 + v13 - 63 * ((v11 // 63) & 0xFF)) & 0xFF
        v9 = u64(v16 + rol64_i(tbl.q(120 + 8 * ((v13 + v19) & 3)) ^ v14 ^ v9, rot))
        v11 += 1
        v14 = u64(v14 + v12)
        v8 = u64(v8 - 0x40A7B892E31B1A47)
        v13 = (v13 + 1) & 0xFF
    return v9


def sub_12780_i(a1: int, a2: int, s0: int, rnd: int, tbl: TableObj) -> int:
    v9 = tbl.b(163)
    s = rnd + v9
    v10 = ((0x1A7B9611A7B9611B * s) >> 64) & MASK64
    v11 = tbl.q(80) ^ u64(0x2545F4914F6CDD1D * rnd + 0x2545F4914F6CDD1D)
    rot = ((rnd & 0xFF) + (v9 & 0xFF) - 29 * (((v10 + ((s - v10) >> 1)) >> 4) & 0xFF) + 1) & 0xFF
    seed = rol64_i(a2, rot) ^ s0 ^ v11

    cnt, blocks = sub_12d50_i(tbl, seed)
    if cnt == 0:
        return 0

    acc = 0x9E3779B97F4A7C15
    hi = (a1 >> 32) & MASK32
    lo = a1 & MASK32
    v28 = u64(s0 ^ tbl.q(48) ^ a2)
    v20 = rnd & 0xFF

    for i, (b0, b1, b2, b3, qv) in enumerate(blocks):
        v23 = tbl.q(120 + 8 * ((b3 + i + b2 + b1) & 3)) ^ acc ^ qv
        old_lo = lo
        idx = tbl.b(164 + (b0 & 7))
        rot2 = (((idx ^ b1 ^ v9 ^ b0) ^ (i ^ v20 ^ (2 * b2) ^ (4 * b3))) & 0x1F) + 1
        f = sub_12e30_i(
            lo,
            u32(v28 ^ v23),
            u32((v28 ^ v23) >> 32),
            rot2,
            idx,
            i,
        )
        lo = u32(hi ^ f)
        hi = old_lo
        acc = u64(acc - 0x61C8864680B583EB)
    return u64((hi << 32) | lo)


def sub_12940_i(a1: int, rnd: int, tbl: TableObj) -> int:
    v4 = tbl.b(163)
    v29 = tbl.q(64)
    v28 = tbl.q(56)
    v5 = u64(0xA24BAED4963EE407 - 0x5DB4512B69C11BF9 * rnd)
    v6 = tbl.b(162)
    v26 = tbl.q(72)
    v25 = tbl.q(0)
    v24 = tbl.q(40)
    rounds = ((v4 + rnd) & 1) + 3
    v23 = v6 + 1
    v7 = v6 + rnd + 1
    v22 = v4 + 1
    v8 = rnd + v6
    v31 = v4
    v10 = v4
    v27 = v5
    i = 0

    for _ in range(rounds):
        v32 = v5
        v33 = v10
        v34 = v8
        v19 = v7
        v18 = v6
        v12 = -63 * (v6 // 63)
        v13 = u64(tbl.q(8 * ((((i & 0xFF) + v31) & 3) + 11)) ^ tbl.q(8 * (i + 1)) ^ v28 ^ v5 ^ v29)
        v14 = v7 - 63 * (v8 // 63)
        prev_i = i
        i += 1
        v15 = rol64_i(v26, (prev_i + v22 - 63 * ((v10 & 0xFF) // 63)) & 0xFF)
        v16 = u64((v25 + v13) ^ rol64_i(v24, (prev_i + v23 + v12) & 0xFF))
        a1 = u64(v16 + rol64_i(v15 ^ a1 ^ v13, v14))
        v6 = v18 + 1
        v7 = v19 + 3
        v8 = v34 + 3
        v5 = u64(v27 + v32)
        v10 = v33 + 1

    return u64(a1 ^ tbl.q(80) ^ u64(0x94D049BB133111EB - 0x6B2FB644ECCEEE15 * rnd))


def sub_12b90_i(a1: int, a2: int, s0: int, rnd: int, tbl: TableObj) -> int:
    v = u64(tbl.q(72) ^ a2 ^ a1 ^ u64(0xD6E8FEB86659FD93 * rnd - 0x2917014799A6026D))
    return u64(v ^ rol64_i(s0, ((rnd + tbl.b(163)) % 0x1F) + 1))


def sub_12ca0_i(a1: int, a2: int, s0: int, a4: int, rnd: int, tbl: TableObj, layer: int) -> int:
    return u64(
        u64(0x9E3779B97F4A7C15 * layer)
        ^ s0
        ^ u64(0x2545F4914F6CDD1D * a4 + 0x2545F4914F6CDD1D)
        ^ rol64_i(tbl.q(56) + a2 + a1, ((rnd + tbl.b(163)) % 0x2F) + 1)
    )


def sub_12c00_i(flag: bytearray, k: int, rnd: int):
    v3 = rnd & MASK32
    v6 = 8 * rnd
    v7 = 7 * rnd
    v9 = rnd
    for n in range(40):
        part = u64((k >> (v6 & 0x38)) ^ v7 ^ (k >> ((v6 & 0x38) ^ 0x38)))
        t1 = (part + v3 + n) & 0xFF
        x = (flag[n] ^ t1) & 0xFF
        x = (x - ((part ^ v9) & 0xFF)) & 0xFF
        rot = (((part & 0xFF) ^ ((v3 ^ n) & 0xFF)) & 7)
        flag[n] = ror8_i(x, rot)
        v9 += 5
        v7 += 13
        v6 += 8


def sub_12480_sym(x, s0: int, rnd: int, tbl: TableObj, layer: int):
    v5 = BitVecVal(tbl.q(40), 64) ^ x
    v6 = 0xA24BAED4963EE407
    v8 = tbl.b(162)
    v20 = v8 + rnd + 7
    v9 = v8 + rnd + 6
    v10 = v8 + rnd
    v19 = rnd + v8 + 1
    v23 = BitVecVal(u64(tbl.q(0) ^ u64(0xD6E8FEB86659FD93 * layer) ^ s0 ^ u64(0x9E3779B97F4A7C15 - 0x61C8864680B583EB * rnd)), 64)
    rounds = tbl.b(161) + 6

    lo = Extract(31, 0, v5)
    hi = Extract(63, 32, v5)
    for i in range(rounds):
        old_hi = hi
        old_lo = lo
        v14 = 31 * (v10 // 31)
        v15 = v20 - 31 * ((v9 - v14) // 31) - v14
        v16 = BitVecVal(u64(tbl.q(8 + 8 * (i & 3)) ^ v6), 64) ^ v23
        v16_lo = Extract(31, 0, v16)
        v16_hi = Extract(63, 32, v16)
        x1 = rol32_bv(old_lo ^ v16_lo, (i + v19 - v14) & 0xFF)
        v17 = old_hi ^ (x1 + (old_lo ^ v16_hi))
        lo = v17 ^ (v16_lo + ror32_bv(old_lo, (i + v15) & 0xFF))
        hi = old_lo
        v6 = u64(v6 - 0x5DB4512B69C11BF9)
        v9 += 1
        v10 += 1
    return Concat(hi, lo)


def sub_12630_sym(a1, s0: int, rnd: int, tbl: TableObj, layer: int):
    v18 = tbl.b(163) + rnd + layer + 1
    v19 = tbl.b(163)
    v6 = rnd + v19
    v7 = u64(0x6B2FB644ECCEEE15 * rnd)
    v8 = 0xBF58476D1CE4E5B9
    v9 = BitVecVal(u64(s0 ^ tbl.q(40) ^ u64(0xA24BAED4963EE407 * layer) ^ u64(0x9E3779B97F4A7C15 - 0x61C8864680B583EB * rnd)), 64) ^ a1
    rounds = tbl.b(160) + 2
    v11 = layer + v6
    v12 = u64(0x94D049BB133111EB - v7)
    v13 = 0
    v14 = v12
    for _ in range(rounds):
        v16 = BitVecVal(u64(s0 ^ v8 ^ tbl.q(88 + 8 * (v13 & 3))), 64)
        rot = (v18 + v13 - 63 * ((v11 // 63) & 0xFF)) & 0xFF
        v9 = v16 + rol64_bv(BitVecVal(tbl.q(120 + 8 * ((v13 + v19) & 3)) ^ v14, 64) ^ v9, rot)
        v11 += 1
        v14 = u64(v14 + v12)
        v8 = u64(v8 - 0x40A7B892E31B1A47)
        v13 = (v13 + 1) & 0xFF
    return v9


def sub_12940_sym(a1, rnd: int, tbl: TableObj):
    v4 = tbl.b(163)
    v29 = tbl.q(64)
    v28 = tbl.q(56)
    v5 = u64(0xA24BAED4963EE407 - 0x5DB4512B69C11BF9 * rnd)
    v6 = tbl.b(162)
    v26 = tbl.q(72)
    v25 = tbl.q(0)
    v24 = tbl.q(40)
    rounds = ((v4 + rnd) & 1) + 3
    v23 = v6 + 1
    v7 = v6 + rnd + 1
    v22 = v4 + 1
    v8 = rnd + v6
    v31 = v4
    v10 = v4
    v27 = v5
    i = 0
    for _ in range(rounds):
        v32 = v5
        v33 = v10
        v34 = v8
        v19 = v7
        v18 = v6
        v12 = -63 * (v6 // 63)
        v13 = u64(tbl.q(8 * ((((i & 0xFF) + v31) & 3) + 11)) ^ tbl.q(8 * (i + 1)) ^ v28 ^ v5 ^ v29)
        v14 = v7 - 63 * (v8 // 63)
        prev_i = i
        i += 1
        v15 = rol64_bv(BitVecVal(v26, 64), (prev_i + v22 - 63 * ((v10 & 0xFF) // 63)) & 0xFF)
        v16 = BitVecVal(u64((v25 + v13) ^ rol64_i(v24, (prev_i + v23 + v12) & 0xFF)), 64)
        a1 = v16 + rol64_bv(v15 ^ a1 ^ BitVecVal(v13, 64), v14)
        v6 = v18 + 1
        v7 = v19 + 3
        v8 = v34 + 3
        v5 = u64(v27 + v32)
        v10 = v33 + 1
    return a1 ^ BitVecVal(u64(tbl.q(80) ^ u64(0x94D049BB133111EB - 0x6B2FB644ECCEEE15 * rnd)), 64)


def build_tables():
    return [TableObj(bytes.fromhex(t["raw_hex"]), bytes.fromhex(t.get("blob_hex", ""))) for t in EMBEDDED_TABLES]


def solve_direct():
    order = ORDER
    targets = TARGETS
    tables = build_tables()

    if len(order) != 81 or len(targets) != 81 or len(tables) != 81:
        raise RuntimeError(f"unexpected sizes: order={len(order)} targets={len(targets)} tables={len(tables)}")

    s0 = S0_INIT
    _s2 = S2_INIT
    del _s2

    seed_hex = FLAG_SEED_HEX or DEFAULT_FLAG_SEED_HEX
    flag = bytearray(bytes.fromhex(seed_hex))
    if len(flag) != 40:
        raise RuntimeError("FLAG_SEED must be 40 bytes after fallback")

    inputs = []

    for rnd in range(81):
        layer = order[rnd]
        tbl = tables[layer]
        target = targets[layer]

        x = BitVec(f"x_{rnd}", 64)
        solver = Solver()
        solver.add(UGE(x, BitVecVal(MIN_INPUT, 64)))
        solver.add(ULE(x, BitVecVal(MAX_INPUT, 64)))

        v5 = sub_12480_sym(x, s0, rnd, tbl, layer)
        v8 = sub_12630_sym(v5, s0, rnd, tbl, layer)
        v10 = sub_12940_sym(v8, rnd, tbl)
        solver.add(v10 == BitVecVal(target, 64))

        if solver.check() != sat:
            raise RuntimeError(f"unsat at round {rnd+1}, layer {layer+1}")

        xv = solver.model().eval(x).as_long()
        inputs.append(xv)

        v5c = sub_12480_i(xv, s0, rnd, tbl, layer)
        v8c = sub_12630_i(v5c, s0, rnd, tbl, layer)
        v9c = sub_12780_i(v8c, v5c, s0, rnd, tbl)
        v18 = sub_12b90_i(v8c, v9c, s0, rnd, tbl)
        sub_12c00_i(flag, v18, rnd)
        s0 = sub_12ca0_i(v8c, v9c, s0, v5c, rnd, tbl, layer)

        print(f"[round {rnd+1:02d}] layer={layer+1:02d} x={xv}", flush=True)

    return inputs, bytes(flag)


def main():
    inputs, flag = solve_direct()

    print("flag:", flag.decode("ascii", errors="replace"))

if __name__ == "__main__":
    main()

flag：SUCTF{y0u_h4v3_0v3rc0m3_81_d1ff1cu1t135}

写在最后

我在apk里塞了三个我很喜欢的剪辑视频，某种程度上也反映了我当下的精神状态和心境，auto re用西游记的主题也是我想去坚持去追寻的精神内核。“念念回首处，即是灵山。”

验证成功的视频是我在《海上钢琴师》里最喜欢的一段台词：

“The world is out there

Nothing but a gangplank to cross

I think land people waste a lot of time wondering why

Why the hell don’t you get off?

Just once? One time?

Winter comes and you can’t wait for summer

Summer comes and you live in dread of winter

That’s way you never tire of traveling

Always chasing someplace far away where it’s always summer

Doesn’t sound like a good bet to me.”

题目在赛中出问题，自己也内疚了挺久的，毕竟给参赛选手带来了并不好的体验。我的CTF生涯也进入倒计时了，在AI横行的当下，作为碳基生物，有一种深深的无力感。

时间不等人，我也该收拾收拾自己的行囊，继续前往下一个人生路口了，可能今后想起我在这片赛场曾经活跃过，曾经感受过成功的喜悦，曾经和一群我认为最可爱的人并肩奋斗过的时候，会笑着细数那些闪闪发光的瞬间。

所以就把这一页当作阶段性的落款吧。山高路远，时代汹涌，前路未明，可我仍愿意相信，所有认真走过的路都算数，所有不肯熄灭的热爱都有回音。纵然有一天我不再活跃于这片赛场，我也会记得，自己曾在这里年轻过、燃烧过、胜过、败过，也无比真诚地热爱过。

“我们 不说再见”