Something always simplifies it for you#

Three things reduce obfuscated arithmetic#

1. The algebra — a simpler equivalent exists, and a solver can prove it
2. The compiler backend — instruction selection recognises an addition
3. You — by reading, which leaves no artefact anyone can check

Only one of these produces evidence.

Nine operations for one addition#

%6  = xor i32 %5, -1          ; ~(x ^ 0x01010101)
%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
%15 = mul i32 -42, %14        ; %14 == %6
%16 = add i32 %12, %15

…is an addition#

%7 and %15 cancel: 42·A − 42·A = 0

−1128481603 + 1145324680 − 68
  =  16843009  =  0x01010101

Everything else is 1 · x.

Same function. Four answers to “did it survive?”#

The deciding variable is where it was applied.

What a simplifier claims#

Three expressions, two obligations:

• input — lifted from the machine code
• candidate — what the tool proposes
• expected — the known original (only in a study)

input ≢ candidate   →  is it sound?
candidate ≢ expected →  did it recover?

The scoreboard, isolated sites#

• 10 / 12 recovered, both 32-bit obligations UNSAT
• 2 returned SMT UNKNOWN

"input_to_candidate": { "result": "unknown",
                        "reason_unknown": "timeout" },
"candidate_to_expected": { "result": "unsat" },
"classification": "SMT UNKNOWN",
"recovered": false

The candidate was right. It is still not accepted.

The scoreboard, composed expressions#

• 44 / 48 whole-function expressions extracted
• 0 / 20 obfuscated return expressions completely recovered
• largest proved reduction: 305 → 79 AST nodes
• the source formula is 12 nodes

Local success does not compose.

Before you credit a simplifier#

Was the expression already canonical before the tool ran?

The retained study records that field per site, on purpose.

Block II#

• Week 4 — MBA, and what a proof of equivalence covers
• Week 5 — optimisation level as a variable, not a nuisance
• Week 6 — a branch the programmer wrote vs one a tool injected

A1 is due at the end of week 5.