From 52ecbb76abfbf59d43d5cd0bfafa1253c0bfec89 Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Wed, 14 Oct 2026 18:07:09 +0200 Subject: [PATCH] spec(access-control-prover): control flow decides dominance; the trace carries each guard's relation, effect and the operation's control context Requirement 10, the structural control-flow graph per function and CfgDominance behind the existing protocol, tasks 4.4 and 4.5. Textual order stays the checker's default; the prover selects control flow. Co-Authored-By: Claude Fable 5.1 --- .kiro/specs/access-control-prover/design.md | 14 ++++++++ .../access-control-prover/requirements.md | 24 ++++++++++++++ .kiro/specs/access-control-prover/tasks.md | 33 +++++++++++++++++-- 3 files changed, 69 insertions(+), 2 deletions(-) diff --git a/.kiro/specs/access-control-prover/design.md b/.kiro/specs/access-control-prover/design.md index fc58504..0b438a1 100644 --- a/.kiro/specs/access-control-prover/design.md +++ b/.kiro/specs/access-control-prover/design.md @@ -220,6 +220,20 @@ from its own request-derived values keeps `request_input`; anything the walk can inter-procedural dataflow beyond the call sites on the path. The trace never carries language, framework, repository, size or count fields. +### cfg and CfgDominance (owned here) +`src/openultrasast/semantic/cfg.py`: `FunctionCfg.from_cst(node, language)` builds basic blocks and edges from +the tree-sitter syntax tree of one function (blocks, if/else, switch arms, loops with back edges, try/catch/ +finally, return, throw, break, continue, exit) and computes dominators (`dominates(a_line, b_line)`) and the +control context of a line (`context(line) -> ControlContext(conditions, in_loop, in_try, catches, on_exception_path)`). +`src/openultrasast/semantic/obligations/cfg_dominance.py::CfgDominance` implements the `Dominance` protocol: +a statement witness dominates when its block dominates the operation's block and its failure effect is +`throws`, `returns` or `exits` (the guard's condition leads to an exit on the failing arm; a bare boolean +whose value no branch or exit consumes before the operation is `value_only`); router and decorator scopes +dominate as before; along a path record, a witness on an earlier hop dominates as before. Without a graph for +a function, `CfgDominance` falls back to `OrderDominance` and records `cfg_unavailable`. +The trace's `Guard` gains `relation` (`all_paths`, `some_paths`, `none`, `after`) and `effect` +(`throws`, `returns`, `exits`, `value_only`); the trace gains `operation_context: ControlContext`. + ### obligations.enforcement ```python def witnesses(*, root: Path, texts: Mapping[str, str], entries: Sequence[EntryPointRecord], language: str) -> list[Discharge] diff --git a/.kiro/specs/access-control-prover/requirements.md b/.kiro/specs/access-control-prover/requirements.md index 4b63b58..551ebc1 100644 --- a/.kiro/specs/access-control-prover/requirements.md +++ b/.kiro/specs/access-control-prover/requirements.md @@ -204,3 +204,27 @@ trace with its verdict, so that a decision model sees the security-relevant stru 6. The hunt defect of an unguarded pair shall reference its trace, so the proof arm and the pre-push admission can show the path. +### Requirement 10: Control flow decides dominance, and the trace says so +**Objective:** As the maintainer, I want a guard to count only when control flow makes the operation unreachable +without it, so that a check in a branch the attacker can avoid, or one whose result is ignored, is not a discharge. + +#### Acceptance Criteria +1. The prover shall build a structural control-flow graph per function on a path from the syntax tree it already + parses: statement blocks, if and else branches, switch arms, loops, try, catch and finally, return, throw, + break and continue, and the function's exit; with no grammar for a construct the function shall be marked + `cfg_unavailable` and judged by order with that degradation recorded. +2. A guard shall dominate an operation when every path from the function's entry to the operation passes the + guard's statement (dominators over the graph); the trace shall record each guard's relation to the operation + as `all_paths`, `some_paths`, `none` or `after`. +3. The trace shall record each guard's failure effect: `throws`, `returns`, `exits` (break, continue, exit call), + or `value_only` when the guard's result is not consumed by a branch or an exit before the operation; a + `value_only` guard shall not discharge. +4. The trace shall record the operation's control context: the branch conditions it sits under in order (the + guard's own condition when it is one), whether it is inside a loop, inside a try whose catch swallows the + guard's exception type, or on an exception path. +5. Router and decorator witnesses shall keep their scope semantics (they dominate the handler as a whole). +6. The parameter list of a Java entry shall carry parameter names only, never annotation names; the arguments + of a handler-named operation shall be the handler's own parameters with their provenance. +7. The existing order-based dominance shall remain the default of the checker; the prover shall select the + control-flow dominance, and the checker's tests shall stay unchanged. + diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index 179ee03..5693152 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -68,18 +68,34 @@ - _Requirements: 4.1, 4.2, 4.3, 4.4, 4.5, 4.6, 6.2, 7.1, 8.1, 8.2_ - _Depends: 1.1, 2.1, 3.1, 3.2_ -- [ ] 4.2 `semantic/obligations/trace.py`: `Guard`, `Hop`, `Trace`, `text()` and `record()`; argument provenance through the IR's binds within each hop, forwarded along the path +- [x] 4.2 `semantic/obligations/trace.py`: `Guard`, `Hop`, `Trace`, `text()` and `record()`; argument provenance through the IR's binds within each hop, forwarded along the path - Done when `tests/test_obligation_trace.py` serialises a three-hop fixture deterministically (text and JSON), traces an argument from an entry parameter to `request_input`, from a literal to `constant`, from an identity source to `authenticated_context`, and marks an unfollowable value `unknown` - _Requirements: 9.1, 9.3, 9.4, 9.5_ - _Boundary: obligations.trace_ -- [ ] 4.3 The prover emits a trace per examined pair (discharged and unguarded), the record and the defect carry them +- [x] 4.3 The prover emits a trace per examined pair (discharged and unguarded), the record and the defect carry them - Done when `tests/test_hunt_prover.py` shows a discharged pair and an unguarded pair each produce one trace with the verdict, the unguarded finding references its trace, and `prover_arm` records carry `traces` - _Requirements: 9.1, 9.2, 9.5, 9.6_ - _Depends: 4.2_ +- [ ] 4.4 `semantic/cfg.py`: structural control-flow graph per function from the syntax tree, dominators, control context (P) + - Java, PHP, Python, JavaScript and TypeScript constructs of requirement 10.1; `cfg_unavailable` otherwise + - Done when `tests/test_semantic_cfg.py` shows, per language, that a guard before an unconditional return + dominates, a guard inside an if-branch does not dominate a statement after the branch, a guard inside a + loop body does not dominate a statement after the loop, a try/catch is represented, and context reports + conditions and loops + - _Requirements: 10.1, 10.2, 10.4_ + - _Boundary: semantic.cfg_ +- [ ] 4.5 `obligations/cfg_dominance.py::CfgDominance`, failure effects, and the trace's control components; the prover selects it; Java parameter names and handler-operation arguments cleaned + - Done when `tests/test_obligation_cfg_dominance.py` shows a value-only predicate does not discharge while the + same predicate guarding a throw does; a branch-only guard yields `some_paths` and no discharge; the prover + smoke on the 23 fixes keeps or raises its recall; `tests/test_mapping_frameworks.py` shows Java parameter + names without annotations + - _Requirements: 10.2, 10.3, 10.4, 10.5, 10.6, 10.7_ + - _Depends: 4.4_ + - [ ] 5. The arm - [x] 5.1 `benchmarks/valid/prover_arm.py`: run over a pool slice with checkpoints, summarise with the valid metrics - Record envelope copied from `hunter_arm`; instrument fields; resume; `summary.json` with recall (pushes and @@ -152,3 +168,16 @@ All 23 executions completed, zero errors; 16 changes checked operations and seven remained unchecked. It materialised only changed source files in temporary directories, so it is not a full-repository recall measurement. The maintainer-owned task 6.1 and release readiness remain unclaimed. + +- Delivery C (2026-10-14) implements tasks 4.2 and 4.3: ordered traces for every examined + path/operation pair, argument origins through local bindings and forwarded parameters, traces in + prover results and arm records, and trace references on unguarded findings. Existing checker + decisions and coverage accounting are unchanged. Declared route access is retained in the trace. +- Delivery C review used the main context because the brief prohibits model calls. Verdict: APPROVED + for tasks 4.2 and 4.3. Regression cases cover unresolved collections, overwritten bindings, + source-name boundaries, missing IR arguments, method parameter forwarding and return-order guards. +- Fresh delivery C verification with UV_NO_SYNC=1 and UV_CACHE_DIR=/tmp/ousast-uv: the exact + requested static gate passed (format, Ruff, mypy over 179 source files); the exact pytest gate + passed with 102 passed, zero failed, exit 0. The initial trace test failed collection because + trace.py did not yet exist; additional regression tests failed before their fixes. No + test_search_* test, network request or model call was made. Changes remain uncommitted.