binculator

Platform: spbctf | Category: Reversing | Type: Challenge | Difficulty: Medium | OS: Linux | Author: XESXOR | Date: 2026-07-02 | Status: Solved Techniques: bfs_pathfinding, capstone_immediate_extraction, dfa_reconstruction, plt_got_hooking, python_bump_allocator_malloc_stub, unicorn_partial_function_emulation

Summary

Task: server streams 10 base64-encoded 32-bit x86 ELF DFA validators, each needing an accepting input string within 120s. Solution: built a generic solver that emulates only init_states() with Unicorn (PLT/malloc hooked), extracts the per-binary accept marker via capstone, reconstructs the DFA graph in emulated memory, and BFS-finds the shortest accepting string.

binculator — spbctf

Description

Сервер присылает вам 10 бинарей по очереди. В ответ необходимо послать строчку, которая заставит текущий бинарь написать 'You win!'. Таймаут 120 секунд на каждый бинарь. После 10-го правильного ответа сервер пришлет флаг.

English: The server ("Welcome to THE BINARY CALCULATOR - binculator") sends 10 base64-encoded 32-bit x86 Linux ELF binaries one at a time. For each one you must send a string that makes the current binary print You win!. There is a 120-second timeout per binary. After the 10th correct answer the server sends the flag. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Each binary is a deterministic finite automaton (DFA) validating an input string. Because you get a fresh, different binary every round with only 120s each, and the DFA graph is built dynamically at runtime (the init_states function is ~1088 disassembly lines and differs per binary), manual reversing per round is infeasible — this challenge demands a generic automated solver.

Analysis

The binaries are ELF 32-bit LSB, Intel 80386, dynamically linked, not stripped (GCC Ubuntu 7.5.0). Reversing main, get_next_state, create_trans and init_states reveals a classic table-driven DFA. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

main (0x08049227)

1. fgets a line from stdin, strlen it.
2. Call init_states() — this builds the whole DFA graph on the heap.
3. Read the start-state pointer from the global init_state (0x804b030).
4. Loop over each character: state = get_next_state(state, ch).
5. After consuming the string: cmp eax, 0xcade7 against the final state's marker (state[0]). If equal → print You win!.

State struct (8 bytes, malloc'd)

[0]  int   marker        ; 0xcade7 = ACCEPT, 0xbbb27 = default non-accept, 0xffffffff (-1) = error
[+4] ptr   trans_array   ; 0 => no transitions (self-loop on any char)

‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Transition struct (8 bytes)

[0]  int   char          ; sign-extended (movsx in create_trans); -1 terminates the array
[+4] ptr   target_state

get_next_state(state, char) (0x080491d2)

• If state->trans_array == 0 → return the same state (self-loop for any char).
• Else linearly scan; return the matching target, or the global error_state (0x804b034, marker = -1) if no match.

create_trans(trans_ptr, char, target) (0x08048536)

Writes trans[0] = movsx(char), trans[1] = target. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

init_states (0x08048561) — the per-binary-unique part

Mallocs an array of 25 state pointers (0x64 bytes), mallocs each 8-byte state, sets all markers to 0xbbb27, then wires transitions with create_trans and marks the single accept state. This function is what differs per round; everything else is identical.

Key insight: rather than reimplement the ever-changing init_states, run it with a CPU emulator and read the resulting graph straight out of emulated memory.

Solution

The solver harness runs on darwin/arm64 (no qemu-i386), so it uses the Unicorn engine to emulate only init_states(): ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

1. Load all PT_LOAD segments into a Unicorn UC_ARCH_X86 / UC_MODE_32 instance.
2. Set up a stack and a heap region; hook the PLT stubs (parse .plt: each 16-byte entry is ff 25 <got_addr>, mapped to a name via .rel.plt + .dynsym). Implement malloc in Python as a bump allocator and stub out the rest, returning by popping the saved return address.
3. Emulate init_states() from EIP=init_states, stopping at a sentinel return address (0xdeadbeef). This builds the real DFA graph in emulated memory.
4. Read the start-state pointer from the init_state global.
5. Extract the accept marker dynamically by disassembling main with capstone and finding cmp eax, IMM (IMM > 0x1000) — the accept constant can differ per binary, so hard-coding 0xcade7 is unsafe.
6. BFS over the reconstructed graph from the start state to any state whose marker == accept marker, recording (prev_state, char) to rebuild the shortest accepting string.
7. Verify by replaying the string through the DFA logic in Python and confirming the final marker == accept marker. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

PLT / malloc hooking (the core harness detail)

 python read-only • copy allowed Copy
# Map GOT offset -> imported name from .rel.plt + .dynsym
got_to_name = {}
for r in elf.get_section_by_name('.rel.plt').iter_relocations():
    got_to_name[r['r_offset']] = dynsym.get_symbol(r['r_info_sym']).name

# Each 16-byte .plt entry is: ff 25 <got_addr>  ->  map name -> plt stub addr
plt_stubs = {}
off = 0
while off < len(plt_data):
    if plt_data[off:off+2] == b'\xff\x25':
        got = struct.unpack('<I', plt_data[off+2:off+6])[0]
        if got in got_to_name:
            plt_stubs[got_to_name[got]] = plt_addr + off
    off += 16
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

plt_by_addr = {v: k for k, v in plt_stubs.items()}
heap_ptr = [0x9000000]

def hook_code(uc, address, size, user_data):
    if address in plt_by_addr:
        name = plt_by_addr[address]
        esp  = uc.reg_read(UC_X86_REG_ESP)
        ret  = struct.unpack('<I', uc.mem_read(esp, 4))[0]
        args = struct.unpack('<4I', uc.mem_read(esp+4, 16))
        if name == 'malloc':
            sz = args[0]
            p = heap_ptr[0]
            heap_ptr[0] = (heap_ptr[0] + sz + 0xf) & ~0xf   # bump allocator
            uc.reg_write(UC_X86_REG_EAX, p)
        else:
            uc.reg_write(UC_X86_REG_EAX, 0)                 # stub everything else
        uc.reg_write(UC_X86_REG_ESP, esp + 4)              # simulate `ret`
        uc.reg_write(UC_X86_REG_EIP, ret)
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

mu.hook_add(UC_HOOK_CODE, hook_code)

Extracting the accept marker with capstone

 python read-only • copy allowed Copy
md = Cs(CS_ARCH_X86, CS_MODE_32)
for ins in md.disasm(main_code, main_addr):
    if ins.mnemonic == 'cmp' and ins.op_str.startswith('eax,'):
        v = int(ins.op_str.split(',')[1].strip(), 0)
        if v > 0x1000:            # skip small compares (e.g. strlen loop counters)
            accept_marker = v
            break

Running init_states and BFS over the reconstructed graph

 python read-only • copy allowed Copy
# sentinel return so emu_start halts cleanly when init_states returns
mu.mem_map(0xdeadbeef & ~0xfff, 0x1000)
esp = mu.reg_read(UC_X86_REG_ESP) - 4
mu.mem_write(esp, struct.pack('<I', 0xdeadbeef))
mu.reg_write(UC_X86_REG_ESP, esp)
mu.emu_start(init_states, 0xdeadbeef)      # build the DFA graph in emulated memory
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

rd = lambda a: struct.unpack('<I', mu.mem_read(a, 4))[0]
start_state = rd(init_state_glob)

# BFS: state -> (prev_state, char); state[0]=marker, state[4]=trans_ptr (0 = no transitions)
seen = {start_state: None}
q = deque([start_state])
accept_state = None
while q:
    st = q.popleft()
    if rd(st) == accept_marker:
        accept_state = st
        break
    tptr = rd(st + 4)
    if tptr == 0:
        continue
    i = 0
    while True:
        c = struct.unpack('<i', mu.mem_read(tptr + i*8, 4))[0]   # -1 terminator
        if c == -1:
            break
        tgt = rd(tptr + i*8 + 4)
        if tgt not in seen:
            seen[tgt] = (st, c & 0xff)
            q.append(tgt)
        i += 1
‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

# reconstruct shortest accepting string
chars = []
cur = accept_state
while seen[cur] is not None:
    prev, c = seen[cur]
    chars.append(c)
    cur = prev
chars.reverse()
answer = bytes(chars).decode('latin1')

The newline gotcha

Appending a trailing \n to the answer drives the DFA into the error state — the accept state has no self-loop for \n. A verifier that replays chars + [0x0a] will flag this. In practice the server's line protocol strips the newline before feeding stdin to the binary, so sending answer\n over the socket is correct — the binary receives just answer. (Verify against chars only, not chars + [0x0a].) ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Network driver

pwn.py connects and loops 10 times: receive until the answer: prompt, grab the last long base64 blob (re.findall(r'[A-Za-z0-9+/=]{200,}', text)[-1]), base64-decode to an ELF, call solve_bytes(elf), then sendall(answer + "\n"). After 10 rounds it reads the flag.

 python read-only • copy allowed Copy
b64 = re.findall(r'[A-Za-z0-9+/=]{200,}', accum.decode('latin1'))[-1]
elf = base64.b64decode(b64)
ans = solve_bytes(elf)                 # Unicorn emulate + BFS
s.sendall(ans.encode('latin1') + b"\n")

‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍

Result

All 10 rounds solved automatically inside the per-binary timeout. Answers in one run: EmQr, vLsnj, zUxx, YEAmgO, Gxopeo, IjLM, HQSPU, WswcEi, YBdNxD, iWoYpq. Server: YES! then flag: auto{REDACTED}. ‍​‌‌​​‌​​​‌‌​​‌​​​​‌‌​‌​​​​‌‌‌​​‌​​‌‌​​​‌​​‌‌‌​​​​​‌‌​‌‌​​​‌‌​​​​‍