Algebraic Nightmare (Reverse Engineering)

Flag: KPMG_CTF{eIToxfbMo0F1YIkbpYHa5tqWhxSp4P4nBeRBWvRjmDtm}

File: Algebraic_Nightmare.elf (the per-instance challenge.elf). ELF 64-bit LSB PIE, x86-64, dynamically linked, stripped. SHA-256 44d57c21ef06c5efcbc2b59daa064e5073870252f111d2cbc9f08b53569662ba. Category: Reverse engineering (bytecode VM with MBA obfuscation)

Brief

An advanced malware sample was recovered from an infected workstation. Static analysis suggests that its validation routine does not use a conventional cryptographic primitive. Instead, the routine appears to consist of thousands of arithmetic and Boolean operations. “Algebra wearing a disguise.”

“Algebra wearing a disguise” describes Mixed Boolean-Arithmetic (MBA) obfuscation: simple operations like + and ^ are rewritten as larger mixes of &, |, ~ and arithmetic. Once you remove the disguise, the check is a short, invertible recurrence. You can run it backwards from the expected outputs to get the flag, without a SAT/SMT solver.

Each instance is personalized, so the constants (and the flag) differ between players. The solver below reads everything from the binary, so it works on any instance.

I analyzed a copy in a scratch directory so the original in ~/Downloads stayed untouched.

Step 1: Triage

$ file chal.elf
chal.elf: ELF 64-bit LSB pie executable, x86-64, ... stripped

$ readelf -S chal.elf | grep -A1 -E '\.text|\.rodata'
  [15] .text     PROGBITS  00000000000010c0  000010c0   00000000000004f9 ...
  [17] .rodata   PROGBITS  0000000000002000  00002000   0000000000044678 ...

$ strings -n 5 chal.elf | grep -E 'specimen|accepted|rejected'
specimen>
rejected
accepted

The binary has only 0x4f9 bytes of code but 0x44678 bytes (about 280 KB) of .rodata, which is mostly high-entropy data. The “thousands of operations” are data interpreted by a small VM, not native code.

Step 2: Disassemble main (the VM)

$ objdump -d -M intel --no-show-raw-insn -j .text chal.elf

main is at 0x10c0. What it does:

  1. Prints specimen> , reads up to 0x80 bytes with fgets into a zeroed 128-byte buffer, and strips the newline with strcspn(buf, "\n").
  2. malloc(0x4462c), then decrypts the program: blob[0] = 0x41 and, for i >= 1, blob[i] = rodata[0x2040+i] ^ key[i & 7], where the 8-byte key is at 0x46670.
  3. Checks the header:
    • blob[0:8] == "ANMBA2\0\0" (movabs rdx,0x3241424d4e41)
    • n_nodes = u32@8, n_out = u32@0xc, length = u32@0x10
    • The input length must equal length, otherwise it prints rejected.
  4. Packs the first 56 bytes of input into 7 little-endian u64 words IN[0..6].
  5. Runs every node (20 bytes each, starting at blob+0x18):

    struct node { u8 op; u8 pad[3]; u32 a; u32 b; u64 c; }   // values v[] stored in a calloc'd array
    
    op result op result
    1 c (const) 8 ~v[a]
    2 IN[c % 7] 9 v[a] << (c&63)
    3 v[a] + v[b] 10 v[a] >> (c&63)
    4 v[a] - v[b] 11 rol(v[a], c&63)
    5 v[a] ^ v[b] 12 ror(v[a], c&63)
    6 v[a] & v[b] 13 v[a] * c
    7 v[a] \| v[b] 14 -v[a]
        other 0
  6. After the nodes come n_out u32 output node indices and then n_out u64 expected values. It ORs together v[out[i]] ^ expected[i] and prints accepted only if the result is zero.

Red herring: for every node, the loop computes a xorshift/golden-ratio “mask” ((c ^ a ^ (b<<17)), ^= <<7, ^= >>9, *= 0x9e3779b185ebca87) and stores it in [rbp-0xf8]. That value never reaches the result (the default branch even reloads it and then zeroes eax). It’s there to make the interpreter look like it does crypto.

Step 3: Decrypt and parse the program

# an_parse.py: shared by the solver (run as: python3 -I an_solve.py chal.elf)
import struct, sys
d = open(sys.argv[1], 'rb').read()          # .rodata vaddr == file offset in this binary
key = d[0x46670:0x46678]
L = 0x4462c
blob = bytearray(L); blob[0] = 0x41
for i in range(1, L): blob[i] = key[i & 7] ^ d[0x2040 + i]
assert blob[:6] == b'ANMBA2'
n, nout, ln = struct.unpack_from('<III', blob, 8)
nodes = [struct.unpack_from('<B3xIIQ', blob, 0x18 + 20*i) for i in range(n)]
o = 0x18 + 20*n
outs = list(struct.unpack_from('<%dI' % nout, blob, o))
exp  = list(struct.unpack_from('<%dQ' % nout, blob, o + 4*nout))
n 14000  nout 7  len 56
outs [486, 518, 550, 582, 614, 646, 678]

Two observations:

  • The program has 14,000 nodes, but the outputs are nodes 486–678, and operands only ever point backwards (no forward references). Walking backwards from the outputs shows that only 662 nodes are live. The other ~13,300 are dead code, added to make the program look bigger.
  • The required length is 56 bytes (7 × 8), so the input is the flag plus padding.

Step 4: Remove the disguise

Printing only the live nodes shows the same few patterns again and again:

n9  = n0 | n7          n18 = n13 ^ n17         n34 = ~n32       n69 = n68 - n68
n10 = n0 & n7          n19 = n13 & n17         n35 = ~n34       n70 = n67 ^ n69
n11 = ~n10             n20 = n19 << 1          ...              n229 = n228 ^ n228
n12 = n9 & n11         n21 = n18 + n20                          n230 = n227 + n229

These are standard MBA identities:

Disguised Real
(x \| c) & ~(x & c) x ^ c
(a ^ b) + ((a & b) << 1) a + b
~~x x
x ^ (c - c), x + (c ^ c), x \| (c ^ c) x
x & 0xffffffffffffffff x

With these removed, the 662 nodes collapse to one step repeated 21 times. Let v[0..6] = IN[0..6]:

v[k+7] = G( rol(v[k] ^ c1, r1) + (v[k+1] ^ c2) ) + rol(v[k+6], r2)
G(t)   = u ^ (u >> 23),  u = t * m        (m odd, all mod 2^64)

Each step has its own c1, c2, r1, r2, m. The checked outputs are v[21..27], the final 7-word window of a nonlinear feedback shift register.

Step 5: Invert the recurrence

Each part of the step can be undone on its own:

  • + rol(v[k+6], r2): subtract it, since v[k+6] is already known when going backwards
  • u ^ (u >> 23): undo the xorshift (iterate x = u ^ (x >> 23) three times)
  • * m with m odd: multiply by m⁻¹ mod 2⁶⁴
  • + (v[k+1] ^ c2): subtract it
  • rol(·, r1) and ^ c1: ror, then XOR

So, knowing v[k+1..k+7], you can solve for v[k] exactly:

v[k] = ror( G⁻¹( v[k+7] - rol(v[k+6], r2) ) - (v[k+1] ^ c2), r1 ) ^ c1

Start from the expected window v[21..27] and step back 21 times to get v[0..6], which is the input.

The solver pulls each step’s parameters from the node graph around every live mul node. It then checks the simplified model against a full reimplementation of the VM on random inputs before inverting:

# an_solve.py  (python3 -I an_solve.py chal.elf)
import os, random
exec(open(os.path.join(os.path.dirname(os.path.abspath(__file__)), 'an_parse.py')).read())
M = (1 << 64) - 1
rol = lambda x, r: ((x << r) | (x >> (64 - r))) & M if r % 64 else x
ror = lambda x, r: rol(x, (64 - r) % 64)

def vm(words):                       # faithful re-implementation of the interpreter
    v = [0] * n
    for i, (op, a, b, c) in enumerate(nodes):
        r = {1: lambda: c, 2: lambda: words[c % 7], 3: lambda: v[b] + v[a],
             4: lambda: v[a] - v[b], 5: lambda: v[a] ^ v[b], 6: lambda: v[a] & v[b],
             7: lambda: v[a] | v[b], 8: lambda: ~v[a], 9: lambda: v[a] << (c & 63),
             10: lambda: v[a] >> (c & 63), 11: lambda: rol(v[a], c & 63),
             12: lambda: ror(v[a], c & 63), 13: lambda: v[a] * c,
             14: lambda: -v[a]}.get(op, lambda: 0)()
        v[i] = r & M
    return v

def xor_operands(andnode):           # (x|c)&~(x&c) -> (x, c)
    orn = nodes[andnode][1]; _, x, cn, _ = nodes[orn]; return x, nodes[cn][3]

steps = []
for i in range(max(outs) + 1):
    op, a, b, c = nodes[i]
    if op != 13: continue                        # one multiply per round
    xr = nodes[nodes[i - 1][1]]                  # (A^B)+((A&B)<<1)
    R, Yand = xr[1], xr[2]
    x, c1 = xor_operands(nodes[R][1]); r1 = nodes[R][3] & 63
    y, c2 = xor_operands(Yand)
    z, r2 = nodes[i + 6][1], nodes[i + 6][3] & 63
    steps.append(dict(x=x, y=y, z=z, c1=c1, c2=c2, r1=r1, r2=r2, m=c, out=i + 10))

# validate the model against the real VM and map nodes -> recurrence indices
w = [random.getrandbits(64) for _ in range(7)]
val = vm(w); seq = list(w)
for s in steps:
    t = (rol(val[s['x']] ^ s['c1'], s['r1']) + (val[s['y']] ^ s['c2'])) & M
    u = (t * s['m']) & M
    out = ((u ^ (u >> 23)) + rol(val[s['z']], s['r2'])) & M
    assert out == val[s['out']]
    seq.append(out)

def unxs(u):                                     # invert u ^= u >> 23
    x = u
    for _ in range(3): x = u ^ (x >> 23)
    return x

v = [None] * (7 + len(steps))
for j, o in enumerate(outs): v[seq.index(val[o])] = exp[j]
for idx in reversed(range(len(steps))):
    s, k = steps[idx], idx + 7
    t = unxs((v[k] - rol(v[k - 1], s['r2'])) & M) * pow(s['m'], -1, 1 << 64) & M
    v[k - 7] = ror((t - (v[k - 6] ^ s['c2'])) & M, s['r1']) ^ s['c1']

print(b''.join(x.to_bytes(8, 'little') for x in v[:7]))
fv = vm(v[:7]); print('vm check:', all(fv[o] == e for o, e in zip(outs, exp)))
$ python3 -I an_solve.py chal.elf
b'KPMG_CTF{eIToxfbMo0F1YIkbpYHa5tqWhxSp4P4nBeRBWvRjmDtm}__'
vm check: True

While solving, I also printed the step-to-index mapping. It confirmed that step k reads (v[k], v[k+1], v[k+6]) for all 21 rounds and that the outputs are exactly v[21..27].

Step 6: Verify against the binary

$ printf 'KPMG_CTF{eIToxfbMo0F1YIkbpYHa5tqWhxSp4P4nBeRBWvRjmDtm}__\n' | ./chal.elf
specimen> accepted

$ printf 'KPMG_CTF{eIToxfbMo0F1YIkbpYHa5tqWhxSp4P4nBeRBWvRjmDtm}\n' | ./chal.elf
specimen> rejected          # fails the 56-byte length check only

The binary needs exactly 56 bytes, so the trailing __ is padding to fill 7 × u64. The flag is the KPMG_CTF{...} part.

Summary

Layer What it was How it was removed
Tiny .text, huge .rodata Bytecode VM Disassemble the interpreter loop at 0x12a0
Encrypted program Repeating 8-byte XOR, magic ANMBA2 Decrypt with the key at 0x46670
xorshift “mask” per node Unused (red herring) Ignore it
14,000 nodes ~13,300 dead Backwards slice from the 7 outputs → 662 live nodes
MBA expressions x^c, a+b, ~~x, x^0 … in disguise Pattern-match the identities
21-round recurrence Invertible NLFSR Run it backwards from the expected window

Takeaways

  • A tiny .text with a big .rodata usually means a VM. Reverse the interpreter, then analyze the bytecode instead of single-stepping it.
  • Slice backwards from what is actually checked. Most of an obfuscated program is often dead.
  • MBA hides simple operations ((x|c)&~(x&c) = x^c, (a^b)+2(a&b) = a+b). Recognize the identities, or confirm a guessed simplification on random inputs as done here.
  • Before reaching for z3 or angr, check whether each step is a bijection. Odd multipliers, xorshifts, rotations and constant XORs are all invertible, so running the steps backwards is exact and instant.
  • Verify a recovered model against a faithful reimplementation of the original before trusting the inversion.