From e514551cb6175d6f0f74b94cc0bfd9916ba4535b Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Wed, 14 Oct 2026 15:54:29 +0200 Subject: [PATCH] spec(access-control-prover): the checker gains an opt-in premise and the unguarded_path label Codex stopped on a real conflict: with path records and no clause or sibling norm the checker returns no finding by design. The prover's premise (a recognised entry is protected unless declared public) is now an opt-in keyword with its own label and evidence, default off, existing behaviour and tests unchanged. Co-Authored-By: Claude Fable 5.1 --- .kiro/specs/access-control-prover/design.md | 14 +++++++++++++- .kiro/specs/access-control-prover/requirements.md | 5 +++++ .kiro/specs/access-control-prover/research.md | 12 ++++++++++++ .kiro/specs/access-control-prover/tasks.md | 9 +++++++++ 4 files changed, 39 insertions(+), 1 deletion(-) diff --git a/.kiro/specs/access-control-prover/design.md b/.kiro/specs/access-control-prover/design.md index 36afee1..4e34ee1 100644 --- a/.kiro/specs/access-control-prover/design.md +++ b/.kiro/specs/access-control-prover/design.md @@ -30,7 +30,10 @@ runner that scores it with the valid-benchmark metrics. - Operation and discharger rows added to `ruleset/obligations/{java,php,python,typescript}.toml`. ### Out of Boundary -- The facts loader and schema, the checker's decision rules, `OrderDominance` (owned by `authorization-obligations`). +- The facts loader and schema, `OrderDominance`, and the checker's existing decision rules (owned by + `authorization-obligations`). One opt-in extension of the checker is allowed and owned here: the + `assume_entries_protected` keyword and the `unguarded_path` label (see the checker block below); default off, + every existing checker test unchanged. - The feature table, the DSPy and hunter arms, the ablation (`hunter-learning-loop`). - The proof arm's demonstration logic (`search-with-proof`); this spec only shapes the finding. @@ -173,6 +176,15 @@ def compose_paths( cached index and the enclosing function of each site (`source.enclosing_at` or the IR spans). - Postconditions: every path's last hop is a target; no path implies nothing; unreached targets are listed. +### checker extension (opt-in) +`check_obligations(..., assume_entries_protected: bool = False)`. With path records, no declared clause and no +sibling norm, the checker today returns no finding (gating 3 of `authorization-obligations`): nothing justified +the obligation. The prover's premise justifies it: a recognised entry is protected unless declared public. With +the keyword on, `_finding` labels such a case `unguarded_path` when the path's entry hop is an entry record whose +access is not `public` and the route is not declared public; evidence carries the entry's kind and evidence +strings and the sentence "no declared policy clause and no sibling norm; the prover assumes a recognised entry is +protected". `findings_to_static` explains the label like the others. `LABELS` gains the value. + ### 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 c7c052e..277389d 100644 --- a/.kiro/specs/access-control-prover/requirements.md +++ b/.kiro/specs/access-control-prover/requirements.md @@ -113,6 +113,11 @@ protected operation, so that every alarm names what to add and where. dominates it along that path or inside its function, the prover shall emit one finding per operation and missing kind with family `access_control`, the operation's path and line, the entry point, the hops, the missing kind and the evidence strings. +1a. The prover's premise shall be explicit: a recognised entry point is protected unless the framework or a + declared policy marks it public. The checker shall apply that premise only when the caller opts in, shall + label such findings `unguarded_path` (distinct from `declared_policy_violation` and + `consistency_violation`), and shall say in the evidence that no policy clause and no sibling norm backed it. + The checker's default behaviour with path records (no clause, no sibling norm, no finding) is unchanged. 2. When every required discharger kind is dominated, the prover shall emit no finding and shall count the operation as `discharged` in the coverage statement. 3. The prover shall never emit a finding for a function whose file failed to parse, whose language has no diff --git a/.kiro/specs/access-control-prover/research.md b/.kiro/specs/access-control-prover/research.md index 989ba2b..1cb723b 100644 --- a/.kiro/specs/access-control-prover/research.md +++ b/.kiro/specs/access-control-prover/research.md @@ -100,6 +100,18 @@ guarded route. Every recogniser lists its names in the facts header and the coverage statement counts routes with unrecognised middleware. +### Decision: an opt-in premise in the checker, not a synthesized policy +- **Context**: Codex's first attempt stopped on a real conflict: with path records and neither a declared clause + nor a sibling norm the checker returns no finding by design (gating 3), so the prover's core verdict could not + be emitted without a change. +- **Alternatives Considered**: synthesize a `DeclaredPolicy` in memory marking every recognised entry + `authenticated` (dishonest: the finding would read "route declared authenticated" when nothing was declared); + a second checker in the prover (duplicates the rules); an opt-in keyword and a distinct label (chosen). +- **Selected Approach**: `assume_entries_protected=False` keyword, label `unguarded_path`, evidence naming the + premise. Default behaviour and tests unchanged. +- **Trade-offs**: the label makes the premise visible in every finding and in the static tags; consumers that + grouped by label need the new value (revalidation trigger for `authorization-obligations`). + ### Decision: no model call inside the prover - **Context**: Requirement 4.4; the maintainer's direction after the engine pilot: the model's job is the trust boundary question the static side cannot answer, asked after a static result exists. diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index d3209d7..9cc445a 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -9,6 +9,15 @@ - _Requirements: 3.1, 3.2, 3.3, 3.4, 3.5, 3.6_ - _Boundary: obligations.paths_ +- [ ] 1.2 Checker opt-in `assume_entries_protected` and label `unguarded_path` in `semantic/obligations/check.py` + - Default off; `_finding` receives the entry records' access by handler; evidence as the design states; + `findings_to_static` explains the label; `LABELS` updated + - Done when the existing checker tests pass unchanged and a new test shows: with paths, no policy, no siblings, + the default gives no finding and the opt-in gives one `unguarded_path` finding for a non-public entry and none + for an entry whose record access is `public` + - _Requirements: 4.1a_ + - _Boundary: obligations.check (opt-in only)_ + - [ ] 2. Entry recognisers - [ ] 2.1 Stapler and Jetty recognisers in `mapping.py` (P) - Public `do[A-Z]...` methods on exposed types or with Stapler-typed or `@QueryParameter` parameters; Jetty