Week 08 · Block III Proof

From proof to a working binary

Six bytes, of which four differ. The audit that reconciles seventy blocks with thirty-seven. And 4,591 test triples, which is a great many inputs and not all of them.

Block III · ProofStudio 28 April 2027Shape: Byte-level rewrite

A solver proved an edge impossible. What has to happen next, and who has to do it?

The solver’s job finished last week. Nothing it did changed a file.

What happens now is a different program: a patch consumer that reads the frozen proofs, checks the bytes it is about to touch against what it expects to find, and writes a new executable. It ran no solver queries of its own — the recorded count is zero — and that separation is the reason this week’s result can be stated cleanly.

Six bytes

before0F8505000000jne 0x140001672

afterE90600000090jmp 0x140001672 ; nop

Work out the displacement, because it is the whole trick. 0F 85 is a two-byte opcode for jne rel32, so the instruction is six bytes long and the next instruction begins at 0x166D; a displacement of 0x05 reaches 0x1672. E9 is a one-byte opcode for jmp rel32, so that instruction is five bytes long and the next one begins at 0x166C; to reach the same 0x1672 the displacement has to be 0x06.

Same destination, different number, because the length of the instruction changed. The sixth byte would otherwise be a stray tail, so it is filled with 0x90 — a one-byte nop — which keeps every subsequent byte in the file at the address it was at before.

That is why four bytes differ out of six, and it is also the arithmetic behind the file-level number:

gates patched, from 22 proved and 22 eligible: 22gates patched, from 22 proved and 22 eligiblevalidation.json
bytes changed in the whole file — 22 gates × 4 differing bytes: 88bytes changed in the whole file — 22 gates × 4 differing bytesmetadata_audit.json
bytes in the approved patch window — 22 × 6: 132bytes in the approved patch window — 22 × 6metadata_audit.json
bytes in the file, every other one of them identical: 571,904bytes in the file, every other one of them identicalmetadata_audit.json

What the rewrite did not touch

metadata_audit.json — the layout audit

every claim here is a checked file-level fact

{
  "file_size": 571904,
  "image_size": 598016,
  "bytes_changed": 88,
  "approved_patch_window_bytes": 132,
  "all_other_file_bytes_identical": true,
  "entire_headers_identical": true,
  "sections_identical": true,
  "imports_exports_relocations_exception_debug_directories_and_payloads_identical": true,
  "target_entry_and_unwind_ranges_identical": true,
  "target": {
    "va": 5368714800,
    "rva": 5680,

lines 1–13 of 98open metadata_audit.json(1 kB)

Headers identical. Sections identical. Imports, exports, relocations, exception and debug directories identical. The target’s entry and unwind ranges identical. No byte outside the approved window changed.

That is a layout-preserving rewrite, and it is a design choice with a cost. Nothing was deleted, nothing moved, and every unreachable instruction is still physically present in the file. The alternative — recompacting the function — would produce a smaller binary and would invalidate every address in it.

Read the last two fields of that record with care:

Seventy blocks, thirty-seven reachable, seventy still there

A control-flow graph of about thirty-seven blocks, much smaller than the original, with the repeated diamond structures replaced by straight-through paths. — What is reachable from the entry, after the patches.
entry-reachable projection, 37 blocksrewritten_entry_reachable.svg — open for the full graph

A control-flow graph of the same rewritten function decoding every instruction in its extent, including unreachable blocks, which is visibly larger and contains disconnected fragments. — Every instruction still in the file, reachable or not.
all-static decode of the same bytesrewritten_all_static.svg — open for the full graph

The same binary, two projections. The left graph is what execution can reach; the right graph is what the bytes contain. Both are true, and a report that shows only the left one while calling the file “cleaned” is misleading about the file.

projection_notes.json — what became unreachable, and what it was

a read-only graph projection; no block was deleted

{
  "original_blocks_now_unreachable": 33,
  "classification_counts": {
    "bogus clone": 11,
    "jump stub": 22,
    "predicate computation": 0,
    "genuine semantic block": 0,
    "unknown": 0
  },
  "projection": "rewritten_entry_reachable.dot/svg: read-only graph projection; no binary block deletion",

lines 1–10 of 14open projection_notes.json(1 kB)

Thirty-three blocks became unreachable: eleven bogus clones and twenty-two jump stubs. Note the two zeroes. Zero predicate computation blocks became unreachable — the arithmetic that computes each opaque condition still runs on every call, because the patched jump sits after it. And zero genuine semantic blocks became unreachable, which is the check that the rewrite did not remove program logic.

Table 08

BCF: proof becomes a working PE patch

The same generic proof-and-patch workflow worked across two implementations.

O0 target	Proved / patched gates	Reachable CFG blocks	Retained validation
OLLVM BCF	22 / 22	11 clean70 original 37 rewritten	PASS4,591 triples; 0 mismatches
Polaris BCF	16 / 16	11 clean54 original 30 rewritten	PASS4,598 triples; 0 mismatches

JNE becomes JMP + NOP. Reachable flow shrinks; predicate arithmetic and dead bytes stay in the PE.

A triple compares clean/original/rewrite. Dedicated PE CFG audit: calls do not split blocks; RET is terminal.Open the original lecture figure (SVG)

A disassembler diff close-up. On the left, conditional JNZ instructions guard duplicated regions. On the right, the same positions hold unconditional JMP instructions while the surrounding predicate computations and stub blocks remain present. — The conditional gates have become unconditional transfers. The predicate arithmetic above them and the stub blocks below them are still there. This is a partial rewrite, and calling it anything else would be wrong.
analysis view — not correctness evidencedemo_bogus_control3_flow_bcf_to_rewritten_2.jpg — open for full resolution

And then it was tested

validation.json — the differential test record

4,591 triples, 0 mismatches

{
  "passed": true,
  "eligible": 22,
  "patched": 22,
  "input_sha256": "3ED20E83BE53F28FAF64D1A1CFBC2FEB323B83EC35CCEE0FAF8D85AD7905285F",
  "output_sha256": "15BF8731CD94663F5E0691983F1616969E28675E89B8595371DDBCBA51EA906A",
  "output_path": "E:\\Workspace\\seeing_through_obfuscation\\results\\deobfuscation\\opaque_rewrite\\ollvm16_o0\\showcase_ollvm_bcf_deopaque.exe",
  "canonical_pass": true,

lines 1–8 of 188open validation.json(3 kB)

what the rewritten executable prints

the six canonical answers, unchanged

SUB      = 08080000
BCF      = 6665BBBC
FLA      = DBEFFCE7
CALLS    = 12345F05
DATA     = 57977293
COMBINED = EEBB6D71
SHOWCASE PASS

7 linesopen canonical_rewritten_stdout.txt(141 B)

A triple runs the clean, original and rewritten builds on the same input and compares all three. 4,591 of them, 13,773 native function calls, zero mismatches — including all four genuine conditions exercised both ways and all twelve feasible joint combinations of them.

The same workflow, unmodified, on the second implementation: sixteen gates proved, sixteen patched, sixty-four bytes changed, reachable blocks 54 to 30, 4,598 triples, zero mismatches. That transfer is the strongest generic result in the course, and it is worth being exact about what made it transfer — the proof was about instruction semantics and the patch was about bytes. Neither step recognised an obfuscator.

This establishes

Twenty-two proved gates were rewritten as jmp plus a padding nop, changing 88 bytes inside a 132-byte approved window and leaving every other byte of a 571,904-byte file identical.
Entry-reachable blocks fell from 70 to 37; the 33 that became unreachable were 11 bogus clones and 22 jump stubs, and no genuine semantic block was among them.
The rewritten executables passed their canonical checks and 9,189 clean/original/rewrite differential triples across two implementations with zero mismatches.
The rewriting step ran zero solver queries of its own: proof generation and patch application are separate programs with separate preconditions.

This does not establish

That the binary was cleaned. Every instruction is still in it, and the predicate arithmetic still executes on every call.
That 9,189 passing triples prove equivalence. They are the inputs that were run.
That exception and unwind behaviour is correct through a patched frame. The audit records that this was not tested.
That the original PDB can be trusted on the rewritten function. The identifier survives; the instruction mappings do not.

Patch and validation: opaque_predicate_rewrite.mdReachability convention: projection_notes.json

Studio: justify a patch you did not write

At RVA 0x1667, derive both displacements from first principles and explain why they differ. Then explain why the nop is necessary rather than tidy.
Using the projection notes, reconcile three numbers: 70 physical blocks, 37 reachable blocks, 33 unreachable blocks. Say what each one is counting.
Find the two zeroes in the classification counts and say what each one rules out.
Separate the evidence: which part of this week’s result is a solver proof, which part is a byte-level argument, and which part is a test? For each, name the file.
Then the A2 rehearsal: write a one-paragraph analyst’s summary of this week’s result that is too strong, and underline the words doing the overreaching.

No new patching. The point is the justification, not the edit.

validation.jsoneligible, patched, triples, mismatches, hashes, genuine-branch coverage3 kB
patch_manifest.jsonall 22 patches: address, expected bytes, written bytes396 kB
metadata_audit.jsonthe file-level audit: what changed and what did not1 kB
projection_notes.jsonthe reachability convention and the classification of what died1 kB
rewritten_target_disassembly.txtthe rewritten function, instruction by instruction25 kB
original_target_disassembly.txtthe same function before the patches, for the diff24 kB
validation.jsonthe second implementation: 16 gates, 4,598 triples3 kB
patch_manifest.jsonthe transfer case's 16 patches — different addresses, same method266 kB
rewritten_target_disassembly.txtthe second rewritten function, instruction by instruction16 kB
opaque_predicate_rewrite.mdthe rewriting study, including the preconditions the consumer checks24 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 compute an x86-64 relative branch displacement by hand
you have week 7's two obligations written out for the gate at RVA 0x1667
you can say what an RVA is and how it differs from a virtual address

From proof to a working binary

Six bytes#

What the rewrite did not touch#

Seventy blocks, thirty-seven reachable, seventy still there#