Week 04 · Block II Simplification

MBA and semantic simplification

Mixed Boolean-arithmetic, the tools that reduce it, and the difference between a shorter expression and a proved one. The honest scoreboard is in here.

Block II · SimplificationStudio 17 March 2027Shape: Claim audit

A simplifier returned a shorter expression. What exactly has been proved, and by what?

Last week’s substitution was an identity with a cancelling constant. This week the same source line becomes a nine-term expression mixing multiplication, XOR and complement — and it is still an identity, still with a cancelling structure, just one you have to do some work to see.

One addition, nine terms

Polaris MBA IR — site 0, the whole expression

this computes input + 0x01010101

  %4 = load i32, ptr %2, align 4
  %5 = xor i32 %4, 16843009
  %6 = xor i32 %5, -1
  %7 = mul i32 42, %6
  %8 = add i32 -1128481603, %7
  %9 = mul i32 1, %4
  %10 = add i32 %8, %9
  %11 = add i32 %10, 1145324680
  %12 = add i32 %11, -68
  %13 = xor i32 %4, -1
  %14 = xor i32 %13, 16843009
  %15 = mul i32 -42, %14
  %16 = add i32 %12, %15
  %17 = getelementptr inbounds [8 x i32], ptr %3, i64 0, i64 0
  store volatile i32 %16, ptr %17, align 16

lines 5–19 of 629open target_function.ll(20 kB)

Work it through, because the semester’s central habit starts here — do the arithmetic yourself before believing a tool about it.

%6 is ~(x ^ 0x01010101). %14 is (~x) ^ 0x01010101, which is the same value: complement and XOR commute. So %7 = 42 · %6 and %15 = −42 · %6 cancel exactly. %9 is 1 · x. What is left is a constant fold:

−1128481603  +  1145324680  −  68   =   16843009   =   0x01010101

The expression is x + 0x01010101, spelled in nine operations, and every choice in it — the 42, the split constants, the pointless multiply by one — is noise placed to make the cancellation non-obvious.

Now the machine code the same expression became:

Polaris MBA x64 — site 0 at RVA 0x1030

fourteen instructions for one add

0000000140001030 <demo_substitution>:
140001030: 48 83 ec 28                 	sub	rsp, 0x28
140001034: 89 4c 24 24                 	mov	dword ptr [rsp + 0x24], ecx
140001038: 8b 4c 24 24                 	mov	ecx, dword ptr [rsp + 0x24]
14000103c: 89 c8                       	mov	eax, ecx
14000103e: 35 01 01 01 01              	xor	eax, 0x1010101
140001043: 83 f0 ff                    	xor	eax, -0x1
140001046: 6b c0 2a                    	imul	eax, eax, 0x2a
140001049: 05 bd bc bc bc              	add	eax, 0xbcbcbcbd
14000104e: 89 ca                       	mov	edx, ecx
140001050: c1 e2 00                    	shl	edx, 0x0
140001053: 01 d0                       	add	eax, edx
140001055: 05 88 44 44 44              	add	eax, 0x44444488
14000105a: 83 c0 bc                    	add	eax, -0x44
14000105d: 83 f1 ff                    	xor	ecx, -0x1
140001060: 81 f1 01 01 01 01           	xor	ecx, 0x1010101
140001066: 69 c9 d6 ff ff ff           	imul	ecx, ecx, 0xffffffd6
14000106c: 01 c8                       	add	eax, ecx
14000106e: 89 04 24                    	mov	dword ptr [rsp], eax

lines 6–24 of 684open demo_substitution_disassembly.txt(39 kB)

The backend kept all of it. imul eax, eax, 0x2a is the multiply by 42; shl edx, 0x0 is the multiply by one, lowered to a shift by zero and then not removed. This is the opposite of last week’s result: at -O0 the arithmetic survived instruction selection completely.

What a simplifier is actually claiming

A simplification workflow has three expressions, not two: the input lifted from the machine code, the candidate the tool proposes, and — only in a controlled study like this one — the expected expression from the known source. Two separate equivalence obligations follow, and they answer different questions.

input ≢ candidate

UNSAT

The query that matters in practice, because it is the only one available when you do not have the source.

Reading: No 32-bit input makes the two disagree, so the candidate is a sound replacement for what was in the binary.

candidate ≢ expected

UNSAT

Available only in a study with ground truth. It measures the recovery, not the soundness.

Reading: The candidate is the original operation, not merely something equivalent to the obfuscated code.

Here is one accepted recovery, verbatim from the retained results:

the site, before

lifted input and the known original

    "family": "ollvm16-sub-O0",
    "operation": "xor",
    "site_index": 1,
    "pe_sha256": "1219EFD932F81930556039CC0221AB757D8F9BA28A5036E5551D2C83BD69A65E",
    "previous_classification": "NO SIMPLIFICATION",
    "input": "ExprOp('|', ExprOp('&', ExprId('x', 32), ExprInt(0xEDCBA987, 32)), ExprOp('&', ExprOp('^', ExprId('x', 32), ExprInt(0xFFFFFFFF, 32)), ExprInt(0x12345678, 32)))",
    "expected": "ExprOp('^', ExprId('x', 32), ExprInt(0x12345678, 32))",
    "id": "ollvm16-sub-O0__xor_1",

lines 3–10 of 590open synthesis_expansion.json(36 kB)

the two obligations, and the verdict

both UNSAT — accepted

    "already_canonical_before_msynth": false,
    "settings": "Preregistered: seed 0, 50 synthesis samples, SMIR on, 10s search; AST/SiMBA internal SMT 2s; independent SMT 10s/query.",
    "input_to_candidate": {
      "result": "unsat",
      "bit_width": 32,
      "elapsed_seconds": 0.0007859999968786724,
      "reason_unknown": null,
      "counterexample": null
    },
    "candidate_to_expected": {
      "result": "unsat",
      "bit_width": 32,
      "elapsed_seconds": 0.00029150000045774505,
      "reason_unknown": null,
      "counterexample": null
    },
    "classification": "EXACT RECOVERY",
    "recovered": true,

lines 28–45 of 590open synthesis_expansion.json(36 kB)

A nine-node input reduced to (x ^ 0x12345678) in 0.147 s, with both 32-bit obligations discharged. Note already_canonical_before_msynth: false — the study records it explicitly, because an expression that was already simple before the tool ran must not be counted as a recovery.

And here is the one that matters more, because it is the one people report wrongly:

the same workflow, a different site

candidate → expected is UNSAT; input → candidate timed out

    "already_canonical_before_msynth": false,
    "settings": "Preregistered: seed 0, 50 synthesis samples, SMIR on, 10s search; AST/SiMBA internal SMT 2s; independent SMT 10s/query.",
    "input_to_candidate": {
      "result": "unknown",
      "bit_width": 32,
      "elapsed_seconds": 10.01568430000043,
      "reason_unknown": "timeout",
      "counterexample": null
    },
    "candidate_to_expected": {
      "result": "unsat",
      "bit_width": 32,
      "elapsed_seconds": 0.0008883999980753288,
      "reason_unknown": null,
      "counterexample": null
    },
    "classification": "SMT UNKNOWN",
    "recovered": false,
    "nontrivial_recovery": false,
    "note": "Full 32-bit symbolic-input proof required. Nonzero-score synthesis best candidates are failures, not claimed sound rewrites; their SAT counterexamples are retained. No obfuscator/source-target hint is passed to the algorithm.",
    "upstream_miasm_pretty_expression": "x + 0x1337",
    "display_note": "Faithful AST renderer; upstream Miasm pretty text retained separately because binary subtraction may be printed as unary negation. No algorithm or proof was rerun."

lines 420–441 of 590open synthesis_expansion.json(36 kB)

Read that carefully. The candidate was the right answer — the candidate-to-expected query is UNSAT. The soundness query hit its ten-second budget and returned unknown. So the recovery is not accepted, and it is recorded as SMT UNKNOWN, not as a success with an asterisk.

UNKNOWN is not a weak yes. It is the absence of an answer. A workflow that treats it as a yes is a workflow that will one day accept something false.

The scoreboard

isolated repeated sites recovered with both 32-bit obligations proved: 10 / 12isolated repeated sites recovered with both 32-bit obligations provedsynthesis_expansion.json
candidates left SMT UNKNOWN, both from the MBA specimen: 2candidates left SMT UNKNOWN, both from the MBA specimensmt_overview.json
composed whole-function return expressions completely recovered: 0 / 20composed whole-function return expressions completely recoveredcomplex_arithmetic_deobfuscation.md
largest proved partial reduction, in AST nodes — against a 12-node source formula: 305 → 79largest proved partial reduction, in AST nodes — against a 12-node source formulacomplex_arithmetic_deobfuscation.md

The first two numbers are the good news, and they are about isolated sites: one operation, one variable, a known shape. The second two are what happens when the operations feed each other.

A second frozen probe was built for exactly this — four small branchless uint32 functions of four to ten operations, where intermediates are consumed by later operations. Machine expressions were extracted for 44 of 48 build/function cases; the four that failed hit a preregistered AST size guard on carry-flag expressions and never reached the simplifier, so they are extraction limits and not simplifier failures. Of the twenty obfuscated complete return expressions that were extracted, the fixed algebraic and oracle configurations completely recovered none. They did produce proved partial reductions, the largest being 305 AST nodes down to 79 — a 74% reduction that is still six times the size of the twelve-node source formula.

So: local success, no composition. That is the honest shape of the result, and it is why the course does not describe expression simplification as a solved problem.

Table 06

What does each deobfuscator actually produce?

Expression recovery, a branch proof, LLVM IR and a rewritten PE are different outputs.

Workflow	Input / idea	Delivered result	Boundary to remember
msynth AST/oracle	Extracted expression; rewrite / match	Simpler expression	No rewritten PE in this study.
SiMBA	Algebraic MBA simplification	Simpler expression	Partial reduction is not full recovery.
Synthesizer	Search for a small expression	Candidate expression	Accept only after equivalence proof.
ollvm-unflattener	Discover states; recover successors	Rewritten PE or failure	A produced PE can have wrong semantics.
Triton DSE/SMT	Symbolic branch conditions	Proof / witness	Analysis itself does not patch the PE.
Proof-driven rewriter	Consume proofs and exact bytes	Patched PE	Predicates and dead bytes can remain.
Mergen	Lift x64 instructions	LLVM IR	Valid IR can silently miscompute.
Ordinary LLVM O2	Optimize retained or lifted IR	Optimized IR	Cannot repair an unsound lift.

Ask two questions: what representation was recovered, and how was its correctness checked?

PE = Windows Portable Executable. The Mergen test harness is not a rewritten original PE.Open the original lecture figure (SVG)

What it looks like in a disassembler

A disassembler diff close-up. The left pane shows simple mov, add and xor instructions with small immediates. The right pane is dense with imul, xor, and, or and add instructions carrying large 32-bit constants, with no branches. — The reason a one-block function can be expensive: nothing here is structurally difficult, and the symbolic expression for the whole function is enormous. Correctness of any simplification of it comes from the retained equivalence proofs, not from this picture.
analysis view — not correctness evidencedemo_substitution2_2.jpg — open for full resolution

This establishes

Linear MBA expanded all 24 sites of this specimen with a distinct operator tree at each, taking the native target from 115 to 678 instructions, and survived instruction selection at -O0.
Ten of twelve isolated repeated sites were recovered with both 32-bit equivalence obligations discharged; two returned SMT UNKNOWN and were not accepted.
In the composed-expression probe, no complete recovery occurred among the 20 extracted obfuscated return expressions, while proved partial reductions did — up to 305→79 AST nodes.

This does not establish

That composed MBA is impossible to simplify. The result is about these tools in these fixed configurations and budgets.
That UNKNOWN means equivalent. In one retained case the candidate was in fact correct and the soundness query still timed out.
That any of this produced a rewritten executable. Nothing in this week's workflow emits a binary — expressions and proof records only.
That four Polaris extraction failures are simplifier failures. They hit an AST size guard before the simplifier ran.

Synthesis results from synthesis_expansion.jsonComposition results from complex_arithmetic_deobfuscation.md

Studio: audit one accepted recovery and one UNKNOWN

Take site 0 from the MBA IR above and prove on paper that it equals x + 0x01010101 modulo 2³². State every step where the width matters.
Open synthesis_expansion.json and find the two UNKNOWN records. For each, write the two obligations, the status of each, and one sentence on what is and is not known about that site.
Find a record where already_canonical_before_msynth is relevant and explain why the study bothers to record that field.
In the composed-expression results, find the 305→79 reduction. Then state what you would still have to do before using the 79-node expression in an argument about the program.

A1 is due at the end of next week. Steps 1 and 2 are the shape of its two main sections.

target_function.llthe full MBA IR for all 24 sites20 kB
demo_substitution_disassembly.txt678 instructions of native MBA39 kB
synthesis_expansion.jsonall 12 expansion records, with both SMT obligations each36 kB
smt_overview.jsonevery solver status in the probe, counted922 B
substitution_complex.cthe composed-expression probe source, frozen separately3 kB
complex_arithmetic_deobfuscation.mdthe full composition study, including what failed27 kB

Come to the studio with

The studio assumes you have done these. Each is written so you can tell whether you have, without asking.

you can evaluate `~(x ^ k)` and `(~x) ^ k` and say whether they are the same
you know what SAT, UNSAT and UNKNOWN mean as answers to a question
you can say what `modulo 2³²` changes about an algebraic identity

MBA and semantic simplification

One addition, nine terms#

What a simplifier is actually claiming#

The scoreboard#