2026-09-09 13:50:46 +02:00
|
|
|
|
# Overview — what this is, and what is actually true of it
|
|
|
|
|
|
|
|
|
|
|
|
**Written 2026-09-09.** Fourteen specs have accumulated and the roadmap still described a pre-Joern world, so
|
|
|
|
|
|
this is the synthesis above them: what the system does, what has been measured, and what is not true yet.
|
|
|
|
|
|
Every number here comes from a committed artifact in `benchmarks/measurements/`.
|
|
|
|
|
|
|
|
|
|
|
|
## What the tool is
|
|
|
|
|
|
|
|
|
|
|
|
A static analyser that separates **what it can prove from what it merely suspects**, and says which is which.
|
|
|
|
|
|
|
|
|
|
|
|
The thesis is not the dataflow engine — CodeQL and Semgrep have one and developers do not turn it on. It is
|
|
|
|
|
|
the **rung**: a claim you can act on without writing a query, and an explicit admission when the engine could
|
|
|
|
|
|
not decide.
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
execution_confirmed a test or sandbox reproduced it (built, no production caller)
|
|
|
|
|
|
model_entailed the graph decided: a flow with no discharge,
|
|
|
|
|
|
an obligation with no guard, a permissive value ← the product
|
|
|
|
|
|
model_corroborated the graph found the shape; a judge with
|
|
|
|
|
|
coverage agreed on the residual question
|
|
|
|
|
|
suspicion an enumerator or a pattern proposed it and
|
|
|
|
|
|
nothing corroborated it ← everything below the line is noise
|
|
|
|
|
|
until proven otherwise
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
Silence is not a clean bill of health. If no fact table covers a site, the model is **silent, not negative** —
|
|
|
|
|
|
23 of the 39 misses in the original entailment ceiling were sinks simply absent from the tables.
|
|
|
|
|
|
|
|
|
|
|
|
## How it works, in one pass
|
|
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
preprocess ─▶ entry-point map ─▶ MAP stage ─┬─ static patterns
|
|
|
|
|
|
├─ semantic overlay
|
|
|
|
|
|
├─ obligations (absence bugs)
|
|
|
|
|
|
├─ tool hunter (LLM)
|
|
|
|
|
|
└─ MODEL LAYER ──▶ one CPG per repository (Joern, subprocess)
|
|
|
|
|
|
├─ taint reachability + sanitizer lattice
|
|
|
|
|
|
├─ dominance guard governs obligated operation
|
|
|
|
|
|
└─ config constant abstraction over a value
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
Three abstractions, one arbiter each, dispatched on spec type so a family without an arbiter cannot be
|
|
|
|
|
|
silently routed to the wrong one. The CPG is built **once per scan** and every question is batched into one
|
|
|
|
|
|
invocation per query kind.
|
|
|
|
|
|
|
|
|
|
|
|
## What has been measured
|
|
|
|
|
|
|
|
|
|
|
|
| | measured | source |
|
|
|
|
|
|
|---|---|---|
|
|
|
|
|
|
| entailment, flat IR → CPG | 2.2% → **41.3%** of the corpus | `2026-09-08-model-entailment-ceiling*.json` |
|
|
|
|
|
|
| vibe-py pairs (30) | **90.0% pair-correct**, 6.7% leak, $0.0068 | `2026-09-08-pipeline-vibe-py.json` |
|
|
|
|
|
|
| — against the LLM hunter | 76.7% / 12.3% at 5× the calls, ~100× the cost | same |
|
|
|
|
|
|
| vampi (python, 520 lines) | **3 of 3** known vulnerabilities at `model_entailed` | `2026-09-09-repo-vampi-authz-precision.json` |
|
|
|
|
|
|
| vampi access-control precision | 28.6% → **50.0%** | same |
|
|
|
|
|
|
| access-control leak, pairs nobody tuned against | 42.9% → **0.0%**, pair-correct unchanged | same |
|
|
|
|
|
|
| libpng envelope (89k lines of C) | build 16s, query 250s, scan 446s, **911 MB** | `2026-09-09-repo-libpng-envelope.json` |
|
|
|
|
|
|
| libpng valid findings | **zero** | same |
|
|
|
|
|
|
| report proportionality | libpng 198 sections → **39** | `2026-09-09-report-proportionality.json` |
|
2026-09-09 17:25:16 +02:00
|
|
|
|
| **CVE-2023-23488, production plugin code** | **found at `class.memberorder.php:936`**, the exact line | `2026-09-09-pmpro-cve-found.json` |
|
|
|
|
|
|
| — precision on that file | 16 of 26 unprepared `$wpdb` queries; **0 of 26 use `->prepare`** | same |
|
2026-09-09 13:50:46 +02:00
|
|
|
|
|
|
|
|
|
|
## What is not true yet
|
|
|
|
|
|
|
|
|
|
|
|
- **The C story does not work.** `c/memory` has produced zero true positives and three distinct classes of
|
|
|
|
|
|
false one. It models string functions; libpng overflows through arithmetic, and its library code never
|
|
|
|
|
|
calls a sink we model. This is structural, not tuning.
|
2026-09-09 17:25:16 +02:00
|
|
|
|
- **Two languages are demonstrated.** Python end to end, and PHP on a real plugin slice where it found a
|
|
|
|
|
|
real CVE. Ruby and Go still have **zero families** — Joern parses them and the engine says nothing.
|
|
|
|
|
|
- **Not at repository scale for PHP.** The 637-file checkout does not load; the 2-file slice does. That
|
|
|
|
|
|
boundary is unmeasured (task 5.10).
|
2026-09-09 13:50:46 +02:00
|
|
|
|
- **The suspicion band is still too loud.** vampi emits 61 report sections for a 520-line application, 38 of
|
|
|
|
|
|
them a candidate the graph could not decide with a judge's opinion attached.
|
|
|
|
|
|
- **The evidence base is two repositories.** One has never produced a true positive.
|
|
|
|
|
|
- **Control dependence is unavailable.** 0 of 13,184 calls in the libpng CPG and 0 of 1,152 in vampi's have a
|
|
|
|
|
|
controlling control structure, so every guard question runs on CFG dominance instead.
|
|
|
|
|
|
- **`execution_confirmed` has no production caller.** The rung exists and nothing reaches it.
|
|
|
|
|
|
|
2026-09-09 17:25:16 +02:00
|
|
|
|
## What scoping is for, which is not what it looks like
|
|
|
|
|
|
|
|
|
|
|
|
The first real CVE was found by **cutting**, not by scanning more. Two of Paid Memberships Pro's 637 files —
|
|
|
|
|
|
the ones holding both ends of the bug — load in 9 seconds, query in 111, and report CVE-2023-23488 at the
|
|
|
|
|
|
exact line. The full checkout does not load at all.
|
|
|
|
|
|
|
|
|
|
|
|
That two-file slice **is the contributor case**. A developer editing `class.memberorder.php` gets precisely
|
|
|
|
|
|
that scan. So scoping is not a workaround for a scale problem; it is the thesis, and the scale problem is
|
|
|
|
|
|
what happens when the thesis is ignored.
|
|
|
|
|
|
|
|
|
|
|
|
The distinction that matters is not whether to cut but **who decides and whether the decision is recorded**:
|
|
|
|
|
|
|
|
|
|
|
|
| | decided by | recoverable afterwards |
|
|
|
|
|
|
| --- | --- | --- |
|
|
|
|
|
|
| **scoping** — a build declaration, a diff, a subtree | the project or the developer | yes, and it is in the artifact |
|
|
|
|
|
|
| **triage** — "this looks like boilerplate" | a model | no; if it drops the file with the bug, the scan reports clean |
|
|
|
|
|
|
|
|
|
|
|
|
Both give the same answer when the model is right. Only one of them tells you when it was wrong, and every
|
|
|
|
|
|
failure found on this checkout was of exactly that shape.
|
|
|
|
|
|
|
2026-09-09 17:04:04 +02:00
|
|
|
|
## Why a corpus of benchmarks is not enough on its own
|
|
|
|
|
|
|
|
|
|
|
|
This is the finding worth teaching, and it is not an opinion — it is what the gates say.
|
|
|
|
|
|
|
|
|
|
|
|
**Twelve engine defects were found in one session by pointing the tool at three real repositories. The three
|
|
|
|
|
|
gates stayed byte-identical through every single fix.** A gate that does not move is a corpus that could not
|
|
|
|
|
|
see the bug.
|
|
|
|
|
|
|
|
|
|
|
|
| defect | what the corpus saw |
|
|
|
|
|
|
|---|---|
|
|
|
|
|
|
| `resolve` matched inside `resolveUrl` (sanitizers) | nothing |
|
|
|
|
|
|
| `user` matched inside `users` (dischargers) | nothing |
|
|
|
|
|
|
| `gets` matched inside `fgets` (sinks) — 26 identical false positives | nothing |
|
|
|
|
|
|
| the model layer had zero production callers | nothing |
|
|
|
|
|
|
| `query_batch` implemented, tested, unreachable | nothing |
|
|
|
|
|
|
| a paid budget halting unpaid arbitration | nothing |
|
|
|
|
|
|
| a region with no function claiming the whole repository's answer | nothing |
|
|
|
|
|
|
| a guard discharging an obligation it is not a guard of | nothing |
|
|
|
|
|
|
| `joern-parse` failing where the frontend succeeds | nothing |
|
|
|
|
|
|
| a 1.49MB batch over Linux's 128KB argv cap | nothing |
|
|
|
|
|
|
| an array callable not recognised as a handler | nothing |
|
|
|
|
|
|
| one defect reported as twenty-six findings | nothing |
|
|
|
|
|
|
|
|
|
|
|
|
The reason is structural rather than a gap in the corpus's coverage. **A pair is a labelled function with a
|
|
|
|
|
|
declared family and a known answer.** It cannot exercise: which region to look at, what to spend, whether the
|
|
|
|
|
|
capability is even reachable, whether two entry points share a sink, whether the question fits in an argv
|
|
|
|
|
|
slot, or whether a flow crosses a module boundary. Every one of those is a property of a *repository*, and
|
|
|
|
|
|
none of them is a property of a function.
|
|
|
|
|
|
|
|
|
|
|
|
Three of the twelve are worse than invisible — they are **quiet failures**, where the tool produced a clean
|
|
|
|
|
|
report and every honesty counter agreed with it. The rung ladder labels a *verdict*; when no verdict is
|
|
|
|
|
|
produced there is nothing to label. That is the failure mode a benchmark score cannot express at all, because
|
|
|
|
|
|
the score is computed from the verdicts that exist.
|
|
|
|
|
|
|
|
|
|
|
|
So the corpus is necessary and not sufficient: it is the **holdout** that stops per-repository tuning, and it
|
|
|
|
|
|
is the wrong instrument for finding out whether the tool works. Both instruments, or neither number means
|
|
|
|
|
|
anything.
|
|
|
|
|
|
|
2026-09-09 13:50:46 +02:00
|
|
|
|
## The lesson that shaped the current specs
|
|
|
|
|
|
|
|
|
|
|
|
Nine engine defects were found in one session by pointing the tool at two real repositories. **Three were the
|
|
|
|
|
|
same bug in three matchers** — a spec token matched as a substring: `resolve` in `resolveUrl`, `user` in
|
|
|
|
|
|
`users`, `gets` in `fgets`. Two were a capability built and unreachable: the model layer itself, then the
|
|
|
|
|
|
query batcher. One was a paid budget stopping unpaid work.
|
|
|
|
|
|
|
|
|
|
|
|
The three gates stayed **byte-identical through every one of those fixes**. That is the finding: a corpus of
|
|
|
|
|
|
function-level pairs could not see any of them, and a repository showed all nine within minutes.
|
|
|
|
|
|
|
|
|
|
|
|
## Where the specs stand
|
|
|
|
|
|
|
|
|
|
|
|
| spec | phase | state |
|
|
|
|
|
|
|---|---|---|
|
|
|
|
|
|
| `contributor-scan` | implementation | 14 done, 15 open — **the active one** |
|
|
|
|
|
|
| `finding-feedback-loop` | design | requirements approved, design awaiting approval |
|
|
|
|
|
|
| `model-grounded-detection` | complete | 16/16; built the arbiter this all rests on |
|
|
|
|
|
|
| `authorization-obligations` | tasks approved | 24 open — superseded in practice by the dominance arbiter |
|
|
|
|
|
|
| `constrained-detector` | tasks | 4 of 20, tasks unapproved |
|
|
|
|
|
|
| `reachability-flow-model` | tasks generated | 23 open, nothing approved — largely delivered by adopting Joern |
|
|
|
|
|
|
| `learning-harness` | implementation | 30 done, 3 open |
|
|
|
|
|
|
| six others | complete | `pair-corpus-honesty`, `corpus-seeded-mechanisms`, `propose-adjudicate-prove`, `three-stage-scan`, `real-world-vfc-slice`, `harnessx-self-improving-rulesets`, `tree-sitter-overlay-extra` |
|
|
|
|
|
|
|
|
|
|
|
|
97 source modules, 90 load-bearing and 7 standalone capabilities; 814 tests.
|