SLOP8445: Seeing Through Obfuscated Code

The thing you will keep meeting

An off-the-shelf unflattener — a tool that undoes one particular trick, where code is rearranged until no block any longer says which block runs next — was pointed at a function that had been through it. The tool exited zero, wrote a valid executable, and took the function's control-flow graph from 56 blocks down to 10: the largest simplification anywhere in this corpus. (Both figures under the same Miasm counting convention, which matters more than it sounds and is week 9's problem.)

SUB      = 08080000
BCF      = 6665BBBC
FLA      = F9CD8332
CALLS    = 12345F05
DATA     = 57977293
COMBINED = EEBB6D71
SHOWCASE FAIL: 1 mismatches

Four legitimate switch alternatives from the original C were grouped together and emitted one after another, so all four now run, every time. Nothing about the graph says so. Nothing about the file says so. One test vector says so immediately.

Week 10 takes it apart.

What you will be able to do

By week 12 you should be able to take an unfamiliar obfuscated function, choose an approach and say why, work across more than one representation, validate whatever you conclude at the level you claimed it, and state the boundary of your own result without being asked. Concretely, you will be able to explain:

• why source, IR and machine code can tell different stories about one function;
• how compiler optimisation can weaken, erase or preserve an obfuscation;
• how mixed Boolean-arithmetic is simplified, and what a simplification proves;
• what makes an opaque predicate different from an ordinary path-dependent branch;
• how symbolic execution and an SMT solver prove a branch direction impossible;
• how such a proof becomes six changed bytes in a working executable;
• why control-flow flattening hides successor relationships rather than values;
• why an unflattener succeeds on one implementation and fails on its close relative;
• why valid-looking deobfuscation output still has to be validated semantically;
• and where generic methods succeed, against where a representation-specific assumption is still doing the work.

Analysis success

A tool ran, produced output, and did not error.

Semantic proof

A property holds — under a stated model, state and path prefix.

Binary rewriting

Bytes changed and a file still loads.

Runtime correctness

The program answered correctly, on the inputs that were actually run.

The argument, in four blocks

What it is built on

build conditions from one frozen source that linked, ran and passed their own checks

68 / 68build conditions from one frozen source that linked, ran and passed their own checksshowcase_matrix_v1.md

injected opaque gates proved one-sided across two different obfuscator implementations

38injected opaque gates proved one-sided across two different obfuscator implementationsfamily_results.json

differential test triples on the rewritten binaries, with zero mismatches

9,189differential test triples on the rewritten binaries, with zero mismatchesvalidation.json

of 4,118 inputs miscomputed by a lift whose LLVM IR verifies cleanly

3,917of 4,118 inputs miscomputed by a lift whose LLVM IR verifies cleanlysemantic_result.json

Where to go next