algoatson.github.io ~/posts
segfault@algoatson.github.io
back to index

defeating obfuscation — MBA, opaque predicates, flattening

2026-02-143 min readre obfuscation

Open a protected binary and the disassembly is a wall: arithmetic that does nothing, branches that never branch, and a giant while/switch where the real logic used to be. None of it is unbreakable — each obfuscation is a transform with a known inverse. The work is recognising which one you're looking at and reaching for the right solvent. VM-based obfuscation is the heavyweight; these three are what you meet first.

target./protected
toolchain
an LLVM-based obfuscator (MBA + opaque predicates + CFF)
goal
recover the handful of real operations under the noise

MBA — arithmetic that hides arithmetic#

Mixed boolean-arithmetic rewrites a simple operation as a sprawling mix of + - ^& | ~ that is algebraically identical but unreadable. The canonical seed identity:

x+y=(xy)+2(x&y)

Apply it recursively and a + b becomes a half-screen of nonsense. You don't simplify it by staring — you either pattern-match known identities, or treat the expression as a black box and synthesize the simplest equivalent from its input/output behaviour:

simplify MBA by synthesis (msynth / SiMBA-style)python
1
2
3
4
# observe the obfuscated expression as a function of its inputs, then ask a
# synthesizer for the smallest expression that reproduces every output.
expr = "(x ^ y) + 2*(x & y)"          # lifted from the disassembly
print(simplify_mba(expr))             # -> "x + y"

For linear MBA this is fast and exact; SMT-backed simplifiers (arybo) prove the equivalence outright. Once each blob collapses to its one real op, the function becomes legible again.

opaque predicates — branches that aren't#

An opaque predicate is a test the obfuscator knows the outcome of — e.g. 7*x*x - 1 != y*y is true for all integers — wired into an if so one side is dead code (often bogus, to waste your time). Don't reason about it; ask a solver whether the condition can ever take the other value:

prove a predicate constant with an SMT solverpython
1
2
3
4
5
import z3
x = z3.BitVec("x", 64)
cond = 7*x*x - 1 != x*x            # the branch condition, lifted
s = z3.Solver(); s.add(z3.Not(cond))
print(s.check())                   # unsat -> always true -> the else-branch is dead

unsat on the negation means the predicate is constant: prune the dead branch and the bogus control flow it guarded evaporates.

control-flow flattening — the dispatcher#

Flattening shreds a function into basic blocks hung off a central switch (state) dispatcher; the original order survives only as a runtime state variable. Static reading order tells you nothing. Symbolically execute the dispatcher: start at each block, let the engine compute the next state, and rebuild the edges into the original CFG:

recovering the real edgestxt
1
2
3
4
5
for each real block B:
    run B symbolically from its entry
    solve for the `state` value it writes
    -> that value selects the next block in the dispatcher
    add edge B -> next; repeat until the graph closes

Triton/angr drive this; Hex-Rays plugins (d810-style) do it inline in the decompiler. The output is the de-flattened function — the dispatcher and its state machine gone, the real basic-block order restored.

what was under all of it

Three transforms, three solvents — and the "protected" check was nine lines:

c
1
2
3
4
5
int verify(const char *k) {
    unsigned s = 0;
    for (int i = 0; k[i]; i++) s = s*31 + k[i];   // a plain rolling hash
    return s == 0x1d8f3a91;
}

The mindset that matters: obfuscation raises the cost of understanding, it doesn't change what the code does. MBA is identities, opaque predicates are solver queries, flattening is a state machine you can replay. Match each to its inverse and the wall comes down to the few lines it was always hiding.