diff --git a/docs/adapters.md b/docs/adapters.md index 254930b3..6f89d76b 100644 --- a/docs/adapters.md +++ b/docs/adapters.md @@ -297,10 +297,13 @@ their own. So the runner reads each artifact before the run and refuses it unless the default is disabled: a Bifrost modeling policy must set `:call-modeling (call-modeling :unmodeled require-model)` and must not name the kernel policies' `optimistic`, and a Semgrep modeling rule must set `options: -taint_assume_safe_functions: true`. Tests pin both strings. CodeQL and Joern -have no such switch to pin — a `ConfigSig` with no `isAdditionalFlowStep` adds -no step and a Joern method with no `FlowMapping` propagates nothing — so -neither is gated. +taint_assume_safe_functions: true`. Tests pin both strings. CodeQL has no +such switch to pin — a `ConfigSig` with no `isAdditionalFlowStep` adds no +step. Joern's equivalent claim ("a method with no `FlowMapping` propagates +nothing") was measured false by the first wave-M1 run: `FlowSemantic` +mappings on the pinned 4.0.610 are additive over the engine's default +pass-through, which is why Amendment A2 moved Joern's propagator and summary +categories to unsupported activation rather than gating them. **The execution arm lands with the language.** Today every modeling command stops at the population gate, because no fixture exists. The arm that invokes diff --git a/docs/modeling-matrix.md b/docs/modeling-matrix.md index d0b7c6a0..b7fe2b3a 100644 --- a/docs/modeling-matrix.md +++ b/docs/modeling-matrix.md @@ -878,6 +878,11 @@ whether the resulting semantics match — which is what the assertions measure. ### Joern — 4.0.610 +> **Amended.** Categories P and O were moved to unsupported activation by +> Amendment A2 after the first wave-M1 run measured `FlowSemantic` as +> additive rather than restrictive; Joern's scored set is S, Z, E, B. + + Verified surface: the OSS data-flow engine ships a flow-semantics loader — `io.joern.dataflowengineoss.semanticsloader` with `FlowSemantic`, `FlowMapping`, `FlowPath`, `ParamOrRetNode`, `NilSemantics`, `NoCrossTaintSemantics`, and @@ -904,6 +909,12 @@ scoped to a separate `modeling.sc` so the kernel script is untouched. ### Semgrep CE — 1.174.0 (`--oss-only`) +> **Amended.** Template 6 (sanitizer-selectivity) was moved to unsupported +> activation by Amendment A3: the mandated safe-function assumption and +> selectivity cannot coexist in one invocation. Semgrep's scored set is +> five templates. + + This partition is **verified by execution** against the pinned CE binary (`semgrep 1.174.0`, `--oss-only`), on small Python probes, before any fixture exists. Each cell below states what was run and what came back. @@ -1138,4 +1149,49 @@ Restating the obligations this tier is most at risk of eroding: ## Amendments -None yet. This document has not been amended since it merged. +### A2 — 2026-08-26: Joern's propagator and summary categories are not load-bearing + +**What changed.** Joern's cells for category P (`opaque-propagator`, +`propagator-position`) and category O (`summary-through`, `summary-field`) +move from scored to **unsupported activation**. Its scored modeling set is +now the eight templates of categories S, Z, E, and B. + +**Why.** The first wave-M1 run (Python) probed the load-bearing contract and +found that on the pinned 4.0.610, `FlowSemantic` mappings are **additive** +over the engine's default unmodeled-call pass-through and cannot restrict +it: removing the propagator declaration leaves the finding standing, and a +declared positional mapping does not exclude the undeclared position — so a +P or O result scores the engine's optimism, not the model. A summary's +field-destination access path is likewise ignored (the whole object is +tainted), resolving that cell's to-be-verified marker negatively. Category Z +remains scored: `NilSemantics` was demonstrated genuinely load-bearing +(removing it restores the flow). The preregistration's stated justification +for leaving Joern ungated — "a method with no `FlowMapping` propagates +nothing" — was measured false and is corrected by this amendment. + +**Tools, templates, and languages touched.** Joern only; templates 3, 4, 7, +8; all wave-M1 languages (the limitation is engine-level, verified on +Python, expected identical elsewhere and to be confirmed by each language's +retained evidence). + +**Freezes invalidated.** None. No modeling report is bound by any freeze. + +### A3 — 2026-08-26: Semgrep's sanitizer-selectivity cell is undecidable by construction + +**What changed.** Template 6 (`sanitizer-selectivity`) moves from scored to +**unsupported activation** for Semgrep CE, by a template-level override; its +category sibling, template 5 (`sanitizer-kill`), remains scored. Semgrep's +scored modeling set is now five templates. + +**Why.** The preregistration mandates `taint_assume_safe_functions: true` +so that propagator models stay load-bearing — and that same option +suppresses flow through the *undeclared* sanitizer-lookalike that template +6's positive requires. Selectivity and the safe-function assumption cannot +coexist in a single CE invocation, so the cell's positive is undecidable by +construction rather than by capability: the first wave-M1 run recorded it +as Semgrep's only false negative before this amendment reclassified it. + +**Tools, templates, and languages touched.** Semgrep CE only; template 6; +all wave-M1 languages. + +**Freezes invalidated.** None. diff --git a/src/main.rs b/src/main.rs index e9c17ae1..5cabbd79 100644 --- a/src/main.rs +++ b/src/main.rs @@ -696,7 +696,16 @@ const MODELING_PARTITION: [ModelingPartitionCell; 24] = [ ModelingPartitionCell { tool: ModelingTool::Joern, category: ModelingCategory::Propagators, - unsupported_reason: None, + // Amendment A2: FlowSemantic mappings on the pinned 4.0.610 are + // additive over the engine's default argument pass-through and cannot + // restrict it, so a propagator declaration is not load-bearing — the + // default decides the cell with or without the model. + unsupported_reason: Some( + "Joern 4.0.610 FlowSemantic mappings are additive over the \ + default unmodeled-call pass-through and cannot restrict it; a \ + propagator model is not load-bearing on the pinned version \ + (Amendment A2)", + ), }, ModelingPartitionCell { tool: ModelingTool::Joern, @@ -706,7 +715,16 @@ const MODELING_PARTITION: [ModelingPartitionCell; 24] = [ ModelingPartitionCell { tool: ModelingTool::Joern, category: ModelingCategory::Summaries, - unsupported_reason: None, + // Amendment A2: same additivity, and the field-destination access + // path of a summary (arg -> field of arg) is ignored — the whole + // object is tainted — so a summary model is likewise not + // load-bearing on the pinned version. + unsupported_reason: Some( + "Joern 4.0.610 ignores a summary's field-destination access path \ + and its FlowSemantic cannot restrict the default pass-through; \ + a summary model is not load-bearing on the pinned version \ + (Amendment A2)", + ), }, ModelingPartitionCell { tool: ModelingTool::Joern, @@ -761,10 +779,33 @@ const MODELING_PARTITION: [ModelingPartitionCell; 24] = [ /// identity alone: `None` when the category is scored, `Some(reason)` when the /// tool declines it. Every cell is present, so an unknown template is a /// programming error rather than a silent scored default. +/// Template-level partition overrides (Amendment A3): consulted before the +/// category cell, for the cells where a tool's capability splits within a +/// category. Semgrep CE can score sanitizer-kill (template 5) but not +/// sanitizer-selectivity (template 6): the mandated +/// `taint_assume_safe_functions: true` — required to keep propagator models +/// load-bearing — itself suppresses flow through the undeclared +/// sanitizer-lookalike, so selectivity's positive is undecidable by +/// construction in a single CE invocation. +const MODELING_TEMPLATE_OVERRIDES: [(ModelingTool, &str, &str); 1] = [( + ModelingTool::Semgrep, + "dfb-template-model-sanitizer-selectivity", + "Semgrep CE cannot express sanitizer selectivity and the safe-function \ + assumption in one invocation: taint_assume_safe_functions suppresses \ + flow through the undeclared sanitizer-lookalike, so the positive is \ + undecidable by construction (Amendment A3)", +)]; + fn modeling_partition_reason(tool: ModelingTool, template: &str) -> Result> { let category = modeling_category(template).with_context(|| { format!("{template:?} is not one of the twelve preregistered modeling templates") })?; + if let Some((_, _, reason)) = MODELING_TEMPLATE_OVERRIDES + .iter() + .find(|(t, id, _)| *t == tool && *id == template) + { + return Ok(Some(reason)); + } MODELING_PARTITION .iter() .find(|cell| cell.tool == tool && cell.category == category) @@ -12668,9 +12709,12 @@ mod tests { #[test] fn modeling_partition_scored_counts_match_the_preregistration() { assert_eq!(modeling_supported_templates(ModelingTool::Bifrost).len(), 2); - assert_eq!(modeling_supported_templates(ModelingTool::Semgrep).len(), 6); + // Amendment A3 moved sanitizer-selectivity out of Semgrep's scored set. + assert_eq!(modeling_supported_templates(ModelingTool::Semgrep).len(), 5); assert_eq!(modeling_supported_templates(ModelingTool::Codeql).len(), 12); - assert_eq!(modeling_supported_templates(ModelingTool::Joern).len(), 12); + // Amendment A2 moved Joern's propagator and summary categories to + // unsupported: FlowSemantic is additive on the pinned 4.0.610. + assert_eq!(modeling_supported_templates(ModelingTool::Joern).len(), 8); } /// Bifrost enters with category S alone — the honest starting position the @@ -12712,6 +12756,10 @@ mod tests { ] { expected.extend(category.templates()); } + // Amendment A3: sanitizer-selectivity is template-overridden out of + // Semgrep's scored set — the safe-function assumption and selectivity + // cannot coexist in one CE invocation. + expected.retain(|template| *template != "dfb-template-model-sanitizer-selectivity"); expected.sort_unstable(); let mut scored = modeling_supported_templates(ModelingTool::Semgrep); scored.sort_unstable();