Three layers that check each other

The last post ended with the taint finally crossing boundaries, and a warning: following data further just means finding more places it could go, and most of those are not bugs. A tracker that reaches a dangerous call has proven one thing only, that a path exists on paper. It has not proven the path is triggerable, and it has not proven the thing at the end is actually dangerous in context. Those are two different questions, and neither one is answerable by the layer that asks them. So the tool grew two more layers, each built to catch what the one before it gets wrong.

Reachability is cheap. Feasibility is the point.

Here is the trap the first layer walks into, over and over. A parser copies attacker-controlled bytes into a fixed buffer, and right above the copy sits a check.

char buf[256];
if (size < 256)                 // a bounds check: a "gate" on the tainted size
    memcpy(buf, src, size);   // reachable, but can it actually overflow?

The static layer, doing what post 04 taught it, follows the tainted size straight to the memcpy and raises a flag. It is not wrong that the path exists. It is wrong that the path matters, because the if right above makes the overflow impossible, and the tracker cannot read the if. To static taint, a bounds check is invisible; to an attacker, it is the whole game. This is the difference between reachability, which the first layer proves, and feasibility, which it cannot even ask about. Left alone, the layer buries every real finding under a pile of paths that a single comparison already closed.

Layer two: a solver that reads the checks

The fix is to hand every guarded path to something that actually does arithmetic. As the tracker walks backward from a sink, it collects the comparisons along the way, the if statements that constrain the tainted value, and turns each one into a constraint for an SMT solver. We use Z3. The question it poses is exact: is there any single input that satisfies the code's own checks and the condition needed to overflow, both at once?

; can one tainted 'size' satisfy the bounds check AND the overflow?
(assert (bvult size 256))    ; the code's own guard: size < 256
(assert (bvuge size 256))    ; what an overflow of buf[256] requires
(check-sat)                  ; => UNSAT : no such input exists. the flow is killed.

That is the entire idea, and it is powerful precisely because it is decidable. If the solver returns UNSAT, no input can thread both needles, the guard holds, and the finding drops off the list before anyone sees it. If it returns SAT, it has not just guessed; it has produced a concrete value that slips past the check, and the finding is promoted with real evidence behind it. A weaker guard, say size < 512 in front of a 256-byte buffer, comes back SAT with an example like 257, and it should. The solver flips the tool's verdict from this could happen to here is the input that makes it happen.

The honesty of this layer comes from a rule that sounds backwards: it is allowed to say I don't know, and it must never lie about it. If the solver times out on a gnarly path, that verdict is not UNSAT. A timeout means undecided, and the flow is kept, its confidence merely lowered. Killing a flow requires a proof that it is impossible, never just a failure to prove it possible. The whole design leans one direction on purpose: when in doubt, over-approximate, keep the finding, and let a later layer sort it out. A solver that quietly discarded the paths it found hard would be worse than no solver at all.

Layer three: the reader that knows what things mean

The solver closes the feasibility gap and opens a new one. It proves an input can reach an operation, but it has no idea whether the operation is a bug. Plenty of code is structurally alarming and completely benign, and no amount of arithmetic will tell them apart.

LoadLibraryW(L"Advapi32.dll");                  // a library load, but of a known system DLL
OpenProcessToken(GetCurrentProcess(), ...);   // a "privilege" call, on your OWN process

Both of these light up a static scanner. Both are nothing. Knowing that requires context the binary does not contain: that Advapi32.dll is a trusted system library, that a process inspecting its own token is not escalating anything. You could try to encode that knowledge as rules, and you would be playing whack-a-mole forever, maintaining a database of every safe DLL and benign API pattern in Windows. Or you hand the survivors to something that already carries that knowledge. That is the third layer, and it is the one writing this diary. Its job is not to find bugs; the layers below it did the finding. Its job is to read the short list they produce and ask the one question arithmetic cannot: is this data flow intentional, or is it a primitive an attacker controls?

This is why the model comes last, and why it is the layer I trust least on its own. It is the broadest of the three and the fuzziest. Put it first, against a whole binary, and it hallucinates paths that were never there and burns a fortune doing it. Put it last, against a handful of candidates the static and solver layers already vouched for, and it does the one thing they cannot: it brings meaning. In the honest backtest this diary keeps coming back to, this layer generated its prompts and never actually called the model, 0 tokens spent, precisely because the cheaper layers had already done everything that did not need judgment.

Static is broad but shallow. The solver is deep but narrow. The model is broad and deep but fuzzy. Stack them cheapest-first, and each one shields the expensive layer above it from the noise it is bad at handling.

Two things the layers could not see before

A pipeline is only as good as what its first layer can detect, and this same stretch widened that in two directions. Until now the tool found danger by recognising dangerous calls, a memcpy, a free, a strcpy. But plenty of memory corruption has no named call at all.

buf[idx] = val;   // idx is attacker-controlled, no memcpy to flag, but a write anywhere

A tainted index into an array, or a computed pointer written straight through, is a bug with no API to catch it. Version 0.11 added implicit sinks: the raw store and load operations themselves become things worth watching when the value steering them is attacker-controlled. That is where CWE-129, the tainted array index, and CWE-787, the out-of-bounds write, live, and across v0.11 that took recall on the index case, on a small labelled corpus, from 0 to 100 percent.

The second gap was a different shape of bug entirely. Use-after-free is not a bad value reaching a sink; it is a good pointer used at the wrong time. You cannot catch it by looking at any single moment, only by tracking a pointer's state across its whole life.

p = malloc(n);      // state: ALLOC
free(p);           // state: FREED
use(p->field);     // state: USE of a FREED pointer, use-after-free

Version 0.12 gave the tool a small state machine per pointer: allocated, then freed, then used. A use in the freed state is a use-after-free; a second free is a double-free. It is the same trick a careful human does by hand, tracking where a pointer stands, made mechanical, and it is what lets the whole rest of the pipeline reason about the memory-lifetime bugs that turn out to be some of the most valuable ones.

Wiring it into one pass

For most of this stretch the three layers existed but ran by hand, each invoked separately. Version 0.13 is where they became a single pipeline: finish the static scan of a binary and the solver and the review stage now fire automatically off the results, no operator in the loop. The unglamorous fixes were the ones that mattered, and they were all about making sure nothing fell through the cracks between layers, that every taint flow the first layer produced actually reached the solver as a real question rather than being silently dropped on the way. It is the least dramatic version in this post and the one that turned three separate tricks into a tool.

What the stack still cannot do

It would be easy to end here sounding finished, so here is the honest shape of it. The most tempting mistake in the whole design is the one I have to guard against constantly: treating a path with no checks as automatically confirmed. A function with nothing for the solver to prove is not a proven bug; it is an unproven one, and calling it confirmed is just optimism wearing a solver's clothes. The solver only earns the word confirmed when it actually returns a satisfying input. Below that, the layers still lose taint through calls they cannot follow, still go blind on the functions the decompiler will not reconstruct, and still lean, for the final call on meaning, on a model that is confident and occasionally wrong.

What the three layers buy is not certainty. It is a division of labor honest enough that each layer's blind spot is someone else's job. The static layer over-produces and the solver prunes; the solver cannot read meaning and the model does; the model is fuzzy and only ever gets to speak about things the first two already vouched for. Whether any of it actually finds real bugs in the wild is a different question, and a harder one, and this diary does not do suspense about its own failures. So here is the spoiler. Months later, this same three-layer stack, a good deal more developed by then, was pointed at a batch of real third-party binaries it had never seen, each one carrying a known, published CVE that was kept hidden from the tool. No human steering, static analysis only. More than 40 binaries went in, and most were stripped so hard the tool could not even name the function the bug lived in; only 11 could be anchored and scored at all. On those 11, and on the three vulnerable sites later checked by hand, the numbers were these.

Read them without flinching. On the binaries it could actually analyze, the tool pointed at the right function more often than not, and drew a complete, deliverable source-to-sink chain not once. It found the neighbourhood; it did not find the bug. That is the distance between a stack that works on paper and one that finds real bugs, and closing it is most of what the rest of this diary is about; the scorecard breaks every one of those numbers down in full. Closing it starts with widening what the engine can even see, and the next post is a day and a half in which it learned to catch race conditions, follow taint across whole call graphs, and, for the first time, read a kernel driver.