SREV
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:
| Opcode | Meaning |
|---|---|
| 0 | trap / halt |
| 2 | conditional PUSH of a template frame |
| 3 | conditional DUP of a stack frame |
| 4 | SP -= operand (pop N) |
| 5 / 6 / 7 | ADD / SUB / XOR dest_reg op= (imm or reg) |
| 9 | HALT / 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:
- The ALU dispatcher’s register-indirect vs. immediate selection was backwards, reading the wrong register.
- Opcode 4 is a raw
SP -= operand(pop-N), not a budget counter.
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 + "}")