Two design questions answered by the entailment measurement.
IL, not AST. Our semantic/ir.py is a lossy AST projection -- flat call/bind
lists, no CFG, no PDG -- which is *why* entailment is 2.2%. Guard dominance is
a dominator-tree question and path-sensitive taint needs branch structure;
a flat bind list expresses neither. Real abstract interpretation is a fixpoint
over a CFG, so the substrate is a Code Property Graph: AST + CFG + PDG + call
graph in one queryable graph, taint as source->sink-minus-sanitizer
reachability, absence as dominance.
Adopt, not build. Building a multi-language CFG/PDG/taint engine on tree-sitter
is reinventing CodeQL/Semgrep/Joern -- the maximal case of this session's
failure mode. Joern is Apache-2.0, covers our exact corpus
(C/C++/Java/JS/Python/Kotlin/binary), has a taint engine, is embeddable, and a
CPG+LLM MCP bridge already exists. The 2.2% on our flat IR is the measured
distance to a real CPG, and closing it by hand is reimplementing Joern.
The flow: source -> Joern CPG -> taint + dominance -> deterministic
entailed/corroborated verdict -> LLM judges the residual, checked against the
CPG. What stays ours is the contribution: the taxonomy and the
source/sink/sanitizer/guard models for the web/logic CWEs, ported to CPG
queries, plus the LLM-checked-against-the-model orchestration. Joern is a
workbench with no opinion on these classes; that opinion is our layer. Named
cost: Joern is JVM/Scala, so server-mode or the MCP bridge, not in-process.
Three-layer adoption now: Joern CPG for the web/logic arbiter, Clearwing for
the memory/C execution tier, and our security modelling + LLM orchestration as
the layer that binds them.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
The analogue of the candidate ceiling, one rung up: not "can a site be
enumerated" (96.6%) but "can a deterministic abstract-interpretation model
DECIDE the vulnerability without trusting the LLM". Offline, no model calls.
model_entailed today 2.2% (2/92 web/logic pairs)
model_corroborated, one-hop taint 24% (22/92)
taint reachable, multi-hop 35% (26/74 flow families)
candidate site enumerable 96.6% (for comparison)
The gap between 96.6% and 2.2% is the gap between enumerating and arbitrating,
and it is the finding. The model cannot be a pure arbiter at v1. But the
measurement diagnoses depth, not impossibility: one-hop source resolution
(real taint sits 1-3 binds upstream: q = '...'+id; execute(q)), a closed
literal sink table (misses project wrappers and path/xss/prototype sinks), and
a function-naming gap that eats 20/50 injection pairs. Deepening the taint to
the candidate enumerator's depth-4 chain already moved injection 24% -> 48%.
So the course is a layered arbiter, not a pure one: report model_entailed
where the model proves it (deterministic, no LLM); let the LLM judge but check
its claim against the resolved taint on the ~35% corroboration band (noise
removed there); honest suspicion for the rest, which is where the deferred
execution/differential tier earns its place. Modeling confirmed as abstract
interpretation; SMT reserved for the memory/C tier; concolic avoided.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
Maintainer correction: execution isn't possible for all SAST targets, and the
bugs this project owns -- IDOR, missing authz, injection -- don't crash
anything. Execution is the easy arbiter only for memory-safety-in-C, which is
not our world.
What execution provided was an independent, deterministic arbiter of whether a
claim is real -- not the same LLM that made it, not a noisy vote. That arbiter
can be built statically, from the code, as a program model the claim is checked
against. LLM proposes; the model disposes. Same architecture, same repair of
the root cause, no runnable target required.
The evidence ladder becomes static and deterministic:
suspicion -> model_corroborated (claim consistent with resolved dataflow /
a guard its siblings carry is absent) -> model_entailed (the model alone
establishes it) -> execution_confirmed (deferred tier, C memory-safety only).
model_corroborated and above are deterministic -- run the checker twice, same
verdict -- which removes the run-to-run noise the same way a crash would, with
no K-runs and no target to build. Our IR candidate enumerator (96.6% ceiling),
binding chains and obligation checker stop being prompt context and become the
arbiter itself.
The course: promote those assets from inputs to arbiter, delete the noise
layer, make the LLM a proposer the model audits, keep the corpus as the
model's calibration set (the fix diff is what the model should see), and defer
execution to Clearwing for the memory-safety classes only. Build the arbiter we
can build from code; adopt the one we cannot, when a class demands it.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
