Algebraic Nightmare (Reverse Engineering)
On this page
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:
- Prints
specimen>, reads up to 0x80 bytes withfgetsinto a zeroed 128-byte buffer, and strips the newline withstrcspn(buf, "\n"). malloc(0x4462c), then decrypts the program:blob[0] = 0x41and, fori >= 1,blob[i] = rodata[0x2040+i] ^ key[i & 7], where the 8-byte key is at0x46670.- 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 printsrejected.
- Packs the first 56 bytes of input into 7 little-endian u64 words
IN[0..6]. -
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 arrayop 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] * c7 v[a] \| v[b]14 -v[a]other 0 - After the nodes come
n_outu32 output node indices and thenn_outu64 expected values. It ORs togetherv[out[i]] ^ expected[i]and printsacceptedonly 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, sincev[k+6]is already known when going backwardsu ^ (u >> 23): undo the xorshift (iteratex = u ^ (x >> 23)three times)* mwithmodd: multiply bym⁻¹ mod 2⁶⁴+ (v[k+1] ^ c2): subtract itrol(·, 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
.textwith a big.rodatausually 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.