From 12d09faeed682916c9097d6b5d6e5ba8f61e75c0 Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Wed, 14 Oct 2026 17:56:50 +0200 Subject: [PATCH] spec(access-control-prover): the ordered trace with argument provenance is the prover's output for every examined pair The maintainer's correction: counts over a function, language or framework carry nothing about safety; the object a decision model may see is the path from an attacker-reachable entry to a protected operation, with the checks on it in control-flow order and the provenance of the operation's arguments. Requirement 9, the trace contract and tasks 4.2 and 4.3. Co-Authored-By: Claude Fable 5.1 --- .kiro/specs/access-control-prover/design.md | 24 +++++++++++++++++++ .../access-control-prover/requirements.md | 24 +++++++++++++++++++ .kiro/specs/access-control-prover/tasks.md | 12 ++++++++++ 3 files changed, 60 insertions(+) diff --git a/.kiro/specs/access-control-prover/design.md b/.kiro/specs/access-control-prover/design.md index 0356a20..fc58504 100644 --- a/.kiro/specs/access-control-prover/design.md +++ b/.kiro/specs/access-control-prover/design.md @@ -196,6 +196,30 @@ framework id; default None keeps today's behaviour). The smoke run of delivery A Jenkins fixes are form-validation and list-filling web methods whose body calls no listed operation; the method is the operation. Jenkins documents the rule (form validation methods must check a permission). +### trace: the ordered serialisation (owned here) +```python +@dataclass(frozen=True) +class Guard: kind: str; scope: str; line: int | None; provenance: str; fact_id: str +@dataclass(frozen=True) +class Hop: function: str; call_line: int | None; guards_before_call: tuple[Guard, ...]; forwarded: tuple[str, ...] +@dataclass(frozen=True) +class Trace: + entry_kind: str; boundary: str; access: str; parameters: tuple[str, ...] + hops: tuple[Hop, ...] # entry first; the last hop holds the operation + operation_kind: str; fact_id: str; operation_line: int + arguments: tuple[tuple[str, str], ...] # (argument text, provenance) in call order + guards_after: tuple[Guard, ...] + requires: tuple[str, ...]; dominating: tuple[str, ...]; missing: str | None + def text(self) -> str: ... # one component per line, in order + def record(self) -> dict: ... # canonical JSON +``` +Argument provenance: within each hop's function, follow the IR's binds backwards from the operation's argument +identifiers to the function's parameters or to a request-source fact (`request_input`), to an identity source +(`authenticated_context`), or to a literal (`constant`); a parameter that the previous hop's call site fills +from its own request-derived values keeps `request_input`; anything the walk cannot follow is `unknown`. No +inter-procedural dataflow beyond the call sites on the path. The trace never carries language, framework, +repository, size or count fields. + ### 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 aaad001..4b63b58 100644 --- a/.kiro/specs/access-control-prover/requirements.md +++ b/.kiro/specs/access-control-prover/requirements.md @@ -180,3 +180,27 @@ can be proved or dismissed without re-deriving it. 1. Each finding shall carry the entry point record (kind, path, line, evidence), the hop list, the operation (id, kind, calls matched, line) and the missing discharger kind. 2. The finding id shall be `obligation::::` as the checker already emits. + +### Requirement 9: The ordered trace is the prover's output for every examined pair +**Objective:** As the maintainer, I want every (entry, operation) pair the prover examined serialised as an ordered +trace with its verdict, so that a decision model sees the security-relevant structure and nothing else. + +#### Acceptance Criteria +1. For every path record and every protected operation at its end, the prover shall emit one trace: the entry + (kind, trust boundary, declared access, parameter names), each hop in order (function, the call line, the + guards that dominate the call in that function with their kind, scope, line and provenance, the entry + parameters and request-derived values forwarded through the call), the operation (kind, fact id, line, the + provenance of each argument: request_input, authenticated_context, constant, unknown), the guards after the + operation, and the verdict (required kinds, dominating kinds, missing kind or discharged). +2. The prover shall emit traces for discharged pairs and for unguarded pairs alike, and shall list unreached + targets with their reason, so that negatives carry the same structure as positives. +3. The argument provenance shall be traced within each hop's function through the IR's binds from the entry's + parameters and the request-source facts, forwarded through the call sites on the path; a value the trace + cannot follow shall be `unknown`, never `constant`. +4. The trace shall carry no language, framework name, repository name, file size, line count, or any count over + the function or the repository: only the ordered components above. +5. The prover-arm record shall carry the traces, and a trace shall serialise to one canonical text form (one + component per line, in order) and one canonical JSON form, both deterministic. +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. + diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index 62fb4ec..179ee03 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -68,6 +68,18 @@ - _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 + - 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 + - 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_ + - [ ] 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