Not observed is
not unreachable.

THE CASE

One image, one defect, two rules

The firmware is ARDUINO-F103-PWM, a 25,460-byte unit test from the public Fuzzware experiments repository. Its one job is to start a PWM output.

In July the pipeline ran the image in an emulator, recovered a control-flow graph, and trapped every function that was neither observed nor reached. Its static analysis found 396 live blocks out of 2,464. It classed 258 functions as dead and wrote 16,814 bytes of trap instructions over them. It then replayed 3 missions, counted zero trap hits, and recorded the result as safe. It also reported 71.9 percent fewer ROP gadgets.

None of that survived an audit. The log from that run shows all 3 patched executions ending in an invalid instruction at address 0x0, while the originals ran to their budget. The patched firmware crashed in every replay, and the validator, which counted trap hits and nothing else, recorded it as safe. Even a correct validator could not have vouched for main(): the emulator stalls in clock setup and never gets that far.

The 258 functions it called dead include main(), setup(), loop() and analogWrite(). They also include TIM_CCxChannelCmd, the function the upstream project uses to decide whether this unit test passed at all.

THE GENERAL PROBLEM

Why July's check passed

The July validation passed for the wrong reason, and that failure is not special to this prototype.

Brown and colleagues evaluated ten debloating tools for USENIX Security 2024. The tools produced a passing program on 22 percent of medium and high complexity benchmarks, and only 13 percent of attempts were sound and robust under differential testing. A replay that passes is evidence about the missions replayed. The July validation replayed missions that never left start-up code.

The same inference appears wherever reachability is used to close a finding. The VEX justification vulnerable_code_not_in_execute_path is defined as code that is "not reachable through the execution of the code, including non-anticipated states of the product". A trace cannot support a statement about states nobody anticipated. PRUNER does not produce VEX. The definition is quoted here because it sets the standard of evidence that such a claim implies.

Not observed is a measurement. Unreachable is a proof claim.

METHOD

What the review records now

PRUNER takes a raw Cortex-M image, its load address, its entry point and the size of its vector table. Nothing else is required for a review.

It binds the run to the SHA-256 of that exact image, collects evidence that code should be kept, and gives every recovered code block one of four verdicts.

The whole policy is nine rules:

observed(b)                              -> reachable(b)
cfg_reachable(b)                         -> reachable(b)
symbolic_witness(b)                      -> reachable(b)
candidate(b), verified_proof(b)          -> proved_unreachable(b)
candidate(b), no_verified_proof(b)       -> unknown(b)
candidate(b), analysis_incomplete(b)     -> unknown(b)
reachable(b), proved_unreachable(b)      -> conflict(b)
conflict(b)                              -> unknown(b)
proved_unreachable(b), rewrite_ready(b)  -> rewrite_authorized(b)

Evidence can add a reason to keep code. It cannot remove one. Even a verified proof authorizes nothing by itself: the last rule also needs the block to be structurally safe to rewrite, and applying the change needs a separate operator switch.

No language model runs anywhere in this pipeline. An earlier draft of this note described a model proposing changes for the gate to check. That is a design direction, not something the pilot did.

The output is an evidence bundle: an HTML report, the per-block verdicts, and an attestation that binds every artifact by hash. It contains no firmware bytes. A second reviewer checks it offline with one command:

python pruner.py verify evidence_bundle
verified 7765e6ab1f3dd5382265c93c07c1c4562e19272a83c685e964a8c61c3feb3e91 (ANALYSIS_ONLY_REVIEW; signature=unsigned)

The bundle from this run is unsigned. Signing is supported and was not used here.

EVIDENCE

What the evidence was

Every number in this section belongs to one small run, and the budgets of that run belong in the same breath.

The observation was the built-in smoke emulator: a random value on every peripheral read, no interrupts, a cap of 100,000 instructions and 3 seconds. It executed 84 block addresses and stalled in clock setup. A budget 100 times larger executed the same 84, so the limit is the peripheral model and not the budget. No Fuzzware trace was imported. The symbolic step had a 1-second budget and reached 6 blocks.

On that evidence, of 2,469 recovered code blocks, 83 were observed, 1,777 more are reachable by control flow from the vector table, and 609 are unknown.

THE REWRITE GATE

Why the gate stayed shut, and what opened it

PRUNER can also rewrite. It replaces a function with trap instructions if a separately checked proof excludes that function and an operator then approves the exact bytes. On this image the gate stayed shut during the review, and under the rule it used it was always going to.

The proof model is a graph over the 273 functions named in the symbol table of the image's ELF file. Its roots are the vector handlers, the entry point, and every function whose address appears anywhere in the image. Direct calls and branches add edges. A control transfer the model cannot bound gets an edge to every function.

That last rule decides the result. The model lists 46 unbounded sites, and one reachable site is enough to make all 273 functions reachable. A root holds one, so the closure is complete at the first step. The checker's answer, 273 of 273 reachable, says nothing about which functions are dead.

The more useful question is how far the closure reaches without that rule.

Even with every indirect call resolved perfectly, the function graph could exclude one function: _fini, 12 bytes. That is what you would expect from a build that already discards unreferenced functions. What is left is reachable in the graph whether or not this product ever uses it. Removing any of it would need an argument about how the device is configured, not about the call graph.

What opened it

After the review, that rule was replaced with facts checked against the bytes. Each function is decoded from its entry, so data inside it is never read as code. A switch table is bounded only when its guard is found in the two instructions before it. Every byte of a function has to be accounted for, and a function with anything left over keeps the old rule.

On this image that took 6 checked table bounds. All 273 functions were then explained, and the closure excluded exactly the function the ladder predicts: _fini. The unchanged gate planned 12 bytes, a policy registered beforehand applied them to a copy, and replay matched on 3 seeds. It is 12 bytes that nothing calls, which is all a call-graph argument can remove from a build that already discards unused functions.

An image that still carries such functions is different. On NUTTX-F103-GPIO, from the same public set, the same procedure excluded 31 functions and rewrote 2,562 of 46,857 bytes, with no conflict at the gate and no trap in replay. Of the 11 samples in that set that load, 10 were rewritten and none failed replay.

The claims in these runs came from a small pattern matcher. The same harness can take them from a language model, which is never trusted: it can only name a structure for the checker to verify, or raise an objection that stops an automatic rewrite. No model run is recorded yet. The method, its assumptions and its limits are written up separately in the repository.

Three limits on the gate

It needs the ELF. Function boundaries come from the symbol table. A raw image without one gets the evidence bundle and no rewrite path.

The checker is separate, not independent. It is a second program that never imports the first, and it rebuilds the model from the firmware before comparing. But the same person wrote both, against the same rules, with the same decoder libraries. It catches a bug in the producer or a tampered artifact. It cannot catch an error in the rules they share, and it has had no outside review. The structure checker behind the newer runs has a single implementation.

The gate has opened only for code nothing refers to. On a 248-byte image built for the purpose, with 13 functions, the checker excluded 5. PRUNED Security signed a certificate for one of them, the dry run planned exactly 4 bytes, the operator switch applied them, and replay matched on 3 seeds. A trace that reports that function as executed turns the result into BLOCKED_CONFLICT. This shows that the gate can open and that it opens for exactly the certified bytes. On the public images it opened under four recorded assumptions, the heaviest of which is that an indirect call only ever reaches a function whose address is stored somewhere in the image. Nothing checks that assumption yet, and the replay behind those runs is the same shallow emulation described above.

CORRECTIONS

What the first draft got wrong

The first draft of this note reported 459 blocks kept and 2,005 unknown. Those numbers were wrong, and checking them is what showed it.

• The static walk stopped at every call. The library call used to list what follows a block leaves out the code after a call, and this kind of image has no return edges. So nothing after a call was ever reached, main() included.
• Executed addresses were credited to the wrong block. As a result, 37 blocks that the emulator had executed were labeled unknown. None are now.
• The vector table was declared too long. The extra words were the first function in the image, which was read as vectors and dropped from the analysis.
• Ordinary returns were listed as unbounded control transfers. There were 20. The recognizer matched one spelling of the return instruction and missed two others, in the producer and in the checker alike. The model listed 66 sites and now lists 46.
• A proof that contradicted observed execution did not raise a conflict. The code was kept either way, but it was reported as merely reachable and the warning was lost. It now blocks approval.
• The evidence bundle recorded a local file path. It now records the file name.

None of these could have authorized a change, because authorization never depended on keep-side evidence. All of them made the evidence wrong, and evidence is the product.

PRUNER's own comparison of the two evidence bundles shows the effect on identical firmware: 1,422 blocks moved from unknown to reachable, 21 moved the other way, and 5 are new to the analysis. That comparison is one of the things a pilot delivers.