From d81c55ed7eea735066b62dce55b5a433d36da65b Mon Sep 17 00:00:00 2001 From: Hugo Date: Fri, 25 Sep 2026 02:51:24 +0200 Subject: [PATCH 1/2] test: specify that a validator proves only the kinds it declares --- tests/test_project_validators.py | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/tests/test_project_validators.py b/tests/test_project_validators.py index 0052b6f..45acf98 100644 --- a/tests/test_project_validators.py +++ b/tests/test_project_validators.py @@ -32,12 +32,10 @@ ) -def verdict(*models: Model) -> Status: +def verdict(*models: Model, sink: TaintKind = TaintKind.COMMAND) -> Status: module = build_hir(SourceManager().add_source("views.py", VIEW)) registry = SecurityModelRegistry() - registry.register( - Source(SymbolId("python.builtins.input"), "stdin"), Sink(SymbolId("python.os.system"), TaintKind.COMMAND), *models - ) + registry.register(Source(SymbolId("python.builtins.input"), "stdin"), Sink(SymbolId("python.os.system"), sink), *models) manager = engine.build_manager(module, registry) run = next(s for s in module.body if isinstance(s, nodes.Function) and s.name == "run") (found,) = manager.get(RefutationAnalysis, run).all() @@ -48,6 +46,18 @@ def test_a_declared_project_validator_refutes_the_flow_it_guards() -> None: assert verdict(Validator(SymbolId("python.views.allowed"))) is Status.REFUTED +def test_a_validator_proves_only_the_kinds_it_declares() -> None: + # A redirect validator says nothing of what a shell makes of the value. + allowed = SymbolId("python.views.allowed") + + assert verdict(Validator(allowed, TaintKind.REDIRECT)) is Status.HOTSPOT + assert verdict(Validator(allowed, TaintKind.COMMAND)) is Status.REFUTED + assert verdict(Validator(allowed, TaintKind.COMMAND), sink=TaintKind.COMMAND | TaintKind.SQL) is Status.HOTSPOT + assert verdict(Validator(allowed, TaintKind.COMMAND | TaintKind.SQL), sink=TaintKind.COMMAND | TaintKind.SQL) is ( + Status.REFUTED + ) + + def test_an_undeclared_project_function_leaves_a_hotspot() -> None: assert verdict() is Status.HOTSPOT assert verdict(Validator(SymbolId("python.other.allowed"))) is Status.HOTSPOT From eb50f10924eb3dd774312da6cfd59cbbd0af49ce Mon Sep 17 00:00:00 2001 From: Hugo Date: Fri, 25 Sep 2026 02:51:24 +0200 Subject: [PATCH 2/2] fix: let a validator prove only the kinds it declares --- CHANGELOG.md | 1 + docs/plugins.md | 2 +- src/coretrace_python/findings/refutation.py | 32 ++++++++++++--------- 3 files changed, 21 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cf3af74..181a89a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,7 @@ ### Precision +- A `Validator` proves its argument safe only for the kinds it declares. A validator declared for `REDIRECT` used to refute a command injection through the same value; the flow is now a hotspot, and it is refuted only when the validator covers every kind reaching the sink (#143). - A sanitizer called inside a project function protects the flows through that function, for every caller. That covers a helper that escapes before answering, a view redirecting to `reverse(...)`, and a helper rendering a template the analyzer shows escaping. Function summaries keep, for each parameter, the taint kinds cleared on every path from it to an external call or to the return value. A path that skips the sanitizer, or a kind it does not clear, still reaches the sink. The cache format is bumped (#134). ### Plugins diff --git a/docs/plugins.md b/docs/plugins.md index ec22e4f..eac5fa4 100644 --- a/docs/plugins.md +++ b/docs/plugins.md @@ -150,7 +150,7 @@ class BottleModels(ModelPlugin): | `SuffixSink(suffix, kinds, positions=())` | A sink matched by the end of the symbol, for methods of any class such as `objects.raw`. | | `SafeArgument(symbol, argument, values, position=None, kinds=ALL)` | A call to the sink `symbol` whose `argument` (by keyword, or at `position`) denotes one of `values` is not a sink for `kinds`, such as `yaml.load` with `Loader=yaml.SafeLoader`. Values are written as the analyzer records arguments: a symbol by its canonical name, a constant as Python writes it (`True`). Only a value given explicitly makes the call safe. | | `TemplateRender(symbol, position=0, keyword="template_name")` | A call rendering, with autoescaping, the template named by its argument at `position` or `keyword`, such as `render_to_string`. What it returns carries no `HTML` when the name is written in the call and the project's template escapes everything it prints (see the usage guide). | -| `Validator(symbol, kinds=ALL, argument=0)` | A callable whose truth proves its argument safe, such as `re.fullmatch`; a flow guarded by it is refuted. `symbol` may be a function of the project, by its project symbol (`python.hc.accounts.views._allow_redirect`), which then counts wherever it is called, in its own module too. | +| `Validator(symbol, kinds=ALL, argument=0)` | A callable whose truth proves its argument safe for `kinds`, such as `re.fullmatch`. A flow guarded by it is refuted when it carries no other kind into the sink, and is a hotspot otherwise: a redirect validator does not make a shell command safe. `symbol` may be a function of the project, by its project symbol (`python.hc.accounts.views._allow_redirect`), which then counts wherever it is called, in its own module too. | | `AuthorizationGuard(symbol, label)` | A decorator or a condition restricting who reaches the code, such as `login_required`; a flow behind it is a hotspot. | Two plugins may describe the same symbol. An identical model is registered once; two diff --git a/src/coretrace_python/findings/refutation.py b/src/coretrace_python/findings/refutation.py index e50d205..d38d2e8 100644 --- a/src/coretrace_python/findings/refutation.py +++ b/src/coretrace_python/findings/refutation.py @@ -60,6 +60,7 @@ TaintAnalysis, TaintFacts, TaintFlow, + TaintKind, ) VALIDATORS = frozenset( @@ -219,15 +220,16 @@ def guards(self, sink: BlockId) -> list[_Guard]: def interpret( self, condition: Value, truth: bool | None - ) -> tuple[dict[Value, str], set[Value]]: - """Values the condition proves safe (with the reason), and values it mentions - without proving anything. ``truth`` is ``None`` when it is not fixed at the sink. + ) -> tuple[dict[Value, tuple[str, TaintKind]], set[Value]]: + """Values the condition proves safe (with the reason and the kinds it proves them + safe for), and values it mentions without proving anything. ``truth`` is ``None`` + when it is not fixed at the sink. A recognised check evaluated the wrong way (``isdigit()`` known false) yields nothing: it is neither a proof nor a reassuring guard.""" definition = self.defs.get(condition) - proven: dict[Value, str] = {} + proven: dict[Value, tuple[str, TaintKind]] = {} mentioned: set[Value] = set() if isinstance(definition, UnaryOp) and definition.operator == "not": return self.interpret(definition.operand, None if truth is None else not truth) @@ -241,27 +243,29 @@ def interpret( recognised = self.recognise(definition) if recognised is None: return proven, set(self.closure(condition)) | {condition} - tested, reason, when_true = recognised + tested, reason, when_true, kinds = recognised if truth is None: mentioned = set(self.closure(condition)) | {condition} elif truth == when_true: # The check proves ``tested``; whatever else it reads is merely mentioned. - proven[tested] = reason + proven[tested] = (reason, kinds) mentioned = set(self.closure(condition)) | {condition} return proven, mentioned - def recognise(self, definition: Instruction | None) -> tuple[Value, str, bool] | None: - """``(validated value, reason, truth that validates)`` for known check shapes.""" + def recognise(self, definition: Instruction | None) -> tuple[Value, str, bool, TaintKind] | None: + """``(validated value, reason, truth that validates, kinds it proves)`` for known + check shapes. A string check, a constant allowlist or an equality with a constant + proves every kind; a ``Validator`` only the kinds it declares.""" if isinstance(definition, Call) and not definition.arguments: callee = self.defs.get(definition.callee) if isinstance(callee, GetAttr) and callee.attribute in VALIDATORS: - return callee.object, f"guarded by {callee.attribute}()", True + return callee.object, f"guarded by {callee.attribute}()", True, TaintKind.ALL if isinstance(definition, Call): symbol = self.symbols.get(definition.callee) validator = self.models.validator(symbol) if symbol is not None else None if validator is not None and validator.argument < len(definition.arguments): - return definition.arguments[validator.argument], f"validated by {symbol}", True + return definition.arguments[validator.argument], f"validated by {symbol}", True, validator.kinds if isinstance(definition, Compare): left, right = definition.left, definition.right if definition.operator in ("in", "not_in") and self.is_constant_collection(right): @@ -269,11 +273,12 @@ def recognise(self, definition: Instruction | None) -> tuple[Value, str, bool] | left, "allowlisted by a membership check on constants", definition.operator == "in", + TaintKind.ALL, ) if definition.operator in ("eq", "not_eq"): for tested, other in ((left, right), (right, left)): if isinstance(self.defs.get(other), Constant): - return tested, "equals a constant", definition.operator == "eq" + return tested, "equals a constant", definition.operator == "eq", TaintKind.ALL return None def examined( @@ -392,8 +397,9 @@ def judge(self, flow: TaintFlow, reachable: bool) -> Verdict: ) for guard in self.guards(sink): found, mentioned = self.interpret(guard.condition, guard.truth) - for value, reason in found.items(): - if value in chain: + for value, (reason, kinds) in found.items(): + # A check proving some kinds only leaves the others reaching the sink. + if value in chain and not flow.kinds & ~kinds: proven.setdefault(value, reason) examined = self.examined(guard.condition, mentioned, flow.argument, chain) for origin in origins: