Devirtualization: verifying the cumulative artifact without a substituted oracle

First, reconcile the inventory

The August 29 archive assessment recorded 5,792 C pseudocode files. That number included 4,397 substantive functions and 1,395 support entries such as aliases, trivial leaves, wrappers, and compiler runtime material. Another 20 substantive functions had records but no successful Hex-Rays output, bringing the substantive inventory to 4,417.

This explains two counts that initially looked inconsistent:

5,792 pseudocode files = 4,397 substantive + 1,395 support
4,417 substantive functions = 4,397 decompiled + 20 failed

The difference was meaningful classification, not evidence that hundreds of functions had disappeared. The archive's listed hashes also passed verification. That established integrity relative to the manifest; it did not establish semantic completeness.

A functional profile has an explicit edge

The static material supported a substantial profile of the drivers: imports, strings, entry points, dispatch structures, callbacks, and many file, registry, device, and memory-related paths.

The same assessment recorded 325 functions containing 626 unresolved indirect call sites. Together with the failed decompilations, these were real limits on a complete behavior account. A report can describe substantial portions of a driver while still being unable to explain every reachable action.

I used four evidence levels: directly supported code behavior, strong capability evidence, candidate capability, and unknown. This made it possible to retain useful findings without letting an import or a suggestive primitive become a claim of arbitrary access from an ordinary user process.

Native closure is a different result

For this project, admitting a native replacement required evidence from the cumulative PE containing the replacements already accepted. An isolated candidate could pass while the integrated image still depended on the virtualized implementation.

The admission process therefore combined actual-byte execution checks, preservation checks, dependency observations, and PE integrity checks. The important property was agreement between the artifact being counted and the artifact being examined.

These checks remain bounded evidence. Passing sampled executions is not a mathematical proof of equivalence for every possible machine state, and structurally valid PE metadata does not demonstrate successful driver loading.

The result that had to be withdrawn

One candidate passed a specialized audit that substituted a helper during execution. When the cumulative image was checked without that substitution, 16 observed paths returned to the virtualized section through the helper dependency.

The earlier test had answered a narrower question than the ledger required. It showed that the candidate worked with the substituted helper behavior. It did not show that the actual integrated implementation was independent of the original virtualized path.

The candidate was retracted from strict accounting. Keeping it would have made the dashboard look better while weakening the meaning of every other entry.

This was the most valuable failure in the project: a producer-side convenience had become an assumption in the verifier. Removing that convenience exposed the difference.

Make the execution environment part of the equivalence claim

An emulator result is a relation between an artifact, an initial state, and an environment model. It is not a property of the candidate bytes alone.

For clarity, write an execution as Exec(B, s, E), where B is the binary, s the initial machine state, and E the environment supplied by the harness. A differential check compares an observation of the reference execution with an observation of the candidate execution:

Observe(Exec(reference, s, E)) == Observe(Exec(candidate, s, E))

This notation is explanatory, not a formal proof produced by the project. Its value is that it makes the hidden dependency on E explicit. If the harness replaces a helper with a model, the result applies to that modeled environment. It does not automatically transfer to execution of the helper's actual bytes.

An observation also needs a defined scope. Depending on the function contract, relevant outputs can include return values, memory writes, preserved machine state, and termination behavior. A comparison of return registers alone would miss a candidate that returns the right value after corrupting unrelated state. Conversely, requiring equality of every scratch register can reject implementations whose externally relevant behavior agrees.

Matching faults require separate accounting. If both executions terminate with an access fault because the initial state is invalid, the match may be useful evidence about failure behavior. It is not a successful normal execution and should not inflate the normal-path sample count.

Dependency closure is an artifact property

For a simplified model, let N be the set of accepted native entries and V the remaining executable virtualized region. A claim that an entry is independent of the virtualized implementation requires accounting for its reachable dependencies, rather than checking only the entry's first transfer.

Observed execution paths that enter V directly falsify that independence claim for those inputs. The converse is weaker: observing no such path over a finite test set does not prove that none exists. Indirect calls, environment-dependent branches, and incomplete state generation leave a residual coverage problem.

That asymmetry is why a negative dependency observation was sufficient to retract the helper-dependent candidate, while a collection of passing executions was only one part of admission.

The cumulative artifact matters for the same reason. Replacing one function can change helper ownership, layout, or the assumptions of another replacement. A passing result attached to an earlier candidate image cannot simply be copied onto the newest PE. Preservation checks need to refer to the integrated bytes under review.

PE validity and semantic preservation cannot substitute for each other

PE checks cover another independent layer. Section permissions, relocation information, exception metadata, checksums, and signature-directory state affect whether a rewritten image is structurally coherent and what deployment obligations remain. They do not establish that a transformed function preserves behavior.

Behavioral agreement on sampled paths has the opposite limitation: it can occur in a harness that does not exercise the Windows loader or kernel execution environment. A function can pass an emulated comparison while its containing image still has invalid unwind metadata or unsuitable section properties.

The verification record therefore needs separate outcomes for structural checks, sampled semantic checks, dependency observations, and runtime deployment. Collapsing them into one PASS hides exactly the information a later reviewer needs when a result is challenged.

The same discipline applies to a claimed absence of virtualized dependencies. Retaining executable virtualized code does not, on its own, prove that every replacement reaches it. It does establish that removal has not been completed. Reachability and physical removal are different claims and need different evidence.

Report the snapshot without inventing a percentage

The retained September 6 summary records 686 functions in the readiness inventory, 527 strict ledger entries, and an intersection of 526 between those sets. Those are not interchangeable numerators and denominators. I would not present 527 / 686 as an unqualified completion percentage.

The same snapshot still recorded executable .tvm0 material and an incomplete six-driver goal. It represented partial native closure, not six fully devirtualized, runtime-qualified drivers.

The practical improvement was a ledger whose entries could be challenged and withdrawn. Progress became a set of claims attached to artifacts and checks, with a clear account of what remained outside them.

Evidence note: this article uses the retained August 29 static assessment and September 6 strict-progress summary. Their counts belong to different stages and are labeled accordingly. They were not recomputed against the current binaries for publication; no driver was loaded as part of preparing this entry.