Buddy the ELF

A 9.5 KB stripped, statically linked x86-64 ELF with a hand-rolled layout (4 raw LOAD segments, no libc, one function at 0x401000). That function is a small bytecode interpreter that runs the user input through fixed per-byte transforms and asserts each result against baked-in constants. One opcode XOR-decrypts the rest of the bytecode in place using a keystream derived from the input, so a wrong flag decrypts the tail to garbage.

Solve

1. In Ghidra, open the single function at 0x401000. It is a dispatch loop reading opcodes from .data (0x403180), with the input buffer in .bss (0x4033a8). Recover the opcode table:

0x00            fail / halt
0x01 ii         idx = ii
0x02            acc = inp[idx]
0x03 kk         acc ^= kk
0x04 kk         acc = (acc + kk) & 0xff
0x05 cc         assert acc == cc
0x06 ii         idx = ii; assert inp[ii] in {0,10}   (terminator / length)
0x07            success
0x08            acc ^= bVar9
0x09            bVar9 = sbox[bVar9 ^ inp[idx]]       (keystream update)
0x0a            acc = sbox[acc]
0x0b ll ll      decrypt next ll bytes: prog[i] ^= bVar9   (self-modifying)
0x0c i1 i2 cc   assert inp[i1] ^ inp[i2] == cc
0x0d xx         nop (2-byte)
0x0e ii         t = xtime(acc, 0x4b); acc = sbox[t ^ acc ^ inp[ii]]   (GF(2^8) mix)

A per-byte block (for example 01 18 / 02 / 0a / 08 / 03 a7 / 04 3a / 05 8a / 09) pins one input byte through an invertible pipeline. The 05 assert fixes acc before the 09 folds the byte into the keystream, so bVar9 is determined as you go. Control flow is input-independent; the only data dependence is the decrypt key at 0x0b.

2. Re-implement the VM with each input byte as a z3 BitVec(8) and the sbox as a z3 Array. When 0x0b is hit, the constraints so far force bVar9, so read its concrete value from the model, decrypt those bytes for real, and continue. The .data program lives at file offset 0x2180 (vaddr 0x403180, length 0x226) and the sbox at file offset 0x2078 (vaddr 0x402078, 256 bytes). The full solver (solve.py):

#!/usr/bin/env python3
import z3

data = open("buddy", "rb").read()
PROG = bytearray(data[0x2180:0x2180 + 0x226])
SBOX = list(data[0x2078:0x2078 + 256])

N = 0x80
inp = [z3.BitVec(f"b{i}", 8) for i in range(N)]
sbox = z3.Array("sbox", z3.BitVecSort(8), z3.BitVecSort(8))
s = z3.Solver()
for i, v in enumerate(SBOX):
    s.add(sbox[i] == v)

_cnt = [0]
def SB(e):
    t = z3.BitVec(f"sb{_cnt[0]}", 8); _cnt[0] += 1
    s.add(t == sbox[e]); return t

acc = z3.BitVecVal(0, 8)
idx = 0
bv9 = z3.BitVecVal(0, 8)

pc = 0
used = set()
while True:
    op = PROG[pc]
    if op == 0x00:
        raise SystemExit("hit fail/halt op")
    elif op == 0x01:
        idx = PROG[pc + 1]; pc += 2
    elif op == 0x02:
        acc = inp[idx]; used.add(idx); pc += 1
    elif op == 0x03:
        acc = acc ^ PROG[pc + 1]; pc += 2
    elif op == 0x04:
        acc = acc + PROG[pc + 1]; pc += 2
    elif op == 0x05:
        s.add(acc == PROG[pc + 1]); pc += 2
    elif op == 0x06:
        idx = PROG[pc + 1]
        s.add(z3.Or(inp[idx] == 0, inp[idx] == 10)); pc += 2
    elif op == 0x07:
        break
    elif op == 0x08:
        acc = acc ^ bv9; pc += 1
    elif op == 0x09:
        bv9 = SB(bv9 ^ inp[idx]); used.add(idx); pc += 1
    elif op == 0x0a:
        acc = SB(acc); pc += 1
    elif op == 0x0b:
        ln = PROG[pc + 1] | (PROG[pc + 2] << 8)
        assert s.check() == z3.sat
        kv = s.model().eval(bv9, model_completion=True).as_long()
        pc += 3
        for i in range(ln):
            PROG[pc + i] ^= kv
    elif op == 0x0c:
        i1, i2, cc = PROG[pc + 1], PROG[pc + 2], PROG[pc + 3]
        s.add(inp[i1] ^ inp[i2] == cc); used.add(i1); used.add(i2); pc += 4
    elif op == 0x0d:
        pc += 2
    elif op == 0x0e:
        ii = PROG[pc + 1]
        hi = z3.LShR(acc, 7) == 1
        t = (acc << 1) ^ z3.If(hi, z3.BitVecVal(0x4b, 8), z3.BitVecVal(0, 8))
        acc = SB(t ^ acc ^ inp[ii]); used.add(ii); pc += 2
    else:
        raise SystemExit(f"unknown op {op:#x} at pc {pc}")

assert s.check() == z3.sat
m = s.model()
flag = bytearray()
for i in range(max(used) + 1):
    b = m.eval(inp[i], model_completion=True).as_long()
    if b in (0, 10):
        break
    flag.append(b)
print("recovered:", flag.decode())

There are two nested decrypts (284 bytes with bVar9=0xc2 at pc 263, then 223 bytes with bVar9=0xce at pc 324) before opcode 7 appears at pc 549. The solver prints the flag.

3. Confirm by running the binary itself: printf 'SVIUSCG{by3_buddy_h0p3_yu0_f1nd_y0ur_d4d}' | ./buddy prints yes. A concrete re-emulation with the recovered string also reaches the success opcode at pc 549, with the unused buffer bytes resolving to 0x00 as the 0x06 terminator checks require.

Flag: SVIUSCG{by3_buddy_h0p3_yu0_f1nd_y0ur_d4d}