How to read a devirtualization coverage figure

What does a devirtualization coverage figure count?

A devirtualization coverage figure counts units of work, and the unit decides the number. Functions, virtual machine handlers, basic blocks and execution paths are all reasonable units, and each gives a different percentage for the same work. Software testing has the same problem: code coverage measured by statements, by branches or by functions gives three different figures for one test suite.

The denominator matters just as much. A figure can be taken over the functions the protector virtualized, over every function in the binary, or over only the functions the analysis reached. Before you compare two figures, or quote one, find out which unit and which scope each one used.

How can one result read 70%, 77% or 90%?

One result can read 70%, 77% or 90% because each figure divides a different count. Take a synthetic program with 52 functions. A protector virtualized 40 of them, and those 40 are the scope of the analysis. The ledger for that scope reads:

• 28 proven, 6 runtime-dependent, 4 unresolved and 2 permanently bounded, for a total of 40;
• a proof summary with a proven count of 28, a bounded count of 2, 1 counterexample and 3 timeouts;
• readable pseudocode for 36 of the 40 functions, including 8 that are not proven.

Three honest-sounding figures come out of that one ledger:

1. 70% is 28 proven out of 40 in scope. This is the figure the ledger supports.
2. 77% adds the 12 functions the protector never touched and divides by all 52. Those functions were never virtualized, so counting them as recovered says nothing about the protection.
3. 90% counts every function that came back as readable pseudocode. It includes 8 functions that are readable but not proven.

The sentence worth quoting leaves the percentages out: “28 of 40 virtualized functions proven, with the other 12 accounted for below.”

How do the four ledger buckets add up?

The four ledger buckets add up to the total in scope, so every counted function sits in exactly one of them and none can drop out of the result. In the synthetic example, 28 + 6 + 4 + 2 = 40. The table gives each bucket in one line; the article on runtime-dependent, unresolved and bounded functions explains each state in depth.

A figure that leaves out a bucket inflates itself by omission. Drop the 12 functions that did not reach proven from the example, and the same work reads 100%.

Why is readable output not proof?

Readable output is not proof because readable pseudocode shows what a function appears to do, while proof shows that the recovered code cannot disagree with the original under a stated model. Semantic names, typed calls and annotations make code easier to inspect. They are a separate deliverable from the evidence that the code is right.

Devirt checks equivalence with a solver, as how Devirt verifies a recovered function describes: the solver looks for an input on which the two disagree. A counterexample shows a disagreement, and a timeout settles nothing, so neither is counted as proven. In the example, the 1 counterexample and 3 timeouts appear in the proof summary, outside the proven count. Research on binary lifters treats the question the same way: validating lifted code is a check of its own, separate from producing it.

What does Devirt check before it delivers a result?

Devirt checks that a result is complete and consistent before it is delivered. A result that fails any of these checks is not delivered:

• The four ledger buckets add up to the stated total.
• The ledger names the scope it covers.
• A completed result carries the ledger, the proof summary and the output.
• The proven and permanently bounded counts in the proof summary match the same counts in the ledger.
• Every output format you requested is present, and each delivered file sits in the storage reserved for your job, is not empty and is encrypted.
• A novel engagement carries a recorded senior review before release.

Devirt also records the scope and the proof summary counts in the audit log for the job. These are consistency checks on the record. They confirm that the ledger is complete and adds up, and they do not replace the evidence itself, which comes from the analysis. The API guide lists the ledger and proof summary fields a completed job returns.

What does the ledger not tell you?

The ledger does not tell you whether the result answers your question. It tells you how much of the declared scope reached each bucket, and three limits still apply:

• A proof holds within its stated model and assumptions. It does not extend to inputs or environments outside them.
• A runtime-dependent function is only as settled as the input you can supply for it.
• A figure from another tool may count a different unit or scope, so two percentages are comparable only when both are stated.

How do you check a result before relying on it?

You check a result before relying on it by reading its ledger in this order, before the output:

1. Find the unit and the scope: what was counted, and which functions are in it.
2. Check the arithmetic: the four buckets add up to the total.
3. Compare the proof summary with the ledger, and note the counterexamples and timeouts.
4. Find the functions your question depends on, and the bucket each one is in.
5. For each bucket, use the table above to decide: rely, confirm or widen the scope.
6. When you report the result, quote the counts, such as “28 of 40 proven”, not only the percentage.

If the functions you need are unresolved or bounded, a wider engagement may settle them. The synthetic sample assessment shows how an estimated evidence boundary is set out before work starts, and more protector and method research is in devirtualization methods.