Week 07 · Block III Proof

Symbolic execution and SMT

One branch, two queries, and a solver that answers one of them with a witness and the other with nothing at all. Plus the assumption that turns zero proofs into three.

Block III · ProofStudio 21 April 2027Shape: Solver walkthrough

What exactly has a solver established when it returns UNSAT for one direction of a branch?

Last week ended with a hand argument and a hole in it: the product of two consecutive integers is even, over the integers, and the machine works modulo 2³². This week we stop arguing and write the obligation down.

Symbolic execution, in one paragraph

Instead of running the function on a value, run it on a variable. Every instruction updates an expression rather than a number: and eax, 1 turns the expression in eax into bvand(previous, 1). When you reach a conditional branch you have an expression for its condition, in terms of whatever you left symbolic. Then you can ask a solver about it.

What you left symbolic is the whole ballgame. Here, the two globals the predicate reads are symbolic — nothing else about the program’s state is. That choice is the analysis’s model, and every result below is a result about that model.

One frozen gate

The condition, translated from the actual instructions, with the framework’s own comments left in:

condition.smt2 — the branch condition, as bit-vectors

read it bottom-up

; Extended part - SUB operation
(define-fun ref!54 () (_ BitVec 32) (bvsub g_14008901c_4 (_ bv1 32)))
; Extended part - IMUL operation
(define-fun ref!63 () (_ BitVec 32) (bvmul g_14008901c_4 ref!54))
; Extended part - AND operation
(define-fun ref!68 () (_ BitVec 32) (bvand ref!63 (_ bv1 32)))
; CMP operation
(define-fun ref!76 () (_ BitVec 32) ref!68)
; Zero flag
(define-fun ref!82 () (_ BitVec 1) (ite (= ref!76 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))
; CMP operation
(define-fun ref!86 () (_ BitVec 32) (bvsub g_140089018_4 (_ bv10 32)))
; Overflow flag
(define-fun ref!89 () (_ BitVec 1) ((_ extract 31 31) (bvand (bvxor g_140089018_4 (_ bv10 32)) (bvxor g_140089018_4 ref!86))))
; Sign flag
(define-fun ref!91 () (_ BitVec 1) ((_ extract 31 31) ref!86))
; TEST operation
(define-fun ref!103 () (_ BitVec 8) (bvand (bvor (ite (= ref!82 (_ bv1 1)) (_ bv1 8) (_ bv0 8)) (ite (= (bvxor ref!91 ref!89) (_ bv1 1)) (_ bv1 8) (_ bv0 8))) (_ bv1 8)))
; Zero flag
(define-fun ref!108 () (_ BitVec 1) (ite (= ref!103 (_ bv0 8)) (_ bv1 1) (_ bv0 1)))
(assert (= ref!108 (_ bv0 1)))
(check-sat)

lines 4–25 of 25open condition.smt2(1 kB)

ref!54 is g − 1. ref!63 is the product. ref!68 masks the low bit. ref!82 is the zero flag from comparing that against zero — the sete. ref!86 and ref!91 are the second global’s comparison against ten and its sign flag. ref!103 is the or and the test, and ref!108 is the zero flag the jne actually reads.

Every one of those is a 32-bit or 1-bit value. Nothing here is an integer.

Two queries

Write P for the path prefix and C for “the branch is taken”. Then there are exactly two things to ask, and they are separate questions:

P ∧ C

SAT

The solver returns a model: both globals zero.

"model": { "g_140089018_4": 0, "g_14008901c_4": 0 }

That is a witness inside the model. It is not automatically a reachable whole-program input, because nothing here checked that those globals can hold those values at this point in a real execution.

Reading: The taken direction is reachable within the model, and here is a state that reaches it.

P ∧ ¬C

UNSAT

No model, because there is none. This is the result the rest of the block is built on, and it is the one most often quoted more strongly than it deserves.

Reading: No assignment to the symbolic globals makes the branch fall through — so under P and this model, that edge cannot be taken.

result.json — the recorded statuses

both queries, plus the unrestricted re-run

  "queries": {
    "true": {
      "status": "SAT",
      "solver_reported_ms": 3,
      "wall_ms": 15.608299989253283,
      "model": {
        "g_140089018_4": 0,
        "g_14008901c_4": 0
      }
    },
    "false": {
      "status": "UNSAT",
      "solver_reported_ms": 3,
      "wall_ms": 13.061899997410364,
      "model": {}
    }
  },
  "unrestricted_queries": {
    "true": {
      "status": "SAT",

lines 10–29 of 82open result.json(2 kB)

The prefix here is trivial — (= (_ bv1 1) (_ bv1 1)), which is to say “no constraints”, because the gate is reached unconditionally. The file records it anyway. On a gate deeper in the function it would not be trivial, and a result whose prefix was not written down would not be interpretable at all.

Doing it 41 times, generically

The same harness, with no per-implementation pattern, on four -O0 lanes:

OLLVM-16 O0 injected gates proved one-sided: 22 / 22OLLVM-16 O0 injected gates proved one-sidedfamily_results.json
Polaris O0 injected gates proved one-sided: 16 / 16Polaris O0 injected gates proved one-sidedfamily_results.json
genuine source branches across the lanes, every one of them two-sided: 16genuine source branches across the lanes, every one of them two-sidedaggregate_accuracy.json
false positives — no genuine branch was ever classified as opaque: 0false positives — no genuine branch was ever classified as opaqueaggregate_accuracy.json

The false-positive count is the number that makes the rest mean something. A classifier that called everything opaque would score 38 out of 38 on the injected gates and be worthless. The genuine conditions staying two-sided is the control.

The aggregate across all four -O0 lanes is 38 true positives, 1 false negative, 0 false positives, 16 true negatives, and 2 branches never reached within the exploration budget. All three of the shortfalls — the false negative and the two unreached — are in one lane, and that lane is the subject of the next section.

The assumption that changes the answer

One implementation’s opaque conditions are not algebraic. They are built from program state that gets initialised at start-up, and its generated C says so in the clear.

arbitrary symbolic globals — 0 of 3 proved

why it stopped

  "sha256": "EC0422510CB401B0EC004A32961F45F5D9A399EA9EB021F4B16A38B6FE8052BE",
  "state_model": "GENERIC ENTRY-STATE RESULT",
  "configuration": {
    "max_runs": 128,
    "max_instructions": 5000,
    "solver_timeout_ms": 1500,
    "solver": "Z3",
    "symbolic_inputs": "ECX/EDX 32-bit",
    "unknown_writable_globals": "first read symbolized, arbitrary concrete seed 1",
    "symbolic_address_policy": "stop, no unrecorded concretization"
  },
  "exploration_complete": false,
  "elapsed_seconds": 1.3108550000033574,
  "runs": [
    {
      "index": 0,
      "seed": {
        "x": 4919,
        "y": 305419896
      },
      "termination": "STATE INITIALIZATION LIMITATION",
      "failure": {
        "reason": "Symbolic effective address requires array/pointer model; no silent concretization",
        "instruction": "0x1400011cc: mov eax, dword ptr [rcx + rax*4]",
        "addresses": [
          "0x14009b138"
        ]

lines 3–29 of 721open result.json(15 kB)

one captured initialised state — 3 of 3 proved

where the state came from

{
  "provenance": {
    "method": "A: actual PE main initialization path emulated by Triton up to target entry",
    "case": "tigress-add_opaque-O0",
    "executable": "E:\\Workspace\\seeing_through_obfuscation\\results\\showcase_matrix_v1\\optimization_survival\\tigress\\add_opaque\\O0\\showcase.exe",
    "sha256": "EC0422510CB401B0EC004A32961F45F5D9A399EA9EB021F4B16A38B6FE8052BE",
    "main": "0x140001300",
    "stop": "0x140001110",
    "instruction_count": 763,
    "malloc_summary": "successful fresh aligned synthetic heap allocation; no target-specific state constants",
    "allocations": [
      {
        "address": "0x72000000",

lines 1–13 of 55open initialized_state.json(20 kB)

Same harness, same branches, same day. Read the left pane’s failure block: the run did not fail to prove the gates, it stopped — at mov eax, dword ptr [rcx + rax*4], a symbolic effective address, with the policy "stop, no unrecorded concretization". Given an unconstrained pointer it declined to guess. The right pane is the alternative: emulate the real initialisation path for 763 instructions, capture the state, keep the function’s two arguments symbolic, and the same three gates fall out. The difference is not a technique — it is an assumption about the world, made explicit and written to a file.

That stopping policy is worth dwelling on. An analysis that silently concretised the pointer would have produced a number, and the number would have been about one arbitrary heap layout while looking like a general result. The configuration records "symbolic_address_policy": "stop, no unrecorded concretization" because refusing to answer is a defensible result and a quiet guess is not.

Which means the honest statement of the right-hand result is long, and the long version is the only correct one: under the captured initialised state, with the function’s arguments still symbolic, three injected gates are one-sided. Not: these predicates are opaque. Allocation outcomes, heap layout, entropy sources and any later mutation of those globals are all outside the model, and a claim about arbitrary program state is a different claim that this evidence does not support.

Table 04

Opaque flow: what survives optimization?

BCF = bogus control flow. The observation is about the measured native target.

Treatment	At O0	O1 through O3 / Ox	Interpretation
OLLVM BCF	Clones and opaque branches	RESIDUESmall optimized opaque-loop structure	Optimization removes much, not everything.
Hikari BCF	Injected native gates already folded	REMOVEDMeasured target matches clean	IR injection does not imply a native predicate.
Polaris BCF	Strong cloned/opaque topology	REMOVEDMeasured target matches clean	A strong O0 example can be weak at O1+.
Tigress AddOpaque	Initialization-dependent opaque flow	PERSISTS/Ox: 6 conditional jumps vs 1 clean	Runtime state matters to proof and optimization.

Choose the optimization level deliberately: it can erase the phenomenon being taught.

Scope: demo_bogus_control_flow in the retained optimization study. Jump counts alone do not prove opacity.Open the original lecture figure (SVG)

This establishes

For the frozen gate at RVA 0x1667, with two globals symbolic and an empty path prefix, the taken direction is SAT with a recorded model and the fall-through is UNSAT.
Across the OLLVM-16 and Polaris -O0 implementations, a generic harness proved all 38 injected gates one-sided while leaving all 16 genuine source branches two-sided, with zero false positives.
For the state-dependent implementation, the generic yield is 0 of 3 and the yield under one captured initialised state is 3 of 3, with the function arguments symbolic in both.

This does not establish

That any of these branches is globally opaque. Each UNSAT is relative to a path prefix and a memory model, both of which are recorded because both are load-bearing.
That the SAT model is a reachable program input. It is an assignment that satisfies a formula.
That the captured-state result says anything about arbitrary globals, allocation outcomes, or state after later mutation.
That anything has been changed in any binary. Nothing this week touched a byte — that is next week, and it is a different tool.

Methodology and controls: opaque_predicate_triton.mdPer-lane results: family_results.json

Studio: interpret a proof you did not run

Nothing is executed this week. The solver artefacts are frozen and that is the point — you are practising the thing an analyst actually does, which is reading somebody else’s result and deciding what it licenses.

Open prefix.smt2, condition.smt2, true.smt2 and false.smt2. Identify which assertion differs between the last two, and say in one sentence what each file is asking.
Write the two obligations for this gate in your own notation, including the bit widths. Then write the sentence that correctly reports the result — the long version, with the qualifiers.
Now write the overclaimed version, the one that drops the prefix and the model. Keep both. A2 asks you to spot the second kind in somebody else’s prose.
Compare the two Tigress result files. State the assumption the right-hand one adds, and list three things it still does not cover.

result.jsonthe frozen gate: statuses, model, metrics, seed2 kB
prefix.smt2the path prefix, trivial here and recorded anyway66 B
condition.smt2the branch condition as bit-vectors, with the framework's comments1 kB
true.smt2P ∧ C — returns SAT1 kB
false.smt2P ∧ ¬C — returns UNSAT1 kB
result.jsonarbitrary symbolic globals: 0 of 315 kB
result.jsoncaptured initialised state: 3 of 326 kB
add_opaque.cthe generated C, where the state-dependent guards are visible542 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 read a bit-vector SMT-LIB formula well enough to follow `bvand`, `bvsub` and `ite`
you have week 6's hand-argument written down — the one with the hole in it
you can state the difference between a satisfying model and a reachable program input

Symbolic execution and SMT

Symbolic execution, in one paragraph#

One frozen gate#

Two queries#

Doing it 41 times, generically#

The assumption that changes the answer#