Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -351,9 +351,10 @@ The [taint-modeling matrix](docs/modeling-matrix.md) is a separate tier that
asks a separate question: not whether an engine can follow flow it can see, but
whether it can be **told** things. Each language row is twenty-four
benchmark-controlled modeling assertions, four per-adapter model encodings, and
one run per adapter against them:
[the Python taint-modeling matrix](docs/python-modeling.md) and
[the JavaScript taint-modeling matrix](docs/javascript-modeling.md). Modeling
one run per adapter against them. Wave M1's three rows are complete:
[the Python taint-modeling matrix](docs/python-modeling.md),
[the JavaScript taint-modeling matrix](docs/javascript-modeling.md), and
[the Java taint-modeling matrix](docs/java-modeling.md). Modeling
cases are `score_tier: "modeling"`, are never in a core denominator, and are
never averaged with a kernel score.

Expand Down
39 changes: 39 additions & 0 deletions adapters/bifrost/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -614,3 +614,42 @@ invoked and retained verbatim with the document's own rationale.
The declaration, not the propagation, is what the cell scores.

See [the JavaScript modeling matrix](../../docs/javascript-modeling.md).

## Java taint-modeling matrix

Wave M1's last row, and the same shape as the two above. The
[modeling matrix](../../docs/modeling-matrix.md) gives this adapter **category S
alone** — declared sources and declared sinks, two of the twelve templates —
and the other five categories are `unsupported` for the standalone policy CLI,
decided from the template identity before the binary is invoked and retained
verbatim with the document's own rationale.

- Artifact: `adapters/bifrost/policies/model-java.rqlp`. Two `:sources` entries
bound to `return-value`, two `:sinks` entries bound to
`(argument :index 0)`, and nothing for categories P, Z, O, E, or B.
- Load-bearing model: the policy sets `:call-modeling (call-modeling :unmodeled
require-model)`. The preregistration recorded the pinned CLI's *acceptance* of
that setting as one of two unverified facts behind Bifrost's category-P cell;
it is now confirmed by
[Amendment A5](../../docs/modeling-matrix.md#a5--2026-08-26-bifrost-v0106-accepts-unmodeled-require-model),
which moves no cell. The other obstacle — showing that a propagator or
transform section actually lowers — is untouched, so category P stays
`unsupported`.
- Invocation:
`cargo run -- run-bifrost-modeling --language java --bifrost <path>`, writing
`reports/bifrost-java-modeling.json` with raw evidence under
`reports/raw/bifrost-java-modeling/`.
- Result on the pinned build: **all four scored assertions decided correctly** —
two `reached` positives, two `not-reached` negatives, no `inconclusive` and no
`runner-error`, with neither undeclared sibling (`Config.fetchLocal`,
`Audit.discard`) picked up. That is Python's row exactly, and it is the
difference between Java and JavaScript: the JavaScript slice's three
`inconclusive` cells are that language's engine incompleteness, not a modeling
property. Its configuration hash is
`921d2c8e531813bf7c9bb93fd6da710e62020f60f9caadc7ac0096c5c31121d9`.
- **Load-bearing verification.** Removing the `Config.fetchRemote` source entry
from a copy of the policy drops `model-declared-source-positive` from one
finding to zero
(`reports/raw/load-bearing-java-modeling/bifrost-declared-source-{with,without}-model.json`).

See [the Java modeling matrix](../../docs/java-modeling.md).
14 changes: 14 additions & 0 deletions adapters/bifrost/policies/model-java.rqlp
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
(policy
:schema-version 1
:id "dataflowbench.taint.model-java"
:name "DataFlowBench Java taint-modeling matrix"
:message "A benchmark-declared model carried input to the declared sink"
:severity warning
:analysis (analysis :type taint :mode may
:call-modeling (call-modeling :unmodeled require-model)
:sources (endpoint-set :entries [
(source :id input :display-name "benchmark input" :categories [input.user-controlled] :selector (rql :schema-version 1 (language java (call :callee (name "dfb_source")))) :bind return-value :labels [attacker-controlled])
(source :id declared-source :display-name "Config.fetchRemote" :categories [input.user-controlled] :selector (rql :schema-version 1 (language java (call :callee (name "fetchRemote")))) :bind return-value :labels [attacker-controlled])])
:sinks (endpoint-set :entries [
(sink :id sink :display-name "benchmark sink" :categories [data.sensitive] :selector (rql :schema-version 1 (language java (call :callee (name "dfb_sink")))) :dangerous-operand (argument :index 0) :accepts [attacker-controlled])
(sink :id declared-sink :display-name "Audit.record" :categories [data.sensitive] :selector (rql :schema-version 1 (language java (call :callee (name "record")))) :dangerous-operand (argument :index 0) :accepts [attacker-controlled])])) )
43 changes: 43 additions & 0 deletions adapters/codeql/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -918,3 +918,46 @@ source even when both denote the same store, and comparing local sources linked
nothing.

See [the JavaScript modeling matrix](../../docs/javascript-modeling.md).

## Java taint-modeling matrix

Wave M1's last row. Same partition — **all six categories scored** — and the
same single `DataFlow::ConfigSig` carrying every declaration role, written in
Java's own vocabulary: `MethodCall` and `getArgument` where the JavaScript query
uses `DataFlow::CallNode`.

- Artifact: `adapters/codeql/queries/JavaModeling.ql`. This is the one modeling
query that sits on the preregistration's *schematic* path rather than under a
`<language>/queries/` subdirectory, and for the same reason the other two sit
off it: a modeling query must live inside its language's existing `qlpack`,
and Java's pack **is** the adapter root. `adapters/codeql/qlpack.yml` declares
`dataflowbench/codeql-java` with the `codeql/java-all` dependency, and
`queries/JavaKernel.ql` already lives beside it; there is no
`adapters/codeql/java/` pack, and a query placed under one would resolve
nothing. A test asserts that every modeling query resolves a `qlpack.yml` two
directories up.
- The database is built from a **traced `javac`**, exactly as the Java kernel
builds it — the Java extractor has no `--build-mode=none` — so the modeling
run differs from its kernel sibling only in which query it loads.
- Invocation:
`cargo run -- run-codeql-modeling --language java --codeql <path>`
(optionally `--codeql-packs <dir>`), writing
`reports/codeql-java-modeling.json` with raw SARIF under
`reports/raw/codeql-java-modeling/`.

**Result on the pinned CLI: 24 of 24 assertions match** — twelve `reached`
positives and twelve `not-reached` negatives, no `inconclusive` and no
`runner-error`, across all six categories. That is the third clean sweep in
three languages, and it is what establishes that the twelve templates are
satisfiable as preregistered rather than badly posed. Its configuration hash is
`38acb5de67ed39a244c7eb8a9db755ddbcf197488051a5f1ec0d35b65fa30aee`.

**Load-bearing verification** is the category-P probe in
`scripts/probe-java-modeling-load-bearing.sh`: the same database analyzed with
and without the five-line `Opaque.carry` propagator step returns one SARIF
result and then zero
(`reports/raw/load-bearing-java-modeling/codeql-opaque-propagator-{with,without}-model.sarif.json`).
CodeQL does not follow `Opaque.class.getMethod(…).invoke(…)` on its own — which,
on the same fixture, [Joern does](../joern/README.md#taint-modeling-matrix).

See [the Java modeling matrix](../../docs/java-modeling.md).
177 changes: 177 additions & 0 deletions adapters/codeql/queries/JavaModeling.ql
Original file line number Diff line number Diff line change
@@ -0,0 +1,177 @@
/**
* @name DataFlowBench Java taint-modeling matrix
* @description Encodes the twelve benchmark-supplied model declarations of
* docs/modeling-matrix.md natively in CodeQL's data-flow
* configuration surface, for the Java modeling population.
* @kind path-problem
* @problem.severity warning
* @precision high
* @id dataflowbench/java-taint-modeling
* @tags security
*/

import java
import semmle.code.java.dataflow.DataFlow
import semmle.code.java.dataflow.TaintTracking

/**
* Entity identity, as the model declaration language defines it: a declaring
* type plus a member name. Binding is never by name shape and never by a
* substring, so `Audit.record` says nothing about `Audit.discard`.
*/
predicate modelCall(MethodCall call, string type, string member) {
call.getMethod().getDeclaringType().getName() = type and
call.getMethod().getName() = member
}

/** The string constant a store call is keyed by. */
predicate storeKey(MethodCall call, string key) {
call.getArgument(0).(CompileTimeConstantExpr).getStringValue() = key
}

/**
* Whether two store calls address the same store identity.
*
* Template 11 binds the store to the type: `Store.put` and `Store.get` are
* static, so neither call carries an instance receiver — a static call's
* qualifier is the `TypeAccess`, never a variable. Template 12 binds it to the
* receiver instance, so the two calls must name the same variable.
*/
predicate sameStore(MethodCall put, MethodCall get) {
put.getQualifier().(VarAccess).getVariable() = get.getQualifier().(VarAccess).getVariable()
or
not put.getQualifier() instanceof VarAccess and not get.getQualifier() instanceof VarAccess
}

module DataFlowBenchModelingConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) {
// The benchmark's own canonical source. Every fixture that is not itself a
// declared-source assertion starts here.
exists(MethodCall call |
call.getMethod().getName() = "dfb_source" and
source.asExpr() = call
)
or
// Template 1 — role `source`, entity `Config.fetchRemote`, out: return.
// The undeclared sibling `Config.fetchLocal` is deliberately absent.
exists(MethodCall call |
modelCall(call, "Config", "fetchRemote") and
source.asExpr() = call
)
or
// Templates 9 and 10 — role `entry-point`, entities `Handler.onRequest`
// and `Handler.onDeclared`, in: 0 tainted on entry. Neither method is
// called from anywhere in its fixture; CodeQL's data flow does not require
// a source to be reachable from a call-graph root. The undeclared siblings
// `onIgnored` and `onUndeclared` are deliberately absent.
exists(Method handler |
handler.getDeclaringType().getName() = "Handler" and
handler.getName() = ["onRequest", "onDeclared"] and
source.asParameter() = handler.getParameter(0)
)
}

predicate isSink(DataFlow::Node sink) {
// The benchmark's own canonical sink.
exists(MethodCall call |
call.getMethod().getName() = "dfb_sink" and
sink.asExpr() = call.getArgument(0)
)
or
// Template 2 — role `sink`, entity `Audit.record`, in: 0. The undeclared
// sibling `Audit.discard` is deliberately absent.
exists(MethodCall call |
modelCall(call, "Audit", "record") and
sink.asExpr() = call.getArgument(0)
)
}

predicate isBarrier(DataFlow::Node node) {
// Templates 5 and 6 — role `sanitizer`, entity `Clean.scrub`, in: 0.
// `Clean.sanitize` is a sibling with the same identity body and a name at
// least as sanitizer-shaped, and it is not declared.
exists(MethodCall call |
modelCall(call, "Clean", "scrub") and
node.asExpr() = call.getArgument(0)
)
or
// The explicit no-flow declarations the model language allows where a tool
// has one: template 3's `Opaque.block` and template 7's `Bridge.hold`.
// Both bodies say flow — `hold`'s is the identity function — so without
// these clauses the query would report the body's semantics rather than
// the summary's, which is exactly the distinction category O exists to
// make observable.
exists(MethodCall call |
modelCall(call, "Opaque", "block") and
node.asExpr() = call.getArgument(0)
)
or
exists(MethodCall call |
modelCall(call, "Bridge", "hold") and
node.asExpr() = call.getArgument(0)
)
}

predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
// Template 3 — role `propagator`, entity `Opaque.carry`, in: 0, out: return.
exists(MethodCall call |
modelCall(call, "Opaque", "carry") and
node1.asExpr() = call.getArgument(0) and
node2.asExpr() = call
)
or
// Template 4 — role `propagator`, entity `Opaque.select`, in: 1, out: return.
// Positional fidelity is native: the step names argument 1 specifically, so
// taint at the undeclared position 0 never takes it.
exists(MethodCall call |
modelCall(call, "Opaque", "select") and
node1.asExpr() = call.getArgument(1) and
node2.asExpr() = call
)
or
// Template 7 — role `summary`, entity `Bridge.pass`, in: 0, out: return.
exists(MethodCall call |
modelCall(call, "Bridge", "pass") and
node1.asExpr() = call.getArgument(0) and
node2.asExpr() = call
)
or
// Template 8 — role `summary`, entity `Bridge.deposit`, in: 0,
// out: `1.payload`. The output position is a heap location, so the step
// lands on the reads of that field of that object rather than on a return
// value. `deposit`'s body writes nothing, so the field's contents come
// from this declaration or from nowhere, and the sibling field `spare`
// takes no step.
exists(MethodCall call, FieldRead read |
modelCall(call, "Bridge", "deposit") and
read.getField().getName() = "payload" and
read.getQualifier().(VarAccess).getVariable() =
call.getArgument(1).(VarAccess).getVariable() and
node1.asExpr() = call.getArgument(0) and
node2.asExpr() = read
)
or
// Templates 11 and 12 — roles `store-write` and `store-read` sharing one
// store identity. `Store.put` binds in: 1 under key: 0; `Store.get` binds
// out: return under key: 0. The two close a roundtrip only when the key
// constants agree and the store identities agree, which is what the
// field-separation and object-separation negatives test.
exists(MethodCall put, MethodCall get, string key |
modelCall(put, "Store", "put") and
modelCall(get, "Store", "get") and
storeKey(put, key) and
storeKey(get, key) and
sameStore(put, get) and
node1.asExpr() = put.getArgument(1) and
node2.asExpr() = get
)
}
}

module DataFlowBenchModelingFlow = TaintTracking::Global<DataFlowBenchModelingConfig>;

import DataFlowBenchModelingFlow::PathGraph

from DataFlowBenchModelingFlow::PathNode source, DataFlowBenchModelingFlow::PathNode sink
where DataFlowBenchModelingFlow::flowPath(source, sink)
select sink.getNode(), source, sink, "A benchmark-declared model carried input to the declared sink."
64 changes: 64 additions & 0 deletions adapters/joern/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -965,3 +965,67 @@ name, so the category-B declaration cannot attach to it. Re-running the same
declarations against an object-literal spelling in which the call *does* resolve
and the semantics *are* found still produces zero flows, so the published
outcome is the same either way.

## Java modeling matrix

`run-joern-modeling --language java` runs the same twenty-four cells for Java —
**sixteen scored and eight preregistered `unsupported`** — through the same
`modeling.sc` and the same `--param` surface documented above, with
`language=JAVASRC` and
`semanticsPath=adapters/joern/semantics/model-java.semantics`. Everything in the
Python section about the script, the selector shapes, and the parser's silent
failure modes applies unchanged; only the semantics file and the frontend
differ.

**Result on the pinned distribution: 14 of 16 scored assertions match** — 6
`reached` positives and 8 `not-reached` negatives, with no false positive, no
`inconclusive`, and no `runner-error`. Categories S, Z, and E are 4/4; category
B is 2/4, its two positives being false negatives. Its configuration hash is
`55282607023d6902aebe9e2e4199542f04b407229ac0ab04eab9b70dd4a6980f`. That is the
same shape as the Python and JavaScript rows, cell for cell.

**Load-bearing verification, on category Z:** removing the
`"dataflowbench.taint.Clean.scrub:java.lang.String(java.lang.String)"`
`NilSemantics` entry turns `model-sanitizer-kill-negative` from 0 flows into 1,
the same demonstration the other two rows record
(`reports/raw/load-bearing-java-modeling/joern-sanitizer-kill-{with,without}-model.json`).

### `javasrc2cpg` binds where `jssrc2cpg` cannot

The JavaScript row records that `jssrc2cpg` gives a class-method call the method
full name `<unknownFullName>`, so its category-B declaration cannot attach at
all. Java has no such problem: `javasrc2cpg` spells the same entity
`dataflowbench.taint.Store.put:void(java.lang.String,java.lang.String)`, a
stable, file-independent full name, and the declaration binds cleanly.

The two category-B positives are false negatives anyway. That is the point of
publishing both rows: taint deposited on the receiver by `put` does not survive
into a separate procedure's `get`, on this engine, whether or not the
declaration binds. The limitation the cell measures is the engine's, and Python,
JavaScript, and Java all reach it by different routes.

### Amendment A4, extended: the reflective body is followed unaided here too

`reports/raw/load-bearing-java-modeling/joern-opaque-propagator-unmodeled.json`
runs `model-opaque-propagator-positive` under the committed Java semantics file,
which after A2 declares nothing at all for category P, and records
`declared_semantic_count: 3` with `flow_count: 1`. The pinned engine follows
`Opaque.class.getMethod(target, String.class).invoke(null, value)` on its own,
through `Method.invoke`'s `Object[]` argument.

[Amendment A4](../../docs/modeling-matrix.md#a4--2026-08-26-the-reflective-opaque-propagator-body-is-not-unfollowable-by-joerns-jssrc2cpg)
was measured on `jssrc2cpg` and withdrew the preregistration's claim as a
*general* one, leaving each language to stand on its own evidence. This is
Java's, on a different reflective construct, and it agrees; A4 carries it as a
dated addendum. No cell moves: A2 had already withdrawn Joern's category-P cells
for the stronger reason.

**The Java semantics file carries no comments**, where Python's and
JavaScript's carry `#` ones. The pinned parser drops every declaration on a
blank line and on a `//` comment, and on this file a leading comment was
measured to produce the same empty parse, so the file is declarations only and
its commentary lives in [the Java modeling matrix](../../docs/java-modeling.md).
`modeling.sc` raises on an empty parse, so a silent drop is a `runner-error`
rather than a scored cell decided by a missing model.

See [the Java modeling matrix](../../docs/java-modeling.md).
3 changes: 3 additions & 0 deletions adapters/joern/semantics/model-java.semantics
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
"dataflowbench.taint.Clean.scrub:java.lang.String(java.lang.String)"
"dataflowbench.taint.Store.put:void(java.lang.String,java.lang.String)" 2 -> 0
"dataflowbench.taint.Store.get:java.lang.String(java.lang.String)" 0 -> -1
Loading
Loading