C:\CTF\K17\SREV.EXE _□X

SREV

rev

Challenge

A stripped x86-64 ELF that presents as a “Time Limit Exceeded” problem: run it and it times out before printing the flag. The task is to figure out why and fix it.

The VM — SROP Dispatch

Rather than a normal jmp/call dispatch loop, every single VM instruction is executed by loading a 0xf8-byte record from a static program table into a fixed buffer shaped like a Linux sigcontext, patching the buffer’s rip field to the handler address, then executing a real rt_sigreturn syscall — which atomically restores all registers and jumps to the patched rip. Every VM instruction costs one genuine kernel signal round-trip. That’s the TLE: it’s real, not a bug, just absurdly slow.

ISA reverse engineered from the static tables:

OpcodeMeaning
0trap / halt
2conditional PUSH of a template frame
3conditional DUP of a stack frame
4SP -= operand (pop N)
5 / 6 / 7ADD / SUB / XOR dest_reg op= (imm or reg)
9HALT / PRINT

Building a Simulator

I extracted the 291-record program table and auxiliary tables from .rodata and wrote a pure-Python simulator. Two decoding bugs required diffing against a ptrace-captured ground truth of the real binary to find:

Once fixed, the simulator revealed what the loop actually does: it brute-forces printable-ASCII candidates into 12 VM registers, running each through a long fixed ADD/XOR mixing chain. Combinatorially intractable (~9612).

Skipping the Brute Force — Inverting the Mixing Chain

The mixing chain (VM records 2–225) is a straight-line program — no branches, each instruction writes one destination register from an immediate or another register’s current value. It’s directly invertible: walk the instructions in reverse, undoing each op (ADD → subtract, XOR → XOR). Starting from the 12 target constants and inverting all 224 mixing ops recovers the original register seeds directly — no search required.

# Invert the mixing chain to recover flag bytes directly
regs = dict(targets)  # 12 target constants from the SUB-chain immediates
for opcode, dest_nib, src in reversed(ops):
    val = src[1] if src[0] == 'imm' else regs[src[1]]
    cur = regs[dest_nib]
    if opcode == 5:    # was ADD -> undo with SUB
        regs[dest_nib] = (cur - val) & MASK64
    elif opcode == 7:  # was XOR -> self-inverse
        regs[dest_nib] = (cur ^ val) & MASK64

flag_chars = ''.join(chr(regs[n]) for n in range(1, 13))
print("K17{" + flag_chars + "}")