Algebraic Nightmare ( Reverse Engineering) - Writeup

Challenge Overview

"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. The analyst who originally investigated it described the routine as: 'Algebra wearing a disguise.'"

The brief tells you almost everything. "Thousands of arithmetic and Boolean operations" and "algebra wearing a disguise" is a textbook description of Mixed Boolean-Arithmetic (MBA) obfuscation — ordinary math (+, *, xor) hidden behind a mountain of equivalent-but-ugly expressions. The real check underneath is small and, crucially, reversible. So there are two ways in:

• The fast way (intended): lift the check into z3 and let the solver find the input.
• The deep way: peel off the obfuscation by hand, recognize the small algorithm underneath, and run it backwards. No solver at all.

This writeup does both, because the second one is what actually teaches you something.

Note on the flag: every instance generates its own unique binary, so the exact flag bytes and the constants you see below will differ from yours. The method is identical. The flag in this writeup is from my instance.

---

Step 0: What is MBA obfuscation? (for first-timers)

Compilers and obfuscators can rewrite a simple operation into a tangle of equivalent ones. A few identities that are always true for any a, b:

a + b   ==  (a ^ b) + 2*(a & b)
a ^ b   ==  (a | b) & ~(a & b)
~(~x)   ==  x
x & 0xFFFFFFFFFFFFFFFF  ==  x
c ^ c   ==  0           (so  x + 0, x | 0, x ^ 0  are all just x)

Read left-to-right they simplify. An obfuscator applies them right-to-left, over and over, until one a + b becomes a 50-line monster. Multiply that across a whole algorithm and you get "thousands of operations" that actually compute something tiny.

The key insight: MBA changes what the code looks like, not what it does. Apply the identities in the simplifying direction and the monster collapses back to a + b.

---

Step 1: Triage the Binary

file challenge.elf

challenge.elf: ELF 64-bit LSB pie executable, x86-64, dynamically linked,
interpreter /lib64/ld-linux-x86-64.so.2, ... stripped

strings challenge.elf | grep -Ei 'specimen|accept|reject|ANMBA'

specimen>
rejected
accepted

So it reads a line, prints accepted or rejected. Standard "find the input that's accepted" crackme.

Now the surprising part — look at how little actual code there is versus how big the file is:

objdump -d -M intel challenge.elf | wc -l       # ~390 lines of disassembly
ls -l challenge.elf                              # ~286 KB file

Tiny code, huge data. When you see that, think virtual machine (VM): a small interpreter loop driving a giant blob of "bytecode." The thousands of operations from the brief aren't CPU instructions — they're entries in a data table the interpreter walks.

---

Step 2: Read main and Find the Interpreter

Open it in Ghidra/IDA (or objdump -d -M intel challenge.elf). main is short. In order, it:

1. Prints specimen>, reads a line with fgets(buf, 0x80), strips the \n with strcspn.
2. mallocs ~0x4462C bytes and fills them by XOR-decrypting a blob from .rodata: plain[i] = rodata[0x2040 + i] ^ key[i & 7], with an 8-byte key at 0x46670. Byte 0 is forced to 'A'.
3. Checks the decrypted blob starts with the magic "ANMBA2" (Algebra? Nightmare? MBA? version 2 — a nice tell).
4. Reads a header: node count, output count, and a required input length (56).
5. Loads your 56-byte input as seven little-endian 64-bit words (x0..x6).
6. Runs a switch-driven loop over fixed-size records — this is the VM.
7. Compares 7 computed "output" words against 7 stored constants. All must match → accepted.

The record format (read straight from the loop) is 20 bytes:

struct node { uint8_t op; uint8_t pad[3]; uint32_t a; uint32_t b; uint64_t imm; };

And the opcode table, recovered from the switch cases:

Every node computes a 64-bit value from earlier nodes. It's a data-flow graph, not a flat program.

The decoy: each loop iteration also computes a hash-looking value using the constant 0x9E3779B185EBCA87 (the golden-ratio constant you'll recognize from xxHash/splitmix). It looks important — but trace where it's used and it only reaches the switch default case, which stores 0. It's a red herring to waste your time. Ignore it.

---

Step 3: Dump the Bytecode (lift.py)

Reproduce the XOR decryption in Python, verify the magic, and parse the node array + output table.

import struct, sys, collections, pickle
d = open(sys.argv[1], 'rb').read()
N   = 0x4462c
key = d[0x46670:0x46678]

b = bytearray(N); b[0] = 0x41                       # byte 0 forced to 'A'
for i in range(1, N):
    b[i] = d[0x2040 + i] ^ key[i & 7]               # XOR-decrypt the blob
assert b[:6] == b'ANMBA2', b[:8]

n_nodes, n_outs, in_len = struct.unpack_from('<III', b, 8)
print('nodes', n_nodes, 'outs', n_outs, 'len', in_len)

nodes = [struct.unpack_from('<BxxxIIQ', b, 0x18 + 20*i) for i in range(n_nodes)]
base  = 0x18 + 20*n_nodes
idx   = struct.unpack_from('<%dI' % n_outs, b, base)                 # output node indices
exp   = struct.unpack_from('<%dQ' % n_outs, b, base + 4*n_outs)      # expected values

print(collections.Counter(n[0] for n in nodes))
pickle.dump((n_nodes, in_len, nodes, idx, exp), open('vm.pkl', 'wb'))

$ python3 lift.py challenge.elf
nodes 14000 outs 7 len 56
Counter({6: 1293, 5: 1245, 7: 1189, 11: 1185, 3: 1182, 13: 1165, 4: 1144,
         12: 1128, 10: 1123, 9: 1096, 8: 1079, 14: 1072, 1: 92, 2: 7})

14,000 nodes for a 56-byte check. That's the "nightmare." Note there are only 7 loads (op 2) — one per input word — and 92 constants. Everything else is arithmetic/Boolean glue: classic MBA.

---

Step 4: Cut the Dead Code

Not all 14,000 nodes matter. Start from the 7 output nodes and walk the dependency graph backwards — anything you don't reach is filler.

import pickle
nn, ln, nodes, idx, exp = pickle.load(open('vm.pkl', 'rb'))
live = set(); stack = list(idx)
while stack:
    i = stack.pop()
    if i in live: continue
    live.add(i); op, a, b, imm = nodes[i]
    if op in (3,4,5,6,7): stack += [a, b]
    elif op not in (1,2): stack.append(a)
print('live nodes:', len(live), 'of', nn)

live nodes: 662 of 14000

95% of the binary is padding. Only 662 nodes actually feed the answer. That alone makes the problem tractable.

---

Step 5: Undo the MBA (simp.py)

Turn each live node into a small expression tree, then repeatedly apply the simplifying identities from Step 0 until nothing changes.

M = (1 << 64) - 1
def rule(e):
    t = e[0]
    if t == '~' and e[1][0] == '~':                 # ~~x -> x
        return e[1][1]
    if t == '-' and e[1] == e[2]:                   # x - x -> 0
        return ('c', 0)
    if t == '^' and e[2] == ('c', 0): return e[1]   # x ^ 0 -> x
    if t == '&' and e[2] == ('c', M): return e[1]   # x & ~0 -> x
    # (a | b) & ~(a & b)  ->  a ^ b
    if t == '&' and e[1][0] == '|' and e[2][0] == '~' and e[2][1][0] == '&' \
       and set(e[1][1:]) == set(e[2][1][1:]):
        return ('^', e[1][1], e[1][2])
    # (a ^ b) + 2*(a & b)  ->  a + b      (here 2*x appears as x << 1)
    if t == '+' and e[1][0] == '^' and e[2][0] == '<<' and e[2][2] == 1 \
       and e[2][1][0] == '&' and set(e[1][1:]) == set(e[2][1][1:]):
        return ('+', e[1][1], e[1][2])
    return e

Emit the result as flat single-assignment (SSA) lines and the 662-node graph collapses to ~230 readable lines. The repeating shape jumps out immediately:

t0 = x0 ^ 0x6d7e120c6c9b32b7
t1 = rol(t0, 8)
t2 = x1 ^ 0xbfeba2e0bfb9a386
t3 = t1 + t2
t4 = t3 * 0x9af133f6d3cc6bfd
t5 = t4 >> 23
t6 = t4 ^ t5                 <- v ^ (v >> 23)
t7 = rol(x6, 14)
t8 = t6 + t7
...
CHECK t152 == 0x9a4d34833f7e192d
CHECK t161 == 0x53a9cb294a0079d9
... (7 checks total)

---

Step 6: Recognize the Algorithm

Every block has the same skeleton. Pull it out as a helper:

F(a, b) = mix( rol(a ^ k1, r) + (b ^ k2) )
mix(v)  = (v * M) ^ ((v * M) >> 23)      # M is an ODD 64-bit constant

And the 7 words are stirred together, each round producing a new 7-word state from the old one:

n0  = F(s0, s1) + rol(s6, 14)
ni  = F(si, si+1) + rol(ni-1, rot)      for i = 1..5   (rot = 17,20,23,26,29)
n6  = F(s6, n0) + rol(n5, 32)

This runs for 3 rounds. Your 56-byte input is the starting state; the final state must equal the 7 target constants. It's a hand-rolled hash/cipher — and the whole thing is a bijection (each step is invertible), which is the crack.

---

Step 7: Run It Backwards (manual_solve.py)

Each primitive has a clean inverse:

Because each round writes the new words in a chain, you peel them off in reverse order: recover s6 from n6 (you already know n0), then s5 from n5, down to s1, and finally s0 from n0.

MASK = (1 << 64) - 1
rol = lambda v, r: ((v << r) | (v >> (64 - r))) & MASK
ror = lambda v, r: ((v >> r) | (v << (64 - r))) & MASK

def F(a, b, k1, r, k2, M):
    v = (rol(a ^ k1, r) + (b ^ k2)) * M & MASK
    return v ^ (v >> 23)

def F_inv_a(y, b, k1, r, k2, M):          # recover a, given F(a,b)=y and b
    v = y ^ (y >> 23) ^ (y >> 46)         # undo the xorshift
    v = v * pow(M, -1, 1 << 64) & MASK    # undo the multiply (M is odd -> invertible)
    return ror((v - (b ^ k2)) & MASK, r) ^ k1

CHAIN_ROT = [14, 17, 20, 23, 26, 29, 32]

def round_inv(n, T):                      # T = the 7 (k1,r,k2,M) tuples for this round
    s = [0] * 7
    s[6] = F_inv_a((n[6] - rol(n[5], 32)) & MASK, n[0], *T[6])
    for i in range(5, 0, -1):
        s[i] = F_inv_a((n[i] - rol(n[i-1], CHAIN_ROT[i])) & MASK, s[i+1], *T[i])
    s[0] = F_inv_a((n[0] - rol(s[6], 14)) & MASK, s[1], *T[0])
    return s

state = TARGET                            # the 7 expected constants
for T in reversed(ROUNDS):                # ROUNDS[*] read off the de-obfuscated program
    state = round_inv(state, T)

flag = b''.join(w.to_bytes(8, 'little') for w in state)
print(flag)

# sanity check: run it forward again, must reproduce TARGET
st = state
for T in ROUNDS: st = round_fwd(st, T)
assert st == TARGET

$ python3 manual_solve.py
b'KPMG_CTF{6izBtRiSj3VD88EsXNxvzUvM_Q7OVkobraBDtxMr1ijp}__'

The forward re-run matches TARGET, so there's zero guesswork — the inversion is provably correct. (The trailing __ is padding to fill the 56-byte block.)

---

Alternative: The 15-Line z3 Solution (intended path)

If you don't need to understand the algorithm, you never have to do Steps 5–7. Just translate every VM node into a z3 bit-vector and ask the solver to make the 7 outputs equal the targets.

import z3, pickle
nn, ln, nodes, idx, exp = pickle.load(open('vm.pkl', 'rb'))
X = [z3.BitVec(f'x{i}', 64) for i in range(7)]
V = [None] * nn
for i, (op, a, b, imm) in enumerate(nodes):
    if   op == 1:  V[i] = z3.BitVecVal(imm, 64)
    elif op == 2:  V[i] = X[imm % 7]
    elif op == 3:  V[i] = V[b] + V[a]
    elif op == 4:  V[i] = V[a] - V[b]
    elif op == 5:  V[i] = V[a] ^ V[b]
    elif op == 6:  V[i] = V[a] & V[b]
    elif op == 7:  V[i] = V[a] | V[b]
    elif op == 8:  V[i] = ~V[a]
    elif op == 9:  V[i] = V[a] << (imm & 63)
    elif op == 10: V[i] = z3.LShR(V[a], imm & 63)
    elif op == 11: V[i] = z3.RotateLeft(V[a],  imm & 63)
    elif op == 12: V[i] = z3.RotateRight(V[a], imm & 63)
    elif op == 13: V[i] = V[a] * z3.BitVecVal(imm, 64)
    elif op == 14: V[i] = -V[a]

s = z3.Solver()
for k in range(7): s.add(V[idx[k]] == exp[k])
for x in X:                                     # force printable ASCII
    for j in range(8):
        c = z3.Extract(8*j+7, 8*j, x); s.add(c >= 0x20, c < 0x7f)

assert s.check() == z3.sat
m = s.model()
print(b''.join(m[x].as_long().to_bytes(8, 'little') for x in X))

$ time python3 solve.py
sat
b'KPMG_CTF{6izBtRiSj3VD88EsXNxvzUvM_Q7OVkobraBDtxMr1ijp}__'
real  0m13s

Adding "find a different solution" returns unsat, confirming the flag is unique.

---

Step 8: Verify Against the Real Binary

Always confirm against the actual program, not just your model:

printf 'KPMG_CTF{6izBtRiSj3VD88EsXNxvzUvM_Q7OVkobraBDtxMr1ijp}__\n' | ./challenge.elf

specimen> accepted

Flag captured. 🎉

---

Summary

Key Takeaways

• Tiny code + giant data = a VM. The "thousands of operations" were a bytecode blob, not real instructions. Spotting this early saves you from stepping 14,000 ops in a debugger.
• MBA only changes appearance. Every ugly expression reduces via known identities. A handful of rewrite rules turned 14,000 nodes into a page of readable math.
• Prune before you analyze. 95% of the graph was padding. A backward reachability walk from the outputs is the single highest-value step.
• Invertible checks don't need a solver. The real algorithm was a bijection — xor, rotate, add, odd-multiply, xorshift all have exact inverses — so you can run the whole thing backwards from the target constants. The solver (z3) is the fast path; the hand inversion is the one that proves you understood it.
• Odd multipliers are reversible mod 2⁶⁴. x * M with odd M is undone by x * pow(M, -1, 2**64). This shows up constantly in hash/PRNG reversing.
• Watch for decoys. The 0x9E3779B185EBCA87 "hash" was computed every iteration but never used — pure time-waste. Trace data flow before trusting that a value matters.

Flag: KPMG_CTF{6izBtRiSj3VD88EsXNxvzUvM_Q7OVkobraBDtxMr1ijp} (per-instance — yours will differ)