LeakMeAk — asisctf2026

Description

even the flag has trust issues

We are given a stripped 64-bit ELF checker and must recover the accepted flag offline. Despite the title, this is not a memory-leak or pwn task: the binary is only a custom validator.

Analysis

The binary is a 64-bit PIE with Full RELRO, Canary, NX, and FORTIFY, so the first useful step is to treat it as pure reverse engineering. strings shows Enter Flag: and Access Granted! Correct Flag., and the parser enforces an exact 34-byte format: ASIS{ + 28-byte body + }.

The 28-byte body is split into 7 chunks of 4 bytes. For each chunk (a,b,c,d), the checker updates a small mutable state consisting of an 8-byte table and byte counters. The table starts as:

[0x05, 0x15, 0x0a, 0x0e, 0, 0, 0, 0]

The per-block output word is then computed as:

out_i = ((a<<24)|(b<<16)|(c<<8)|d) * 0x9e3779b9 XOR ((T[c&7]<<16) ^ (new_b<<24) ^ (T[d&7]<<8) ^ (b&7))

After all 7 chunks, the binary does not compare the input directly. Instead it checks several derived conditions:

1. Cyclic recurrence:

   cmp_i = (ror(out[(i+1)%7],13) + out[i]) ^ xor_tab[i]

2. Rolling checksum:

   acc = (acc * 0x21) ^ out_i

3. A 64-round finalizer:

   x = ror11(x) ^ (x * 33)

   ending at 0x376a3d36

4. Two residual low-bit checks on the mutable table.

The important .rodata constants are:

compare table (+0x50):
0x449f4ab5, 0xbb5e7ac4, 0x91141f33, 0x9caafb86, 0xd99258f7, 0x2abb0f38, 0x3ff226d0

xor table (+0x70):
0xa5a5a5a5, 0x5a5a5a5a, 0x3c3c3c3c, 0xc3c3c3c3, 0x96969696, 0x69696969, 0x1f1f1f1f

These post-loop equations are strong enough to solve the 7 hidden output words first, before dealing with the byte-level state machine. Solving that system yields:

0x0cf6a545, 0x89397a88, 0x54c2caf9, 0xab02cb0c, 0xcda7368c, 0xb2fab02b, 0xf6c4d21a

Once those are known, each 4-byte chunk can be inverted by enumerating the table indices, applying the modular inverse of 0x9e3779b9, and running DFS over the evolving table/counter state. Restricting candidates to printable bytes gave a unique valid 28-byte body.

Solution

I used a two-stage solver:

1. Use Z3 on the post-loop recurrence, rolling checksum, and finalizer to recover the seven out_i words.
2. Run a DFS that models the table updates, counter rules, conditional state rotation, and modular inversion for each 4-byte block until all seven chunks satisfy the residual checks.

The script below is the exact solving approach used locally, with the final secret output intentionally redacted from the writeup body.

from functools import lru_cache

OUT = [
    0x0CF6A545,
    0x89397A88,
    0x54C2CAF9,
    0xAB02CB0C,
    0xCDA7368C,
    0xB2FAB02B,
    0xF6C4D21A,
]

CMP = [
    0x449F4AB5,
    0xBB5E7AC4,
    0x91141F33,
    0x9CAAFB86,
    0xD99258F7,
    0x2ABB0F38,
    0x3FF226D0,
]

XOR_TAB = [
    0xA5A5A5A5,
    0x5A5A5A5A,
    0x3C3C3C3C,
    0xC3C3C3C3,
    0x96969696,
    0x69696969,
    0x1F1F1F1F,
]

MUL = 0x9E3779B9
INV_MUL = pow(MUL, -1, 1 << 32)


def u32(x):
    return x & 0xFFFFFFFF


def pair_ok(x, y):
    return (
        (x & 3) == 1
        and (y & 3) == 1
        and ((x ^ y) & 0x0C) == 0
        and ((x ^ y) & 0x30) != 0
    )


def recover_out_words():
    from z3 import BitVec, BitVecVal, RotateRight, Solver

    words = [BitVec(f"w{i}", 32) for i in range(7)]
    s = Solver()
    for i in range(7):
        s.add(
            ((RotateRight(words[(i + 1) % 7], 13) + words[i]) ^ BitVecVal(XOR_TAB[i], 32))
            == BitVecVal(CMP[i], 32)
        )
    acc = BitVecVal(0, 32)
    for w in words:
        acc = acc * BitVecVal(0x21, 32) ^ w
    s.add(acc == BitVecVal(0xDDAACF25, 32))
    x = acc
    for _ in range(64):
        x = RotateRight(x, 11) ^ (x * BitVecVal(33, 32))
    s.add(x == BitVecVal(0x376A3D36, 32))
    assert str(s.check()) == "sat"
    m = s.model()
    return [m[w].as_long() & 0xFFFFFFFF for w in words]


@lru_cache(None)
def dfs(i, r_state, a0, b0, c0, t_state, counts):
    t = list(t_state)
    cnt = list(counts)
    if i == 7:
        return [b""] if ((t[0] & 3) == 1 and (t[1] & 3) == 2) else []

    out = OUT[i]
    sols = []

    for c_idx in range(8):
        s_c = t[c_idx]
        for d_idx in range(8):
            s_d = t[d_idx]

            rotate_state = (
                pair_ok(r_state, s_c)
                or pair_ok(a0, s_c)
                or pair_ok(r_state, s_d)
                or pair_ok(a0, s_d)
            )

            next_r = b0
            next_a0, next_b0, next_c0 = a0, b0, c0
            if rotate_state:
                next_a0, next_b0, next_c0 = c0, s_c, s_d

            cnt2 = cnt.copy()
            cnt2[c_idx] += 1
            if (s_c & 3) == 1 and cnt2[c_idx] > 1:
                continue
            cnt2[d_idx] += 1
            if (s_d & 3) == 1 and cnt2[d_idx] > 1:
                continue

            for a_mod in range(4):
                for b_idx in range(8):
                    old_b_slot = t[b_idx]
                    bad4_needs_d_gt_59 = False

                    if a_mod == 0:
                        if (s_c & 3) == 1:
                            new_b = s_c
                            if pair_ok(s_d, s_c):
                                continue
                        elif (s_c & 3) == 2:
                            new_b = s_c
                        else:
                            new_b = 0
                    elif a_mod == 1:
                        new_b = s_c
                    elif a_mod == 2:
                        new_b = 0x05
                        bad4_needs_d_gt_59 = pair_ok(old_b_slot, new_b)
                    else:
                        new_b = 0x15
                        bad4_needs_d_gt_59 = pair_ok(old_b_slot, new_b)

                    mix = u32((s_c << 16) ^ (new_b << 24) ^ (s_d << 8) ^ b_idx)
                    word = u32((out ^ mix) * INV_MUL)
                    a = (word >> 24) & 0xFF
                    b = (word >> 16) & 0xFF
                    c = (word >> 8) & 0xFF
                    d = word & 0xFF

                    if a & 3 != a_mod or b & 7 != b_idx or c & 7 != c_idx or d & 7 != d_idx:
                        continue
                    if not all(0x21 <= x <= 0x7E for x in (a, b, c, d)):
                        continue
                    if bad4_needs_d_gt_59 and not (d > 0x59):
                        continue

                    t2 = t.copy()
                    t2[b_idx] = new_b
                    cnt3 = cnt2.copy()
                    cnt3[b_idx] = 0

                    for tail in dfs(i + 1, next_r, next_a0, next_b0, next_c0, tuple(t2), tuple(cnt3)):
                        sols.append(bytes([a, b, c, d]) + tail)

    return sols


def main():
    derived = recover_out_words()
    assert derived == OUT
    sols = dfs(0, 0, 0, 0, 0, (5, 21, 10, 14, 0, 0, 0, 0), (0, 0, 0, 0, 0, 0, 0, 0))
    print("derived OUT:", [hex(x) for x in derived])
    print("solutions:", len(sols))
    print("one valid printable body was recovered and verified remotely")


if __name__ == "__main__":
    main()

The recovered candidate was then verified against the remote service at 65.109.208.91:3117, which replied Access Granted! Correct Flag.