Skip to main content

Week 06 · Block II Simplification

Bogus control flow and opaque predicates

Four branches the programmer wrote, twenty-two a tool injected, and the question of how you tell them apart when you do not have the source.

Block II · SimplificationStudio 31 March 2027Shape: Ground truth against graph

Which of these twenty-six conditional branches did the programmer actually write?

Bogus control flow adds branches that never go both ways, guarded by predicates whose value the transformer knows and the analyst is supposed not to. It also clones real code, so that the branch has somewhere plausible to go.

The target for this week and the next two was written to make the distinction checkable. It has exactly four conditions, each with a constant you will recognise on sight.

The four genuine conditions

showcase.c — demo_bogus_control_flow

ground truth: four conditions
uint32_t result = 0x11111111u;

if (x == 0x1337u) {
    result ^= 0x22222222u;
} else {
    result += 0x3333u;
}

if (y > 0x12340000u) {
    result += 0x4444u;
}

if ((x & 0xFFu) == 0x37u) {
    result ^= 0x55555555u;
}

if ((y & 1u) == 0u) {
    result -= 0x6666u;
} else {
    result += 0x7777u;
}
lines 201–221 of 483open showcase.c(12 kB)

the clean build of it

39 instructions, 11 blocks, four Jcc
140001210: 4883ec10                 sub rsp, 0x10
140001214: 8954240c                 mov dword ptr [rsp + 0xc], edx
140001218: 894c2408                 mov dword ptr [rsp + 8], ecx
14000121c: c744240411111111         mov dword ptr [rsp + 4], 0x11111111
140001224: 817c240837130000         cmp dword ptr [rsp + 8], 0x1337
14000122c: 0f8512000000             jne 0x140001244
140001232: 8b442404                 mov eax, dword ptr [rsp + 4]
140001236: 3522222222               xor eax, 0x22222222
14000123b: 89442404                 mov dword ptr [rsp + 4], eax
14000123f: e90d000000               jmp 0x140001251
140001244: 8b442404                 mov eax, dword ptr [rsp + 4]
140001248: 0533330000               add eax, 0x3333
14000124d: 89442404                 mov dword ptr [rsp + 4], eax
140001251: 817c240c00003412         cmp dword ptr [rsp + 0xc], 0x12340000
140001259: 0f860d000000             jbe 0x14000126c
14000125f: 8b442404                 mov eax, dword ptr [rsp + 4]
lines 1–16 of 39open clean_target_disassembly.txt(2 kB)

An equality test against 0x1337, a threshold against 0x12340000, a low-byte test against 0x37, and a parity test. In the clean listing the first one is cmp dword ptr [rsp + 8], 0x1337 followed by jne — a direct transliteration. Eleven blocks, fourteen edges, four conditional branches: that is the whole function.

Every one of those four is path-dependent: whether it is taken depends on the arguments, and both directions are reachable. Keep that word. An opaque predicate is not “a branch whose outcome depends on something obscure” — it is a branch one of whose directions is unreachable, by construction, and the whole of week 7 is about how you would show that.

What the pass adds

the same function, with bogus control flow

the predicate, at the top of the function
140001630: 55                       push rbp
140001631: 4883ec40                 sub rsp, 0x40
140001635: 488d6c2440               lea rbp, [rsp + 0x40]
14000163a: 8955f8                   mov dword ptr [rbp - 8], edx
14000163d: 894dfc                   mov dword ptr [rbp - 4], ecx
140001640: 8b05d6790800             mov eax, dword ptr [rip + 0x879d6]
140001646: 8b0dcc790800             mov ecx, dword ptr [rip + 0x879cc]
14000164c: 89c2                     mov edx, eax
14000164e: 83ea01                   sub edx, 1
140001651: 0fafc2                   imul eax, edx
140001654: 83e001                   and eax, 1
140001657: 83f800                   cmp eax, 0
14000165a: 0f94c0                   sete al
14000165d: 83f90a                   cmp ecx, 0xa
140001660: 0f9cc1                   setl cl
140001663: 08c8                     or al, cl
140001665: a801                     test al, 1
140001667: 0f8505000000             jne 0x140001672
14000166d: e973050000               jmp 0x140001be5
140001672: 8b55fc                   mov edx, dword ptr [rbp - 4]
140001675: 448b4df8                 mov r9d, dword ptr [rbp - 8]
140001679: b810000000               mov eax, 0x10
lines 1–22 of 460open original_target_disassembly.txt(24 kB)

Read it instruction by instruction. Two movs load a pair of writable globals through RIP-relative addressing — 0x14008901C into eax and 0x140089018 into ecx. Then edx = eax − 1, imul eax, edx, and eax, 1, cmp eax, 0, sete al. That is the algebraic half: g · (g − 1) & 1 == 0. The other half is cmp ecx, 0xa / setl cl — a signed comparison of the second global against ten. or al, cl, test al, 1, and the jne at 0x1667 goes to the real code while the fall-through goes to a stub.

So the gate is a disjunction, and its first disjunct is the interesting one: the product of two consecutive integers is even, so the low bit is zero, so the sete always sets al — which makes the whole or always true and the branch always taken.

Over the integers. Over 32-bit values with wraparound you would want to check, and “I can see it is always true” is not a check. Week 7 stops looking at it and proves it instead.

Note also why the globals are there at all. A predicate over initialised constants would fold away during compilation. A predicate over writable globals cannot be folded, because the compiler cannot prove that nothing writes them — which is the same fact the analysis in week 7 has to work around.

The graph

A compact control-flow graph of eleven blocks with fourteen edges, showing four two-way branches that reconverge, and a single return.

The clean target: eleven entry-reachable blocks. You can read the source off this graph.

PE-byte audit: calls do not split blocks, ret is terminalclean_entry_reachable.svg — open for the full graph
A much larger control-flow graph, roughly seventy blocks, with repeated diamond structures and many edges, most leading into duplicated regions.

The same function after the pass: seventy entry-reachable blocks. The repeated diamond shapes are the injected gates, each with a clone of real code on one side.

same audit convention — 70 entry-reachable blocksoriginal_entry_reachable.svg — open for the full graph
A disassembler diff close-up. The left pane shows comparisons against 1337h and 12340000h and a low-byte test. The right pane contains those same comparisons interleaved with RIP-relative global loads, an imul, test instructions and duplicated routes.

Both panes, close up. The genuine comparisons — 1337h, 12340000h, the low-byte test — are still there on the right, among the injected predicate machinery. That is what makes the target usable: ground truth is visible inside the treated binary.

analysis view — not correctness evidencedemo_bogus_control3_flow_clean_to_bcf_2.jpg — open for full resolution
conditional branches in the treated target
26conditional branches in the treated targetfamily_results.json
of them injected opaque gates
22of them injected opaque gatesfamily_results.json
genuine source conditions, all two-sided
4genuine source conditions, all two-sidedfamily_results.json
entry-reachable blocks, clean to treated
11 → 70entry-reachable blocks, clean to treatedselected_metrics.md

Four implementations, four different amounts of nothing

Table 04

Opaque flow: what survives optimization?

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

TreatmentAt O0O1 through O3 / OxInterpretation
OLLVM BCFClones and opaque branchesRESIDUESmall optimized opaque-loop structureOptimization removes much, not everything.
Hikari BCFInjected native gates already foldedREMOVEDMeasured target matches cleanIR injection does not imply a native predicate.
Polaris BCFStrong cloned/opaque topologyREMOVEDMeasured target matches cleanA strong O0 example can be weak at O1+.
Tigress AddOpaqueInitialization-dependent opaque flowPERSISTS/Ox: 6 conditional jumps vs 1 cleanRuntime 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)

One row on that table needs unpacking, because it is the week’s most useful correction.

One implementation’s -O0 IR has the same 44-block / 69-edge topology as the specimen above. Its machine code has 15 blocks and 18 edges. The reason is that most of its injected guards are literal icmp eq i32 1, 1, and the backend folds those without being asked. The four conditional jumps that survive into its machine code are the four genuine source conditions.

So when the week 7 workflow runs on that binary and proves zero injected gates, that is not a failure of the workflow. There were no injected gates left in the machine code to prove anything about. Crediting those four surviving branches as “removed injected predicates” would invert the result completely — and it is exactly the kind of mistake that a workflow reporting only successes would make.

A different mechanism: state, not algebra

One implementation in this corpus builds its opaque conditions from runtime-initialised program state rather than from an algebraic identity — source-level guards over globals set up at start-up.

A small control-flow graph with several conditional branches, before symbolic simplification under a captured initialised state.

Before: the target as recovered, with its guards intact.

symbolic projection, not a patched binarytigress-add_opaque-O0_before.svg — open for the full graph
The same graph after symbolic simplification under a captured initialised state, with fewer branches remaining.

After: the same graph, simplified under one captured initialised state.

symbolic projection, not a patched binarytigress-add_opaque-O0_after.svg — open for the full graph

Both are symbolic projections — a read-only graph, not a rewritten executable. The difference between them is not a technique, it is an assumption: the right-hand graph assumes the state that was captured at run time. Next week that assumption turns zero proofs into three.

Studio: separate the genuine from the injected

Working from the clean and treated disassembly of the same function:

  1. Find all four genuine conditions in the treated listing. Give the address of each. Say what you used to identify them.
  2. Find one injected gate. Write out the predicate it computes, as algebra, from the instructions.
  3. Now argue that your predicate is always false — and then find the hole in your own argument. The hole is the reason week 7 exists.
  4. Read the family results file and find the lane where zero gates were proved. Write one sentence explaining why that is not a failure of the prover, citing the block counts.

Come to the studio with

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

Enlarged evidence

Open the file