Skip to content

fix(core): Mitigate fact explosion on some projects - #392

Draft
Saloed wants to merge 129 commits into
saloed/5-default-getfrom
saloed/42-proof-guided-any-compression
Draft

Saloed wants to merge 129 commits into
saloed/5-default-getfrom
saloed/42-proof-guided-any-compression

Conversation

@Saloed

@Saloed Saloed commented Sep 1, 2026

Copy link
Copy Markdown
Contributor

No description provided.

misonijnik and others added 30 commits August 27, 2026 20:21
…e star

Replaces the two hard-coded Spring hacks with rule-level star operators: the
controller parameter source is now `$*UNTRUSTED`, and the controller-return
any-field sinks are expressed with a starred metavar. Both the source hack and
the sink hack are deleted.

Also restores the Z2F-gate bypass for controller-return sinks and tightens the
source `$TYPE` regex, which the hack had been masking.
Keeps array and primitive parameters as plain value sources, stars the
untrusted-path-source pattern-not with a fresh metavar, drops the List adapter
overloads from the command-injection sink, and collapses the servlet upload
source read-back -- all expressible directly now that a starred metavar means
whole-object taint.

Documents the pattern-not star limitation, the sink focus requirement and the
Go parity story in the rules README.
resolveArrayPosition was the last implicit type-triggered array mechanism: it
silently gave every array- or Object-typed source ASSIGN position an element
twin. The star operator expresses the same thing from the rules, and does it
better -- the any-field star is recursive, so it also catches the deep
Map<String,String[]> flows the element-only twin missed.

Array and vararg sink args are now starred explicitly, the implicit sink
any-field emission is gone, and the Go side drops its blanket any-accessor
emission in favour of explicit variadic taint in the Go model config.
Makes the servlet source whole-object and adds the channel-model getter
passthroughs it reads back, and stars the xss and response-injection value
sanitizers so a sanitized wrapper is recognised as clean at every depth.
Collapses the source down to a single focused form, focuses and stars the
session-store sink, and flags a tainted attribute NAME as well as a tainted
value -- previously only the value was considered.
Makes the java.io.File model field-sensitive with starred path sinks, and
migrates every starred metavar in the ruleset, the Spring rule provider and the
rules README to the $*VAR spelling the parser accepts.
misonijnik and others added 18 commits August 27, 2026 18:23
Adds phase3/CoverageBeanIsolation.{java,yaml} + Phase3BeanIsolationTest.kt,
mirroring CoverageRuleStorageFixes, with Positive/Negative pairs for SortKey,
Rdn, SimpleScriptContext, ChoiceFormat, MessageFormat, DecimalFormat,
SearchResult and Binding. ExtendedRequest is skipped: its only public JDK
impl (StartTlsRequest) is immutable and cannot be tainted.

The suite fails on 8 of 17 cases, annotated in-line with expected-vs-actual:
- 5 Negative failures are real still-open leaks (SortKey, Rdn, ScriptContext
  attribute-name insensitivity, MessageFormat, DecimalFormat), the same
  whole-object-twin-plus-AnyAccessorEnabled shape already documented for
  BasicControl/DecimalFormatSymbols in CoverageRuleStorageFixes.java.
- 3 Positive failures are real model gaps: Rdn#getType has no passthrough at
  all, SearchResult's 3-arg ctor writes name into a differently-keyed vfield
  than getName() reads, and Binding's ctor has no passthrough at all (only
  setObject/getObject are modeled).

No changes under model/, rules/, or scripts/; no case weakened or ignored.
See .superpowers/sdd/bean-isolation-report.md for full details.
…ose remaining gaps

Removes NegativeScriptContextDifferentAttributeNoLeak: it asserted
that javax.script.ScriptContext#setAttribute("k", ...) does not reach
getAttribute("other"), but the single, name-insensitive
.ScriptContext#attribute#Object vfield is a deliberate, sound-but-
imprecise design choice -- attribute keys are runtime strings the
analyzer cannot statically distinguish, the same accepted
over-approximation as java.util.Map's MapValue slot. Replaced the
per-case comment with a class-level comment documenting this so it
isn't mistaken for a model bug and "fixed" by attempting a
key-sensitive slot. PositiveScriptContextAttribute is kept.

Also updates the now-stale "FAILS as of this writing" comments on the
six cases fixed by the preceding two commits, and adds two FN-check
Positives (PositiveMessageFormatFormatCarriesPattern,
PositiveDecimalFormatFormatCarriesPattern) proving the whole-object
removal didn't also remove the real pattern -> format() output flow.
…external getter

Verifies the mechanism the conductor response-source stars rely on: $*P marks
every field of an object, and a field-sensitive external getter (modeled
this.<slot> -> result, here NameClassPair#getName reading .name#) propagates
that mark to the sink. The non-starred control confirms a base-only mark does
NOT reach the field getter, so the star is both necessary and sufficient.
Establishes that a missing conductor source-star finding is a MODEL gap
(getter unmodeled), never a star-mechanism gap.
unrollAccessor excluded the literal field name "<rule-storage>" from
any-accessor unrolling, so a starred value would not subsume the synthetic
carrier the passthrough models wrote into.

The config no longer has that name: every slot it guarded is now an ordinary
field, either split into per-property fields where the owner conflated several
of them or renamed to the one store it models. The predicate is therefore
already true for every field the analyzer sees, and keeping it only preserves a
name-based special case that nothing can trigger.

Field accessors now unroll unconditionally, like element accessors.
The default get model was merged into every non-static get* call
unconditionally, on top of whatever the passthrough config had already
produced, guarded by a commented-out `passThroughFacts.isNone &&` and a
`todo: fix owasp`.

That todo is stale. It dates from when the model copied the whole object
(`CopyAllMarks(from = This, to = Result)`); the field-based rewrite reads
the `<get-default>` carrier slot instead, and the guard no longer costs
any traces.

Verified: OWASP trace stats are byte-identical with and without the guard,
on the same portable project model and the same ruleset --
upstream OWASP-Benchmark/BenchmarkJava (the CI gate) total=4112,
simple=493, generatedSuccess=3619 both ways; the explyt fork total=4338,
simple=503, generatedSuccess=3835 both ways.

The precondition site in JIRMethodCallPrecondition still adds the default
rules unconditionally: it works on rules rather than evaluated facts, so
it has no isNone to test, and staying wider there can only over-admit
candidate traces, never drop valid ones.
JIRTaintCleanActionEvaluator resolved the type of every cleaned position and, when it
was java.lang.String, appended a hardcoded FieldAccessor(String, "<string-bytes>",
"byte[]") and cleaned that too. It existed because the models kept a string's content in
a sub-slot: a depth-one sanitizer clean cleared the string but not `str.bytes`, so the
next getBytes() read the taint straight back out. The constant carried a
`todo: fix in config?` saying as much.

The config side is fixed on 4-config (`refactor(model): stop hanging String content
slots off String positions`) - a String content slot no longer hangs off a String-typed
position, so this append has nothing left to clean and the special case can go. With it
go the PositionTypeResolver this evaluator only needed for the type test, and the
ActionPosition#append helper that existed for nothing else.

Same family as dropping the <rule-storage> unroll exception earlier on this branch:
an engine special case that only existed to prop up a slot shape in the model.

Verified after the split: rule-tests 687 pass / 0 FN / 0 FP / 0 skipped, querylang Java
243 and Go 792 with no failures, OWASP 2859 traces with TP 1286 - and 4-config on its
own, with this special case still in place but nothing for it to clean, is green too.
A sanitizer's `focus-metavariable` names the value that gets sanitized;
every other
metavariable in the pattern is only there to constrain the match.
Sources and sinks
already honour it (`ensureSourceStateVars` / `ensureSinkStateVars`), but
cleaners never
did -- `TaintRuleProcessing` carried a `// todo: sanitizer focus
metavar` and threw the
focus away, leaving `TaintCleanCompositionStrategy` to guess.

Its guess was wrong. `buildStateCleanAction` invokes `stateClean` once
per metavariable
the edge accesses, so `pos` is whichever metavariable that invocation is
for -- not the
focused one. For

    $*URI = (HttpServletRequest $REQ).getRequestURI();
focus-metavariable: $URI

it fires with `pos=Result` (for `$URI`) and again with `pos=This` (for
`$REQ`), and
`cleanerPositions`' `+ listOfNotNull(pos)` emitted a clean action for
both --
`[Result, Result, This, Result]`. Reading `request.getRequestURI()`
therefore untainted
`request` itself, and every later `request.getParameter(..)` on that
flow silently lost
its mark (jeesite5 unvalidated-redirect).

Thread `focusMetaVars` through `ProcessedTaintCleanRule` into the
strategy and emit `pos`
only on the focused metavariable's invocation. Scoped deliberately: a
sanitizer that
declares no focus metavariable has no way to say which value it
sanitizes, so it keeps the
old wide behaviour and cannot silently lose clean actions.

The same bug was live in five other sanitizer blocks: `$CLEAN =
$STR.replaceAll(..)` in
http-response-splitting-sinks.yaml was untainting `$STR`, and four
`Encode.forHtml(.., $*UNTRUSTED, ..)` blocks were untainting `$POLICY` /
`$AS` / `$H`.
Narrowing a sanitizer can only add findings, never lose them.
When a sink condition needs a mark that may be hidden under a
parameter's abstraction, the
callee posts a `TaintMarkFieldUnfoldRequest`.
`MethodSideEffectHandlerWithAnyAccessorRequestHandling` only overrode
`handleZeroToFact`,
so the request was dropped as soon as the caller was itself analyzed
from an initial fact
-- that is, for every value more than one frame from its source. Any
sink reading a
*field* of a formal parameter was lost that way (kkFileView `new
File(String)`,
Stirling-PDF `File#toPath()`).

Two things are needed beyond the plain override:

1. The caller is usually abstract too, so the requested mark is not on
that edge --
   measured at depth 1: `final=var(0).path/*`, `delta=[File#path]`, mark
nowhere. Refining
   only when the delta carries the mark makes the handling inert. So
when it does not,
   refine on the *shape* the delta does carry, restricted to a single
`FieldAccessor` --
   the shape a field-sensitive library model produces (`file.path`,
`bean.url`). Fanning
   out over several accessors, or over elements, re-analyzes far too
much.

2. Cost. Answer only while the request is still un-refined
   (`kind.fact.getAllAccessors().isEmpty()`); fact-to-fact edges vastly
outnumber
   zero-to-fact ones. On tms (stock 70 s / 154 results), all variants
keeping 154 results:
   no guards 900 s timeout -> un-refined guard 403 s -> + single-field
103 s.

Rejected alternative, for the record: re-addressing the request to the
current frame so it
climbs -- either by retargeting the propagated kind, or by requesting a
split of the
current frame's own initial fact via the side effect requirement channel
(which needs no
`handleSummary` change, since that channel is independent of summaries).
Both fully
recover the shapes, and both time out on tms at 900 s, with and without
a hop cap and with
the single-field guard. The cost is breadth: splitting an initial fact
in every frame the
request passes through pushes a requirement to every caller
transitively. The
`emptySet()` that `handleSummary` returns on `SummaryApRefinement` is
correct and stays --
a summary carrying an unanswerable request must stop where the caller's
fact is more
concrete than the summary being applied.
The mechanism gave element taint to an array position without a rule. The
starred rules give the same taint, and they give it where the rule author can
see it. Thus the mechanism is not necessary.

Deletes both halves:
  - the sink bridge: patchSinkConditionFactReader (JVM and Go),
    arrayElementConditionReaders, callArgumentMayBeArray;
  - the source duplication: resolveWithArray, resolveArrayActionPosition and
    resolveArrayPosition.

This needs the any-accessor fix at the base of the stack. Without that fix a
star loses its taint at a primitive element read, and bad-hexa-conversion
finds nothing.
The array-element mechanism is deleted. A base-only source thus stops at an
element read of a primitive array. Only the star continues.

Flips the base-only case to assertNotReachable and states the new contract.
…ization overloads

Commit 54749bcdd dropped <serialized-value> reads from all non-String
readValue/readValues overloads, reasoning they cannot type-check against
byte[]/Reader/InputStream. Restores all nine removed entries; the
deserialization slot must not be deleted.
…ization overloads

Commit 54749bcdd dropped <serialized-value> reads from all non-String
readValue/readValues overloads, reasoning they cannot type-check against
byte[]/Reader/InputStream. Restores all nine removed entries; the
deserialization slot must not be deleted.
@Saloed
Saloed force-pushed the saloed/42-proof-guided-any-compression branch from 9888e94 to a715731 Compare September 1, 2026 18:11
@Saloed
Saloed force-pushed the saloed/5-default-get branch 11 times, most recently from 87fc96d to 7f34b11 Compare September 17, 2026 07:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants