diff --git a/.kiro/specs/access-control-prover/design.md b/.kiro/specs/access-control-prover/design.md index 58ea937..1e557bf 100644 --- a/.kiro/specs/access-control-prover/design.md +++ b/.kiro/specs/access-control-prover/design.md @@ -1,474 +1,418 @@ # Design Document ## Overview -**Purpose**: a deterministic prover for the access-control family: given a change checked out at head, find -every protected operation reachable from an entry point without a check dominating the path, and say what is -unchecked. **Users**: the maintainer, scoring it as an arm on the training pool; the pre-push hook and the proof -arm, consuming its findings. **Impact**: adds Java and framework entry recognition to the mapper, receiver- and signature-precise call -resolution in the obligations package `[2026-10-29]`, a path builder and enforcement witnesses in the -obligations package, a prover over the hunter's per-change context, and a runner that scores it with the -valid-benchmark metrics. +The access-control prover remains a deterministic rule arm over the existing obligation checker. The amendment +changes the semantic contract: resolution, resource matching, authority matching and dominance return abstract +relations rather than booleans, and every examined path receives one of three judgments: `unguarded`, +`discharged`, or `indeterminate`. A degraded instrument may reduce precision to `indeterminate`; it cannot +manufacture either final verdict. + +Target knowledge remains outside the engine. Entry shapes live in registered recognition strategies, while +operations, dischargers, resource rules and authority implications live in promoted fact data. A label-blind +initialization job produces that knowledge, and evaluation freezes its digest before admission labels are opened. ### Goals -- A finding names an entry point, the hops, the operation and the missing check; nothing else is a finding. -- Scored on the pool: recall on 23 fixes and 93 locations, false alarms per 100 ordinary pushes, seconds per change. -- Resolution precision `[2026-10-29]`: a guard discharges only the operation whose resource it binds, and a - call resolves to the class and signature it targets; an operation declared on a base class attaches only to - the classes that extend it. -- Coverage stated per repository: what was recognised, reached, checked, and left unchecked by reason. +- Produce an unguarded finding only from a complete, sufficiently resolved evidence path. +- Make call, path, resource, authority and control-flow uncertainty explicit and monotone. +- Carry target knowledge as verified data or recogniser strategies, never engine branches. +- Attribute development gains across analyzer and fact changes before measuring an untouched admission population. +- Fail the runtime and instrument gates rather than summarize partial work as a result. ### Non-Goals -- Taint flow, the Joern engine, nesting-aware dominance, families other than access control. -- Model calls inside the prover; intent adjudication stays a separate arm. -- The unseen pilot measurement and the pre-push wiring (later increments of other specs). +- Taint analysis, Joern integration, model calls inside the prover, or vulnerability families beyond access control. +- Client-side presentation gating, proof execution, pre-push wiring, or admission-policy thresholds. +- Replacing the existing order-based checker mode for consumers that do not opt into prover semantics. ## Boundary Commitments ### This Spec Owns -- Entry recognisers for Stapler, Jetty handlers, Symfony attributes, Livewire and Laravel controllers, Remix - exports, Tornado handlers, and programmatic servlet/handler registration sites `[2026-10-29]` - (`mapping.py` blocks, each with evidence). -- `semantic/obligations/resolution.py`: the class table and receiver- and signature-qualified call - resolution `[2026-10-29]`. -- The optional `receiver` field of `semantic/ir.py`'s `CallSite` and its capture in `semantic/cst.py` - (additive, default `None`; every existing consumer unchanged) `[2026-10-29]`. -- `semantic/obligations/paths.py`: `PathRecord` and `compose_paths` over the caller index. -- `semantic/obligations/enforcement.py`: router, decorator, voter `[2026-10-29]` witnesses from route files - and attributes, each carrying the resource it binds `[2026-10-29]`. -- `hunt/prover.py`: `prove_change` and `Coverage`. -- `benchmarks/valid/prover_arm.py`: the runner and its summary. -- Operation and discharger rows added to `ruleset/obligations/{java,php,python,typescript}.toml`. +- The abstract evidence domain and three-way pair/path judgment. +- Stable program identities, conservative call-target sets and bounded interprocedural summaries. +- Resource- and authority-sensitive operation/witness matching. +- Prover-mode control-flow dominance without textual-order fallback. +- Acquired entry, operation, discharger and authority knowledge needed by this family. +- Deterministic traces, failure-visible coverage, development arms and the admission-run contract. ### Out of Boundary -- The facts loader's existing fields, `OrderDominance`, and the checker's existing decision rules (owned by - `authorization-obligations`). Three extensions are allowed and owned here: the handler-named operation fields - (`handlers`, `framework`) in the facts; the `assume_entries_protected` keyword and the `unguarded_path` label - (see the checker block below); and, `[2026-10-29]`, the optional `resource` field on `Discharge` with the - `resource_bound` keyword and the all-kind caller-hop re-judgement in `_on_caller_hop` (see the checker block - below). Each is additive or 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. +- The legacy checker behavior used by existing callers; default APIs remain backward compatible. +- Target labels and benchmark curation, owned by `valid-detection-benchmark`. +- Runtime demonstrations, owned by `search-with-proof`. +- Hook admission and rollout, owned by `pre-push-safety-net`. +- Continuous fact evolution after the one-time initialization pass. ### Allowed Dependencies -- `openultrasast.source` (callers_of, code_index, product_files, generated_reason), `openultrasast.mapping`, - `openultrasast.semantic.cst` and `ir`, `openultrasast.semantic.obligations` (check, facts, dominance), - `openultrasast.hunt.producers.Context`, `benchmarks.valid.metrics`, `benchmarks.unseen.score`. +- `openultrasast.source`, `openultrasast.mapping`, the existing semantic IR and CFG, and the existing obligation + facts/checker contracts. +- The hunter `Context` caches, valid-benchmark metrics, replay record envelopes and reserved-population guard. - No new third-party dependency. ### Revalidation Triggers -- A change to `EntryPointRecord` fields or `Discharge` scopes. -- A change to `CallSite` fields or the caller-index keying `[2026-10-29]`. -- A change to the replay record shape `benchmarks.valid.metrics` scores. -- A change to the hunt defect shape (`defect_from`). +- A change to `EntryPointRecord`, `Operation`, `Discharge`, `Trace`, hunt-defect or replay-record contracts. +- A change to call-site receiver/signature capture, target-knowledge schemas or authority implication semantics. +- A change to path aggregation, judgment ordering, admission population isolation or the 120-second budget. ## Architecture ### Existing Architecture Analysis -The checker already judges reached operations by path and witnesses by scope; the hunter's `Context` already -caches everything the prover reads. The missing pieces are the inputs: entries for Java and the pool's PHP, -TypeScript and Python frameworks; paths; witnesses from outside the function; operation rows for the pool's -protected calls. The prover is wiring plus those inputs. +The delivered baseline already recognises entries, composes bounded paths, discovers operations and witnesses, +builds structural CFGs, emits traces and scores replay records. Its decision interfaces are boolean: unresolved +receivers fall back to a bare name, unavailable CFGs fall back to textual order, and a witness either discharges or +does not. The amendment preserves the existing checker as the single verdict owner while inserting typed abstract +values before that boolean boundary and adding an opt-in three-way judgment path. ### Architecture Pattern & Boundary Map -```mermaid +~~~mermaid flowchart LR - C[hunt.producers.Context\nproduct files, texts, IR, call index, entry points] --> P[hunt.prover.prove_change] - M[mapping.analyze_entry_points\n+ Stapler, Jetty, Symfony, Livewire, Remix, Tornado\n+ programmatic registration] --> C - C --> RES[obligations.resolution\nclass table, receiver-qualified calls] - RES --> P - P --> PA[obligations.paths.compose_paths] - P --> EN[obligations.enforcement.witnesses\nrouter, decorator, voter, resource-bound] - PA --> CK[obligations.check.check_obligations] - EN --> CK - RES --> CK - F[ruleset/obligations/*.toml\noperations, dischargers] --> CK - CK --> P - P --> R[benchmarks/valid/prover_arm.py\nrecords, metrics, coverage, anchor refusal] - P --> H[pre-push admission / proof arm\nhunt defects] -``` -- Selected pattern: inputs assembled in the prover, decision in the existing checker. -- Existing patterns preserved: closed facts in TOML with checked headers; `_entry` recogniser blocks; per-change - `Context`; replay record shape; counts and digests in records. -- Steering compliance: no model call, instrument gate (bytes read), plain English, standard metrics. + TK[Target knowledge] --> MR[Mapping registry] + TK --> FI[Fact interpreter] + MR --> CTX[Per change context] + FI --> OP[Operations and witnesses] + CTX --> SI[Symbol index] + SI --> CR[Call resolution] + CR --> FS[Function summaries] + OP --> FS + FS --> PM[Concrete path materializer] + CTX --> CFG[Control flow relations] + PM --> J[Three way judgment] + CFG --> J + OP --> J + J --> TR[Canonical traces] + J --> PR[Prover findings and coverage] + TR --> RUN[Development and admission runners] + PR --> RUN +~~~ + +Dependency direction is: +`abstract domain -> fact and recogniser adapters -> symbol resolution -> summaries and CFG -> checker judgment +-> prover integration -> runners`. Engine modules never import target-named strategy modules. Target-aware +adapters may import engine contracts. + +- **Strategy + Registry**: entry recognisers are registered per recognition concern. +- **Interpreter**: promoted fact rows describe operations, dischargers, resource rules and authority implications. +- **Adapter**: the prover converts repository IR, target knowledge and context caches into engine contracts. +- **Abstract interpretation**: finite domains and monotone joins propagate evidence and incompleteness. ### Technology Stack -| Layer | Choice | Role | Notes | -|---|---|---|---| -| Analysis | Python 3.11, tree-sitter IR, regex caller index | entries, paths, operations | existing | -| Facts | TOML under `ruleset/obligations/` | operations, dischargers | existing loader | -| Scoring | `benchmarks.valid.metrics`, `benchmarks.unseen.score` | recall, false alarms per 100 | existing | +| Layer | Choice | Role | +|---|---|---| +| Analysis | Python 3.11, existing semantic IR and structural CFG | symbols, calls, summaries, dominance | +| Knowledge | Existing TOML fact files and mapping strategies | target-specific vocabulary | +| Scoring | Existing valid-benchmark metrics and replay records | development and admission results | ## File Structure Plan -``` +~~~text src/openultrasast/ -├── mapping/ # recogniser registry [2026-10-29]: one strategy module per -│ │ # recognition concern, each registering itself in one table -│ ├── registry.py # the registry the language dispatch consults -│ ├── registration_sites.py # call-site handler registration strategy (data-driven vocabulary) -│ └── stapler.py, jetty.py, symfony.py, livewire.py, remix.py, tornado.py -│ # strategy modules migrating from mapping.py's legacy blocks -├── mapping.py # dispatch consults the registry during migration; blocks retire -│ # family by family (breadth map tracks the order) +├── mapping/ +│ ├── registry.py # strategy registration and dispatch +│ ├── registration_sites.py # generic call-site registration adapter +│ └── .py # one target-aware strategy per migrated concern ├── semantic/ -│ ├── cst.py # + capture call receiver text in _call [2026-10-29] -│ ├── ir.py # + CallSite.receiver: str | None [2026-10-29] +│ ├── ir.py # CallSite receiver and signature evidence +│ ├── cst.py # receiver, arity and signature capture │ └── obligations/ -│ ├── resolution.py # ClassRecord, class_table, qualify — receiver/signature resolution [2026-10-29] -│ ├── paths.py # PathRecord, compose_paths(callers, entries, targets, depth, fan_out) -│ └── enforcement.py # witnesses(root, texts, entries, facts) -> list[Discharge] -├── hunt/prover.py # prove_change(root, change, ctx) -> ProverResult(findings, coverage) -└── ruleset/obligations/{java,php,python,typescript}.toml # + operation and discharger rows, checked headers -src/openultrasast/tools/fact_init.py # the one-time initialization job: extract + propose -> verify -> promote [2026-10-29] -benchmarks/valid/prover_arm.py # run / summarize; records per change; coverage table; anchor refusal -tests/test_mapping_registry.py, tests/test_mapping_registration_sites.py, tests/test_obligation_resolution.py, -tests/test_obligation_paths.py, tests/test_obligation_enforcement.py, tests/test_hunt_prover.py, -tests/test_prover_arm.py, tests/test_fact_init.py -``` +│ ├── abstract_domain.py # relations, completeness, resources, authorities, judgments +│ ├── resolution.py # SymbolId, symbol index and CallTargetSet +│ ├── summaries.py # monotone FunctionSummary computation over call components +│ ├── paths.py # concrete evidence paths and cutoff records +│ ├── operations.py # operation/witness abstract identities +│ ├── dominance.py # legacy order mode, unchanged by default +│ ├── cfg_dominance.py # prover-mode control-flow relation, no order fallback +│ ├── check.py # opt-in abstract matching and PairJudgment +│ ├── enforcement.py # target-aware enforcement adapter +│ └── trace.py # canonical trace with abstract relations and completeness +├── hunt/ +│ ├── producers.py # cached symbol index and summaries +│ └── prover.py # integration, path aggregation, findings and coverage +└── tools/ + └── fact_init.py # label-blind extract/propose/verify/promote workflow +ruleset/obligations/*.toml # promoted operation, witness and authority knowledge +benchmarks/valid/ +├── prover_arm.py # records, stage funnel, gates and four-arm comparison +└── prover_admission.py # frozen-manifest admission orchestration +tests/ +├── test_obligation_abstract_domain.py +├── test_obligation_resolution.py +├── test_obligation_summaries.py +├── test_obligation_judgment.py +├── test_obligation_trace.py +├── test_mapping_registry.py +├── test_fact_init.py +├── test_hunt_prover.py +└── test_prover_arm.py +~~~ ### Modified Files -- `src/openultrasast/mapping.py`: dispatch consults the `mapping/` registry (Strategy pattern); legacy blocks - migrate into strategy modules family by family; `EntryPointRecord` unchanged. -- `src/openultrasast/hunt/producers.py`: `Context` exposes `entry_points` and `ir(path)` already; add nothing - unless a cache is missing (then a `cached_property`, same pattern). -- `src/openultrasast/ruleset/obligations/*.toml`: rows only, admitted through the fact gate. +- Existing facts, IR, checker, dominance, trace, prover and arm modules receive additive or opt-in contracts. +- Existing callers retain legacy defaults; only the prover selects three-way judgment and strict CFG semantics. +- Existing completed benchmark records remain immutable development baselines. ## System Flows -```mermaid -sequenceDiagram - participant R as prover_arm - participant X as Context - participant P as prove_change - participant PA as compose_paths - participant EN as enforcement - participant CK as check_obligations - R->>X: checkout head, Context(root, change) - R->>P: prove_change(root, change, ctx) - P->>X: entry_points, call_index, texts, ir(path) per touched file - P->>PA: targets = touched functions + callees holding operations - PA-->>P: PathRecords (hops entry..operation function), unreached list - P->>EN: route files, attributes, entries - EN-->>P: router/decorator Discharges - P->>CK: irs of touched + hop files, entries, facts, paths, OrderDominance(texts), extra_witnesses - CK-->>P: ObligationResult (findings, discharges, degradations) - P-->>R: ProverResult(findings as hunt defects with entry, hops, operation, missing; coverage) - R->>R: record per change; metrics.summarize; coverage table -``` -Gating: a file that fails to parse, a language without facts, or an unrecognised framework yields coverage -counts and no finding. A declared-public route suppresses `path_guard` only. + +### Analysis +~~~mermaid +flowchart TD + A[Read cached source] --> B[Recognise entries and facts] + B --> C[Build symbol index] + C --> D[Resolve call target sets] + D --> E[Compute function summaries] + E --> F[Materialise evidence paths] + F --> G[Match witnesses to obligations] + G --> H[Evaluate control flow] + H --> I{Path state} + I -->|complete and missing| U[Unguarded] + I -->|complete and governed| DCH[Discharged] + I -->|possible unknown or cut| IND[Indeterminate] + U --> FIND[Finding and trace] + DCH --> TRACE[Trace only] + IND --> TRACE +~~~ + +### Evaluation +~~~mermaid +flowchart LR + ACQ[Label blind acquisition] --> FREEZE[Freeze candidate bundle] + BASE[Materialize baseline bundle] --> DEV[Four arm development comparison] + FREEZE --> DEV + DEV --> AUDIT[Review ordinary labels] + AUDIT --> HOLD[Untouched paired admission run] + HOLD --> GATE{Instrument budget and quality gates} + GATE -->|pass| GO[G1 eligible] + GATE -->|fail| NOGO[No go] +~~~ ## Requirements Traceability | Requirement | Components | |---|---| -| 1.1-1.8 | mapping recognisers | -| 1.9 | mapping `_jetty_registration_entries` + `resolution.class_table` | -| 2.1-2.8 | enforcement.witnesses, facts rows, checker (existing) | -| 2.9 | facts rows (handler-named webhook and data-exposure patterns), `handlers_of` | -| 2.10 | enforcement resource tokens and voter witnesses; checker `resource_bound` | -| 3.1-3.6 | paths.compose_paths | -| 3.7 | hunt.prover target enumeration (down-call budget) | -| 3.8 | trace `guards_before_call` + checker `_on_caller_hop` all-kind re-judgement | -| 3.9 | resolution.qualify, class_table, `CallSite.receiver` | -| 3.10 | checker `_on_caller_hop` + prover witness assembly | -| 4.1-4.6 | hunt.prover.prove_change | -| 5.1-5.5 | prover_arm | -| 5.6 | prover_arm anchor refusal | -| 6.1-6.2 | prover_arm timing, Context caches | -| 7.1-7.2 | Coverage in prove_change, prover_arm summary | -| 7.3 | prove_change error reasons | -| 8.1-8.2 | finding shape in prove_change | -| 9.1-9.6 | trace serialisation in prove_change (obligations.trace) | -| 10.1-10.7 | cfg.FunctionCfg, CfgDominance | - -## Pattern Application and Fact Acquisition `[2026-10-29]` - -The implementation follows the steering pattern discipline (`code-standards.md`): the engine stays -target-agnostic; per-target vocabulary is data. Concretely for this spec: - -- **Strategy + Registry** for entry recognisers: the recognisers this spec adds (registration sites, and the - migration of existing framework blocks) live as strategy modules in a `mapping/` registry -- one module per - recognition concern, each naming its target family in the filename, registering itself in one table. The - dispatch in `mapping.py` consults the registry; it does not name frameworks. -- **Interpreter** for obligation facts: operation rows, discharger rows, handler-name families and - registration-site vocabulary are TOML data interpreted by the engine; adding a target's vocabulary is a data - change reviewable in one place. -- **Adapter** at the engine seams: `hunt/prover.py`'s callers adapter binds the IR to the caller index - (receiver-qualified through `resolution`); `obligations/enforcement.py` adapts framework constructs into - `Discharge` witnesses and is target-aware territory -- engine modules never import it. - -### Fact acquisition (the one-time initialization pass) - -Per-target vocabulary is produced by a one-time initialization job, not by hand-specced enumerations. The job -has two modes and one gate: - -1. **Extraction mode**: walks the repository's existing recogniser code and framework knowledge (the legacy - `mapping.py` blocks, the current TOML rows) and extracts the target vocabulary already embedded there into - the acquirable structures (row families, strategy registrations). -2. **Proposal mode**: an LLM pass (or the maintainer) proposes the vocabulary a new target needs -- entry - shapes, registration sites, handler-name families, policy-decision constructs -- against the target's - repository. -3. **The gate**: every extracted or proposed row passes the same header discipline the facts files already - enforce (source, version, region) and engine verification admits each row (the row must match what the - code says); only then is it promoted to a closed row. Nothing skips the gate. - -The initialization job is a pipeline tool in this spec's scope (it produces the data the engine consumes); -the standing fact-proposal lane (LLM proposes continuously, engine verifies, repetition promotes) remains the -roadmap's growth path and is out of boundary here. First runs: extraction over the current embedded -vocabulary, proposal for the training pool's target families, with the pool repositories as evidence. - +| 1.1, 1.2, 1.3, 1.4, 1.5, 1.6, 1.7 | mapping registry, registration adapter, fact initialization, coverage | +| 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 2.10 | fact interpreter, abstract domain, operations, enforcement, witness matcher | +| 3.1, 3.2, 3.3, 3.4, 3.5, 3.6, 3.7, 3.8, 3.9, 3.10 | symbol resolution, summaries, path materializer | +| 4.1, 4.2, 4.3, 4.4, 4.5, 4.6, 4.7 | pair judgment, checker integration, prover findings | +| 5.1, 5.2, 5.3, 5.4, 5.5, 5.6, 5.7 | prover arm, four-arm development comparison | +| 6.1, 6.2, 6.3 | context caches, deadline state, runner budget gate | +| 7.1, 7.2, 7.3, 7.4, 7.5, 7.6 | completeness, prover coverage, runner funnel | +| 8.1, 8.2, 8.3 | finding contract, trace references, proof-arm filter | +| 9.1, 9.2, 9.3, 9.4, 9.5, 9.6, 9.7 | canonical trace and record provenance | +| 10.1, 10.2, 10.3, 10.4, 10.5, 10.6, 10.7 | strict CFG dominance and legacy order compatibility | +| 11.1, 11.2, 11.3, 11.4, 11.5, 11.6, 11.7, 11.8 | abstract domain, path and operation aggregation, transition report | +| 12.1, 12.2, 12.3, 12.4, 12.5, 12.6, 12.7, 12.8, 12.9 | acquisition record, freeze manifest, admission runner | ## Components and Interfaces -### mapping recognisers -| Field | Detail | -|---|---| -| Intent | name web-exposed methods of the pool's frameworks as `route` entries with evidence | -| Requirements | 1.1-1.8 | +### Abstract evidence domain +~~~python +class EvidenceRelation(Enum): + MUST = "must" + MAY = "may" + NO = "no" + UNKNOWN = "unknown" -Each block follows the existing pattern: scan the file text (and the IR's function spans when a method body is -needed), call `_entry(target, start, end, handler, name, kind, access, trust_boundary, evidence, conditions)`. -Stapler: class text matches `extends|implements` one of the exposed types, or a method parameter is typed -`StaplerRequest`, `StaplerRequest2`, `StaplerResponse` or annotated `@QueryParameter`/`@AncestorInPath`; method is -`public` and its name matches `^do[A-Z]`. Access `public` only for `UnprotectedRootAction`. Jetty: classes -extending `AbstractHandler`, `HttpServlet` or annotated `@Path`/`@GET`/`@POST`. Symfony: methods with -`#[Route(` or `@Route(`; classes extending `AbstractController`. Livewire: classes extending `Component`, public -methods not starting with `_`, plus `Route::` registrations naming a controller method. Remix: `export const|function -action|loader` under `app/routes`. Tornado: classes extending `RequestHandler` or `WebSocketHandler`, request -methods and `open`. +class PairJudgment(Enum): + UNGUARDED = "unguarded" + DISCHARGED = "discharged" + INDETERMINATE = "indeterminate" -Registration sites `[2026-10-29]` (1.9): the call-site registration concept the Python route -registrations and the WordPress registration table already use, stated once, generically: when the -repository's own code registers a handler at a call site (a constructor or registration method whose argument -names the handler class), the registered class's request methods become `route` entries at the method's -declaration line in the registered class's file, with the registration site (`path:line`) and the registered -class name as evidence and `registered_by` set. The registration-site vocabulary -- which constructors and -methods count as registrations, and which methods of the registered class are request methods -- is acquirable -data under the facts discipline (R2 AC7), carried by a registration strategy module in the recogniser -registry, never hardcoded in the engine. Class-literal resolution goes through `resolution.class_table`. A -registration whose target class the repository does not define yields coverage (`registration_unresolved`) and -no entry. Jetty's programmatic servlet registration is the first data case (seatunnel evidence), not the -definition. - -### obligations.paths -```python @dataclass(frozen=True) -class PathRecord: - hops: tuple[tuple[str, int | None], ...] # ("path::function", line of the call site in the caller), entry first - entry: str # "path::function" of the entry hop - complete: bool # True when hops[0] is an entry point +class Completeness: + is_complete: bool + reasons: tuple[str, ...] = () -def compose_paths( - *, callers: Callable[[str, str], Sequence[tuple[str, int]]], # (path, function) -> caller sites - entries: set[str], targets: Sequence[tuple[str, str]], max_depth: int = 3, fan_out: int = 25, -) -> tuple[list[PathRecord], list[str]]: # complete paths, unreached "path::function" targets -``` -- Preconditions: targets name functions with IR; `callers` resolves a function to its call sites through the - 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. - -### obligations.resolution `[2026-10-29]` (3.7, 3.9; feeds 1.9, 2.10, 3.10) -```python @dataclass(frozen=True) -class ClassRecord: - path: str # file declaring the class +class ResourceRef: + kind: Literal["exact", "aliases", "request_global", "unknown"] + values: tuple[str, ...] = () + +@dataclass(frozen=True) +class AuthorityRef: + values: tuple[str, ...] + is_unknown: bool = False +~~~ + +The partial order places definite evidence below possible or unknown evidence. Join never converts `MAY` or +`UNKNOWN` into `MUST` or `NO`. The precision order is: + +~~~text +MUST <= MAY <= UNKNOWN +NO <= MAY <= UNKNOWN +~~~ + +`MUST` and `NO` are incomparable. The alternative-path join is fixed by this table: + +| join | MUST | NO | MAY | UNKNOWN | +|---|---|---|---|---| +| MUST | MUST | MAY | MAY | UNKNOWN | +| NO | MAY | NO | MAY | UNKNOWN | +| MAY | MAY | MAY | MAY | UNKNOWN | +| UNKNOWN | UNKNOWN | UNKNOWN | UNKNOWN | UNKNOWN | + +Three separate operations prevent one table from being used for the wrong quantifier: + +1. `join_alternatives` uses the table above when alternative call targets or control paths contribute evidence. +2. `conjoin_dimensions` combines kind, scope, resource, authority and dominance for one witness: any `NO` + produces `NO`; otherwise any `UNKNOWN` produces `UNKNOWN`; otherwise any `MAY` produces `MAY`; only + all-`MUST` produces `MUST`. +3. `aggregate_witnesses` asks whether any witness definitely governs one obligation: any `MUST` produces + `MUST`; otherwise `UNKNOWN` takes precedence over `MAY`, and `MAY` takes precedence over `NO`. + An empty witness set is `NO` only when discovery and facts are complete; otherwise it is `UNKNOWN`. + +For one complete path, all required obligations at `MUST` yield `discharged`; any `MAY` or `UNKNOWN` yields +`indeterminate`; otherwise any `NO` yields `unguarded` and every `NO` obligation is reported missing. +Thus a mixed `[MUST, NO]` obligation vector is unguarded for the `NO` obligation. Resource +alias sets join by finite union; an unbounded or unresolvable value joins to `unknown`. Authority implication is +read from promoted facts and contributes its fact identifier to the match evidence. + +### Symbol resolution +~~~python +@dataclass(frozen=True, order=True) +class SymbolId: + module: str + enclosing_type: str | None name: str - superclass: str | None - abstract: bool - methods: tuple[str, ...] - -def class_table(texts: Mapping[str, str], language: str) -> Mapping[str, ClassRecord] - # bare class name -> record; one table per change, cached on the Context - -def qualify(*, receiver: str | None, enclosing_class: str | None, name: str, - arity: int | None, table: Mapping[str, ClassRecord]) -> str - # the qualified key for a callee: "Class.name" when the receiver text names a class - # in the table (or `this`/`self`/bare call in a class's own file), "Class.name/arity" - # when the class declares same-name methods with distinct parameter lists and the - # call site's arity is known, and the bare "name" when the receiver is unresolvable - # (dynamic languages, framework objects the repository does not define). -``` -- Preconditions: `receiver` is the receiver expression text captured on `CallSite` (new field; `None` for - bare calls in dynamic languages); `class_table` covers the repository's own classes only. -- Postconditions: same-name methods on different classes yield different keys; overloads with known distinct - arity yield different keys; unresolvable receivers fall back to the bare name and are counted - `receiver_unresolved` in coverage, never silently merged. -- Base-class attachment rule: an operation or handler-named entry declared on a class attaches to a path only - when the entry's (or call site's) class is that class or an in-repo subclass of it; `abstract` classes and - framework bases never project onto unrelated routes. -- Consumers: the prover's `callers` adapter returns, for a target key `Class.name`, only caller files whose - IR binds the callee to a receiver of that class (or subclass); the target enumeration joins callees by - qualified key instead of trailing name. `compose_paths` and `check_obligations` consume `path::function` - strings unchanged -- qualification happens before them, so `PathRecord` keeps its shape. -- Budget: the class table is one pass over texts (already read); resolution adds no tree walks. The target - enumeration extends down through calls within its own budget (`down_depth`, default 2, sharing the fan-out - bound), so an operation one call deeper than the handler is reached without unbounded descent. - -### 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. - -Resource-bound discharge `[2026-10-29]` (2.10): `check_obligations(..., resource_bound: bool = False)`. With the -keyword on, a witness whose `resource` field is set suppresses only operations whose resource token equals it -(a token computed the way `Operation.resource` already is: receiver first segment, table name, or the row's -`resource_arg`); a witness with `resource` unset keeps today's behaviour. Default off; existing tests unchanged. - -Caller-hop re-judgement `[2026-10-29]` (3.8, 3.10): `_on_caller_hop` re-judges a witness on an earlier hop for -every discharger kind, not only `path_guard` and `ownership_check`: the witness is re-judged against the -operation moved to the hop's call line, by the selected dominance. A guard recorded on a hop before the call -(`guards_before_call`) participates in the same re-judgement, so a finding is never emitted when the pair's own -trace shows a dominating guard of a required kind. Router and decorator scopes keep their whole-handler -semantics. - -### facts extension: handler-named operations (owned here, schema change) -`[[operation]]` rows gain two optional fields: `handlers` (a list of regular expressions over the function name) -and `framework` (a recogniser id the mapper's evidence names: `stapler`, `tornado`, `remix`, `jetty`, -`symfony`, `laravel`). A row with `handlers` and no `calls` is a handler-named operation: `find_operations` -yields it at the function's declaration line for every function whose name matches and that the caller lists as -a recognised entry of that framework (new keyword `handlers_of: Mapping[str, str] | None`, function name to -framework id; default None keeps today's behaviour). The smoke run of delivery A showed why: 15 of the 17 -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). - -Handler-named rows for the webhook, build-trigger and data-exposure shapes `[2026-10-29]` (2.9): the -`handlers` patterns extend to verb families whose handler name itself carries the obligation -- endpoints -that act with repository or job privileges when called (webhook and build-trigger shapes) and endpoints that -expose protected data (data-exposure shapes) -- as operation rows on framework-recognised entries, at the -declaration line. The families are rows in the facts files, not code: a new verb family is a row addition -acquired through the one-time initialization pass for the target (or proposed by the fact-proposal lane), and -a row without `handlers` never matches a declaration name. The gate-1 misses (Stapler webhook and -chart-data endpoints) are the first evidence set, not the definition. - -### 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. - -### 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 the operation is unreachable -from the guard's failing arm: either that arm exits (`throws`, `returns`, `exits`), or the operation lies only -inside the passing branch (`if (can(x)) { op(); }`, effect `branches`); a bare boolean whose value no branch or -exit consumes before the operation is `value_only` and never discharges; 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`, `branches`, `value_only`; `constrains` for an identity constraint or a -non-permissive value on the operation's own line, which has no failing arm; router and decorator witnesses carry -`exits`); the trace gains `operation_context: ControlContext`. Coarse spots accepted for this increment: a -ternary or switch expression is one node, several statements on one line share it, a guard's result held in a -variable is followed by name without reassignment tracking. - -### obligations.enforcement -```python -def witnesses(*, root: Path, texts: Mapping[str, str], entries: Sequence[EntryPointRecord], language: str) -> list[Discharge] -``` -Reads Laravel route files (`routes/*.php`) for `->middleware([...])` and controller constructors for -`$this->middleware`/`authorizeResource`; Symfony attributes and `config/packages/security.yaml` -`access_control`; Tornado `@authenticated`; emits `Discharge(kind="path_guard", scope="router"|"decorator", path, -function, line=None, evidence=...)` for each covered handler. Names recognised live in the facts files' headers. - -Resource binding and policy witnesses `[2026-10-29]` (2.10): every witness this module mints carries the -resource it binds (`Discharge` gains an optional `resource: str | None`, default `None`): the route path for -router middleware, the attribute or subject expression for a policy-layer guard, the middleware name for -`auth`-class guards (no resource -- `None`). A policy-layer witness covers an action's operations when a -policy decision (voter, capability check, or equivalent) reachable from the action -- in the action body or a -function it calls -- names the action's attribute or subject; the witness is scoped to that action's -operations with the attribute or subject as its resource. Which constructs count as policy decisions is -acquirable data in the facts files (the discharger rows already carry the vocabulary); the witness shapes are -engine behaviour. Discharge matching is the checker's `resource_bound` keyword (above); the resource token -computation is shared with `Operation.resource` so the two sides compare like with like. Symfony's voter -attributes are the first data case (kimai evidence), not the definition. - -### hunt.prover -```python -@dataclass(frozen=True) -class Coverage: files_by_language, frameworks_recognised, entry_points, reached, unreached, operations_checked, - operations_discharged, unchecked_by_reason # all ints or dicts of ints + signature: tuple[str, ...] | None @dataclass(frozen=True) -class ProverResult: findings: tuple[dict, ...]; coverage: Coverage; degradations: tuple[dict, ...] +class CallTargetSet: + targets: tuple[SymbolId, ...] + completeness: Completeness +~~~ -def prove_change(root: Path, change: Mapping[str, Any], ctx: Context | None = None, *, max_depth: int = 3) -> ProverResult -``` -- Touched functions come from `_candidates`-style enumeration (touched head lines to function spans), build - output left out via `source.generated_reason`. -- Targets = touched functions plus callees that hold a protected operation, joined by qualified key - (`resolution.qualify`) and followed down through calls within the `down_depth` budget (default 2) sharing the - fan-out bound, so an operation one call deeper than the handler is reached `[2026-10-29]` (3.7). -- The `callers` adapter resolves a target to its call sites through the caller index and keeps only callers - whose receiver binds to the target's class (or subclass); unresolvable receivers fall back to the bare name - and are counted `receiver_unresolved` in coverage `[2026-10-29]` (3.9). -- Findings: for each `ObligationFinding`, a hunt defect dict with `path`, `line`, `family="access_control"`, - `function`, `evidence` (entry record summary, hops, operation id and calls, missing kind), `id` as the checker - emits. -- Degradations and every unchecked reason land in `Coverage`. +The symbol index covers repository-defined declarations and inheritance. Exact receiver and full signature produce +one complete target. Partial type or signature information produces a finite candidate set with an incompleteness +reason. No call falls back to a global bare-name key. Base declarations attach through explicit descendant edges. -### prover_arm -`python -m benchmarks.valid.prover_arm run POOL --repos REPOS --out DIR [--slice 1] [--only all] [--max-depth 3]` -writes `.json` per change (replay record envelope copied from `hunter_arm`: id, case_id, -repo, kind, family, path, function_lines, files, head, instrument {changed_bytes, hook_bytes_read, head_verified}, -findings, coverage, seconds, status), resumes by skipping done records, then `summarize` writes `summary.json` -(metrics from `benchmarks.valid.metrics.summarize`, per-repository and per-framework coverage, changes over 120 s, -instrument failures) and refuses when any record read zero bytes of a file git holds. +### Function summaries and paths +~~~python +@dataclass(frozen=True) +class FunctionSummary: + symbol: SymbolId + operations: tuple[Operation, ...] + witnesses: tuple[Discharge, ...] + calls: tuple[CallTargetSet, ...] + completeness: Completeness +~~~ -Anchor refusal `[2026-10-29]` (5.6): `_prove` validates every returned finding's `path` against the files it -actually read (`instrument.file_bytes`); a finding on an absent path marks the record -`status="instrument_failure"`, reason `stale_anchor`, findings cleared -- the same treatment as a zero-byte -read. `summarize` refuses to summarise a run containing such records, listing them by record id. +Summaries are computed by a monotone worklist over strongly connected call components. Their finite contents grow +by union until stable. A budget cutoff stops growth, records the cutoff and leaves affected summaries incomplete. +Concrete paths are then materialised from recognised entries through exact targets for evidence. Candidate edges +may contribute diagnostic traces but cannot complete a final path. + +### Witness matching and judgment +~~~python +@dataclass(frozen=True) +class WitnessMatch: + relation: EvidenceRelation + resource_relation: EvidenceRelation + authority_relation: EvidenceRelation + evidence: tuple[str, ...] + +@dataclass(frozen=True) +class PathJudgment: + judgment: PairJudgment + missing: tuple[str, ...] + completeness: Completeness + matches: tuple[WitnessMatch, ...] +~~~ + +A witness governs an obligation only when kind, scope, resource, authority and dominance are all `MUST`. +Any `MAY` or `UNKNOWN` required relation makes the path indeterminate. With complete evidence and no governing +witness for a required kind, the path is unguarded. Multiple paths aggregate as follows: + +- any complete unguarded path -> `unguarded`; +- complete enumeration and every path discharged -> `discharged`; +- otherwise -> `indeterminate`. + +The checker gains an opt-in abstract mode. Legacy callers keep the current boolean result and order-based default. + +### Strict CFG dominance +`CfgDominance.relation` returns an evidence relation and a guard effect. Prover mode never calls +`OrderDominance` when a graph, line mapping or construct is unavailable; it returns `UNKNOWN` with +`cfg_unavailable` or `line_without_node`. Route and declaration scopes return `MUST` only after exact handler +attachment. The legacy dominance class remains unchanged. + +### Target knowledge and acquisition +The mapping registry and fact interpreter are target-aware adapters. The initialization job has: + +- extraction mode for existing strategies and fact rows; +- proposal mode for source- or documentation-derived candidate knowledge; +- verification that checks source, version, region and concrete matches; +- promotion that writes only verified rows or enabled strategies; +- an acquisition record containing input revision, evidence digest, accepted/rejected proposals and output digest. + +Admission mode prevents the acquisition process from receiving benchmark labels or fix locations. A changed output +digest after labels are opened spends the population. + +### Prover integration +`prove_change` orchestrates cached reads, recognition, resolution, summaries, paths, strict dominance and +judgment. It emits findings only for `unguarded` pairs and preserves all three judgments as traces. Coverage +contains stage counts, reason counts, pair judgments and exploration cutoffs. Exceptions are recorded at the stage +that raised them. + +### Development and admission runners +Before comparison, the development runner materialises and validates two immutable bundles: + +~~~python +@dataclass(frozen=True) +class AnalyzerBundle: + analyzer_revision: str + fact_set_digest: str + acquisition_record_digest: str + configuration_digest: str +~~~ + +The baseline bundle points to the analyzer revision and fact set that produced the immutable 2026-10-28 records; +the candidate bundle points to the amended equivalents. The runner refuses a four-arm comparison if either +revision or fact artifact cannot be materialised and digest-verified. It then registers baseline +analyzer/baseline facts, baseline analyzer/candidate facts, candidate analyzer/baseline facts and candidate +analyzer/candidate facts. This separates knowledge coverage from engine behavior. + +The admission runner accepts only a frozen manifest naming analyzer, facts, acquisition, configuration and +population digests. The population manifest is produced and reviewed by `valid-detection-benchmark`; this spec +only consumes and validates it. The runner verifies its review and isolation fields, scores its paired +vulnerable/fixed cases and reviewed ordinary labels, refuses zero-byte or stale-anchor records, fails any change +over 120 seconds, and never converts indeterminate pairs to clean results. + +## Data Models + +### Canonical trace +Each trace carries: +- entry identity and target-knowledge evidence; +- exact hops and call-target completeness; +- operation kind, resource and authority; +- witnesses with kind, scope, provenance, resource, authority, dominance and match relations; +- control context and guard effects; +- completeness reasons and final path judgment; +- analyzer, fact-set and input digests. + +Repository identity, repository size and function-size features remain outside decision input. + +### Run manifest +The manifest contains population role (`development` or `admission`), immutable input digest, analyzer revision, +fact-set digest, acquisition-record digest, configuration digest, label-review state and spent-state marker. +The analyzer/fact bundle is a separate immutable input whose artifacts must be materialisable by revision and +digest; a manifest cannot redefine or synthesize the baseline. ## Error Handling -- Exceptions inside `prove_change` per file are recorded under their own reason key - `error:` `[2026-10-29]` (7.3), never folded into `framework_unrecognised` or any other - quiet reason; the change is still proved for the other files. A provider never appears (no model call). A - checkout failure is an instrument failure on the record (`status="instrument_failure"`, reason type only). +- Parse, recognition, resolution, summary, CFG and judgment exceptions become stage-specific incompleteness reasons. +- Deadline, fan-out, depth and recursion limits preserve accumulated evidence and return indeterminate affected + pairs. +- Zero-byte reads and stale anchors are instrument failures that invalidate the run. +- Missing or mismatched manifest digests invalidate admission rather than falling back to development mode. ## Testing Strategy -- Unit: each recogniser on a fixture file written in the test (not copied from clones) with positive and negative - cases; `compose_paths` on a three-file fixture (depth 1, 2, 3, unreached, fan-out cut, same-name in two files); - `witnesses` for a Laravel route file, a Symfony attribute, a Tornado decorator. `[2026-10-29]`: - `class_table`/`qualify` on a fixture with two same-name methods on different classes (distinct keys), two - same-name methods with different arity (distinct keys), an unresolvable receiver (bare name + - `receiver_unresolved` counted), an abstract base method reached through a subclass (attaches) and through an - unrelated class (does not); a programmatic `addServlet` registration fixture yielding entries at the - registered class's methods with registration evidence, and an unresolved registration yielding coverage only; - a voter fixture (`isGranted` with attribute, `voteOnAttribute` implementation) yielding a `voter` witness with - the attribute as resource; a resource-mismatch fixture (guard binds another object's resource -> operation - stays undischarged). -- Integration: `prove_change` on a git fixture with a Stapler-style class: an unguarded `doTestConnection` that - calls `lookupCredentials` yields one finding with hops and missing `path_guard`; the same with - `Jenkins.get().checkPermission(...)` above the call yields none; a Laravel controller behind `auth` middleware - yields none; an unrecognised framework yields coverage only. `[2026-10-29]`: the guard sits one call deeper - than the handler (a helper checks permission before the operation) and discharges; a guard whose trace shows - it dominating before the call produces no finding; an operation on a base handler class attaches to the - subclass route only; two classes with the same method name keep separate verdicts. -- Runner: a two-change fixture pool produces records the metrics summarise; a zero-byte read refuses; - a fixture finding anchored to an absent path refuses with `stale_anchor` `[2026-10-29]`; a fixture raising a - recognition exception counts it under `error:` and not under `framework_unrecognised` - `[2026-10-29]`. +- Unit: the complete join table, dimension conjunction, witness aggregation and monotonicity laws; symbol + collisions and overload candidates; resource aliases and authority + implication; SCC termination; CFG unknown behavior; three-way aggregation. +- Metamorphic: renaming a type preserves judgment; adding an unresolved overload can only preserve a judgment or + move it to indeterminate; removing semantic evidence cannot switch directly between discharged and unguarded. +- Integration: exact unguarded and discharged paths; a guard in a called helper; registration-site entries; base + attachment; resource mismatch; authority insufficiency; ambiguous calls; CFG unavailable; budget cutoff. +- Runner: baseline/candidate bundle materialisation, four-arm attribution, paired vulnerable/fixed scoring, + reviewed-manifest validation, freeze-digest guard, zero-byte and stale-anchor refusal, indeterminate rate, and + hard 120-second gate. + +## Migration Strategy +1. Add abstract types and adapters without changing legacy checker defaults. +2. Add strict resolution, summaries and judgment behind the prover's opt-in path. +3. Migrate traces and coverage, then enable the amended development arms. +4. Freeze facts and analyzer before running a separate admission population. + +Rollback is the previous prover arm and fact-set digest; baseline records remain immutable and comparable. diff --git a/.kiro/specs/access-control-prover/requirements.md b/.kiro/specs/access-control-prover/requirements.md index 7e318aa..ea71423 100644 --- a/.kiro/specs/access-control-prover/requirements.md +++ b/.kiro/specs/access-control-prover/requirements.md @@ -1,304 +1,279 @@ # Requirements Document ## Project Description (Input) -An access-control prover: a deterministic check that an operation needing authorization is reachable from an -entry point without a check dominating the path, modelled per framework, built from the existing obligation facts, -caller index and entry-point mapper, scored as a rule on the access-control training pool (recall on 23 fix -changes, false alarms per 100 ordinary pushes) and feeding the proof arm. +An access-control prover: a deterministic check that a protected operation is reachable from an attacker-facing +entry point without a required authorization check governing that path. The prover consumes acquired entry, +operation and enforcement facts, resolves calls and resources conservatively, emits an ordered trace for every +examined pair, and is measured separately on development and admission populations. ## Introduction -The maintainer's finding of 2026-10-14: the hunter's features (diff shape, function size, callers, entry-point -counts, name roles, textual obligation order) describe the shape of code around a change and cannot decide that -code is unsafe. Unsafety for access control is a property: an operation that needs authorization is reachable by a -caller that no check has constrained. The access-control training pool (23 fix changes, 93 verified locations, -460 ordinary pushes, 23 application repositories) holds exactly that shape: a permission check added before a -protected operation in a web-exposed method. Seventeen of the 23 fixes are Jenkins plugin web methods. +The security object for access control is not the shape of a changed function. It is an ordered path from an +attacker-facing entry to a protected operation, together with the authorization evidence that governs every +relevant control-flow and call-flow step. The 2026-10-28 development measurement established a useful baseline: +15 of 23 fix changes detected, 15.0 flagged ordinary pushes per 100, and no instrument failures. The subsequent +ablation showed that unresolved calls, over-broad resource matching, missing registration facts and silent +fallbacks account for both missed detections and false alarms. -This spec delivers the prover for that one family, as a deterministic rule with no model call, measured on the -pool with the standard metrics, and emitting findings that carry the unguarded path so the proof arm can act on -them. It is the increment that follows the annotation ablation in `hunter-learning-loop`. +This amendment makes uncertainty part of the result rather than a side counter. A pair is `unguarded`, +`discharged`, or `indeterminate`; degraded resolution, missing control-flow semantics, incomplete facts and +budget cutoffs cannot create a final security verdict. It also separates label-blind fact acquisition and +development regression from admission measurement on untouched repositories. -**Amendment 2026-10-29 (after the 2026-10-28 measurements).** Gates 1-3 measured the built prover on the pool: -recall 65.2% (15/23), 15.0 false alarms per 100 ordinary pushes, a zero-shot judge that costs no recall but -drops almost no false alarms. The taxonomy of the 8 misses and of 12 sampled kept false alarms points at one -cross-cutting gap: the prover resolves too shallowly and too loosely. Operations and guards one call deeper -than a handler are invisible; same-name methods on different classes are conflated; operations declared on -abstract bases are projected onto routes that never implement them; coarse guards (a path guard, a generic -ownership check) discharge operations whose resource they do not bind. This amendment adds the resolution -requirements (Requirement 3 acceptance criteria 7-10, Requirement 2 acceptance criteria 9-10), the -programmatic-registration entry facts (Requirement 1 acceptance criterion 9), and the failure-visibility -criteria (Requirement 5 acceptance criterion 6, Requirement 7 acceptance criterion 3). Acceptance criteria -added or changed by this amendment carry the tag `[2026-10-29]`. - -Per the specification-level steering rule, this amendment states **acquisition capabilities**, not per-target -inventories: the target vocabulary implied below (registration sites, handler-name families, policy-witness -shapes) is data the fact pipeline acquires per target -- a one-time initialization job per target can produce -it, and can extract the target knowledge already embedded in the repository's recogniser code into the same -structures -- with the engine's verification discipline admitting each row. The named repositories appear only -as benchmark evidence the acquired data must satisfy. +Concrete frameworks and repositories are benchmark evidence, not acceptance-criteria inventories. Target +vocabulary is acquired as reviewed data or recogniser strategies and is verified before promotion. The abstract +interpretation engine remains target-agnostic. ## Boundary Context -- **In scope**: entry-point recognition for the pool's frameworks; reachability paths from entry points to - touched functions through the existing caller index; framework enforcement points that discharge an obligation - outside the function (route middleware, controller attributes, declared public routes); resolution of calls on - those paths precise enough to place operations and guards in the function that holds them `[2026-10-29]`; - the verdict per change; a runner that scores the verdict as an arm on the pool; a coverage statement per - repository. -- **Out of scope**: taint flow, the Joern engine, any model call inside the prover, new families beyond access - control, a project-owned declared policy file (exists in `authorization-obligations` and is consumed as is), - the unseen pilot measurement (G1 exit, run by the maintainer after this arm exists), the pre-push hook wiring - (`pre-push-safety-net`), client-side JavaScript permission gating (hiding controls in a browser frontend -- - the byobu miss of gate 3 is not a server-side security object) `[2026-10-29]`, tuning the zero-shot judge - prompt (gate 2 measured the judge inert on this pool; the lever is the trace, not the prompt) - `[2026-10-29]`, re-auditing the pool's negative pushes (owned by `valid-detection-benchmark`) - `[2026-10-29]`. -- **Adjacent expectations**: `authorization-obligations` owns the facts schema, the checker and the dominance - protocol; this spec extends facts and supplies paths and witnesses through the checker's existing parameters. - `hunter-learning-loop` owns the feature table and the hunter arms; the prover is scored beside them with the - same metric functions. `search-with-proof` consumes the finding's path and operation to build a demonstration. - `valid-detection-benchmark` owns the pool: 3 of 12 sampled "ordinary" pushes carry real missing-check bugs - (pre-2019 negatives), so false-alarm counts read against that pool overstate the prover's error until the - negatives are re-audited `[2026-10-29]`. +- **In scope**: acquired entry, operation and enforcement knowledge; exact and conservative call resolution; + resource- and authority-sensitive witness matching; bounded interprocedural summaries and concrete evidence + paths; control-flow-sensitive dominance; three-way pair judgments; failure-visible coverage; development and + admission runners. +- **Out of scope**: taint flow; the Joern engine; model calls inside the prover; vulnerability families other than + access control; client-side presentation gating; pre-push hook wiring; proof execution; hand-tuning vocabulary + from evaluation labels. +- **Adjacent expectations**: `authorization-obligations` supplies the existing checker and fact contracts; + `valid-detection-benchmark` supplies reviewed populations; `search-with-proof` consumes unguarded traces; + `pre-push-safety-net` may consume the arm only after admission passes. ## Requirements -### Requirement 1: Entry points of the pool's frameworks -**Objective:** As a maintainer, I want the entry-point mapper to name the web-exposed methods of the frameworks -the pool uses, so that reachability starts where an attacker starts. +### Requirement 1: Acquired attacker-facing entry points +**Objective:** As a maintainer, I want entry recognition to consume verified target knowledge, so that new targets +can be covered without adding target vocabulary to the analysis engine. #### Acceptance Criteria -1. When a Java file declares a public method whose name starts with `do` in a class that extends or implements - a Jenkins or Stapler exposed type (Descriptor, Action, RootAction, Plugin, UnprotectedRootAction, - AbstractDescribableImpl, or a parameter typed StaplerRequest, StaplerResponse or annotated QueryParameter), - the mapper shall record an entry point of kind `route` with trust boundary `http_request` and the method's - line range, with access `public` when the class implements UnprotectedRootAction and `unknown` otherwise. -2. When a PHP file declares a Symfony controller action (a method carrying a `Route` attribute or annotation, or - a class extending AbstractController with public methods named by a routes file), the mapper shall record it - as a `route` entry with the attribute's path as evidence. -3. When a PHP Livewire component or Laravel controller method is registered by a route file, a `Route::` call, a - `wire:` binding or a public method on a class extending Livewire Component, the mapper shall record it as a - `route` entry, and shall carry a declared access of `public` only when the route file names no middleware. -4. When a TypeScript or JavaScript file under a Remix or React Router routes directory exports `action` or - `loader`, the mapper shall record each export as a `route` entry with trust boundary `http_request`. -5. When a Python class extends a Tornado RequestHandler or WebSocketHandler, the mapper shall record its `get`, - `post`, `put`, `delete`, `patch` and `open` methods as `route` entries. -6. When a Java class extends a Servlet, a Jetty handler or a JAX-RS resource, the mapper shall record the - request methods as `route` entries (existing Servlet and JAX-RS rows are kept; Jetty handlers are added). -7. The mapper shall record every recogniser's evidence strings so a finding can name why a method is an entry. -8. If a file's framework is not recognised, then the mapper shall record nothing for it and the coverage - statement (Requirement 7) shall count the file as unchecked; silence is never a pass. -9. `[2026-10-29]` When the repository's own code registers a handler at a call site rather than declaring it - through annotations or configuration, the mapper shall record the registered class's request methods as - `route` entries with the registration site and the registered class as evidence, so that a server assembled - in code still yields entry points. The registration-site vocabulary for a target is acquirable data under - Requirement 2 acceptance criterion 7's discipline, not engine code; Jetty's programmatic servlet - registrations are the first case (the seatunnel miss of gate 3). +1. When verified target knowledge describes a declarative entry shape, the mapper shall record every matching + repository-defined handler as an entry with its source range, trust boundary and recognition evidence. +2. When verified target knowledge describes a call-site registration, the mapper shall resolve the registered + repository-defined handler and record its request methods as entries with the registration site and resolved + handler identity as evidence. +3. If a registration target cannot be resolved to repository-defined code, the mapper shall emit no entry for it + and shall record `registration_unresolved` coverage. +4. When acquired knowledge proves that an entry is intentionally public, the mapper shall record access `public`; + otherwise, the mapper shall record access `unknown` rather than infer public access. +5. The mapper shall preserve the promoted fact or strategy identifier and the concrete source evidence on every + entry record. +6. If no promoted entry knowledge covers a file, the prover shall record `framework_unrecognised` and shall not + interpret the absence of entries as a clean result. +7. When target entry knowledge is added or updated, the system shall apply it through data or a registered + recognition strategy without changing target-agnostic analysis modules. -### Requirement 2: Enforcement points outside the function -**Objective:** As a maintainer, I want checks that frameworks apply outside the handler to count as discharges, -so that a guarded route is not reported because its handler body shows no check. +### Requirement 2: Acquired protected operations and enforcement evidence +**Objective:** As a maintainer, I want operations and authorization evidence represented as verified knowledge, +so that the prover compares the correct action, resource and authority. #### Acceptance Criteria -1. When a Laravel route registration attaches `auth`, `can:`, `role` or `permission` middleware, or a controller - calls `authorizeResource` or `middleware` in its constructor, the prover shall supply a discharge witness of - scope `router` for every handler the registration covers. -2. When a Symfony action carries `IsGranted`, `Security` or a `denyAccessUnlessGranted` call, or security.yaml's - `access_control` covers its path with a role, the prover shall supply a `decorator` or `router` witness. -3. When a Jenkins web method, or a method it calls on its own path, calls `checkPermission`, - `checkAnyPermission` or guards on `hasPermission` with an exit, the existing statement witnesses shall apply; - `RequirePOST`, `POST` and `Interceptor` annotations shall not count as authorization. -4. When a Remix action or loader calls a session requirement (`requireUser`, `requireUserId`, - `requireAuthentication`, `authenticateApiRequest`, `authorize`) before the operation, the prover shall treat - that call as a path guard, and when the operation reads a record by an identifier from the request without an - ownership constraint bound to the authenticated principal the prover shall report the missing - `ownership_check` (the pool's CWE-639 case). -5. When a Tornado handler is decorated with `authenticated` or `tornado.web.authenticated`, or the class - overrides `get_current_user` and checks it before the operation, the prover shall treat that as a path guard. -6. Where a declared policy marks a route public, the prover shall suppress `path_guard` findings for it and - keep `ownership_check` findings, as the checker already does. -8. Where a framework's security model makes the web method itself the protected operation (Jenkins form - validation and list-filling methods `doCheck*`, `doFill*Items`, `doTest*`, `doValidate*`, `doVerify*`, which - Jenkins requires to check a permission; Tornado handler methods; a Remix action), the facts shall be able to - name the obligation by handler name pattern and framework, and the prover shall apply such an operation only - to functions the mapper recognised as entries of that framework, at the method's declaration line. -7. The prover shall write every enforcement fact as closed data in the obligation facts files, with the header - naming the clones and references checked, and shall never add a name that does not occur in the checked code - or the framework's documentation. A proposed fact (from a maintainer or an LLM proposal pass) is promoted to - a closed row only after the same header discipline is satisfied `[2026-10-29]`; per-target vocabulary enters - as data through this gate, never as engine code. -9. `[2026-10-29]` The facts shall be able to name, by handler-name pattern and by the privileged calls the - handler makes, webhook and build-trigger obligations and protected-data exposure obligations, applied at the - method's declaration line to entries the mapper recognised. The name families for a target are acquirable - data under acceptance criterion 7's discipline -- a one-time initialization pass per target can produce them - (and can extract the vocabulary already embedded in the repository's recogniser code into those structures) - -- and the pool's Stapler webhook and data-exposure handlers are the first cases (the git-plugin, p4, - analysis-core and global-build-stats misses of gate 3 all reached the entry and checked no operation). -10. `[2026-10-29]` A guard shall discharge an operation only when it binds that operation's resource: when the - guard constrains a different path, a different object, or a permission level the operation does not require, - the prover shall treat the operation as undischarged (the crx and kimai misses of gate 3: a generic - `path_guard` or `ownership_check` dominated a credentials form-fill and invoice actions whose resource it - never touches). Where the target's policy layer decides access by an attribute or subject of the request -- - a voter, policy, or capability decision reachable from the action or a function it calls -- the prover shall - supply a policy witness scoped to that action's operations with the attribute or subject as its resource; - Symfony's voter decisions are the first case. +1. When promoted operation knowledge matches a call or recognised handler, the prover shall record the protected + operation, its required authorization kinds, its resource identity and any required authority. +2. When promoted enforcement knowledge matches a statement, decorator, route, policy decision or equivalent + construct, the prover shall record a witness with its scope, resource identity, authority and provenance. +3. When a handler name itself denotes a protected action, the prover shall apply that operation only to an entry + recognised for the same promoted target knowledge. +4. When a route or declared policy marks an entry public, the prover shall waive only a request-level path guard + and shall preserve resource, ownership and authority obligations. +5. When a witness binds a different resource or an insufficient authority, the prover shall not use that witness + to discharge the operation. +6. When a witness is request-global, the prover shall use it without resource equality only when the operation + fact explicitly declares that witness kind sufficient at request scope. +7. If resource identity or authority compatibility cannot be decided, the prover shall treat the witness match as + unknown rather than matching it broadly or rejecting it as definitely unrelated. +8. When one authority implies another, the prover shall apply that implication only from promoted target + knowledge and shall record the implication used in the trace. +9. When target knowledge is extracted or proposed, the acquisition workflow shall verify its source, version, + region and match evidence before promoting it to closed data or an enabled strategy. +10. If proposed target knowledge contradicts the inspected source or lacks verification evidence, the acquisition + workflow shall reject it with a reason and shall not modify promoted knowledge. -### Requirement 3: Reachability paths through the caller index -**Objective:** As a maintainer, I want a path from an entry point to each touched function, so that an -obligation inside a helper is judged by the checks on the way to it. +### Requirement 3: Conservative interprocedural reachability +**Objective:** As a maintainer, I want calls resolved to stable program identities and paths carried through +helpers, so that unrelated same-name code neither creates nor suppresses findings. #### Acceptance Criteria -1. When a change is checked out at head, the prover shall build, for every touched function and every function - that holds a protected operation it calls, the caller chains that end at an entry point, through the - per-change caller index, up to a configurable depth with default 3 and a configurable fan-out with default 25 - callers per step. -2. The prover shall emit each chain as a path record whose hops are `path::function` strings from the entry to - the operation's function, in the shape `check_obligations` and `OrderDominance` already consume. -3. If a touched function is itself an entry point, then the prover shall emit the one-hop path. -4. If no chain reaches an entry point within the depth, then the prover shall record the function as - `unreached` in the coverage statement and shall produce no finding for it. -5. The prover shall deduplicate chains, shall stop at the first entry point on a chain, and shall bound the work - so a change of the pool's largest repositories finishes within the budget of Requirement 6. -6. When two functions share a name in different files, the prover shall keep the chains separate by file. -7. `[2026-10-29]` When a function on a path calls another function of the repository that holds a protected - operation, the prover shall extend the path through that call (within the depth and fan-out budget) so the - operation is checked even though no touched function holds it directly; an operation buried one call deeper - than the handler shall not be invisible (the gate 3 operation-fact misses). -8. `[2026-10-29]` When a guard sits in a called function on the path, before the call or before the operation, - the trace shall carry it with its own function, line and kind, and dominance shall honour it as if it sat in - the hop's own function; a guard one call deeper than the handler shall still discharge (the dependency-track - and shopper false alarms of gate 3). -9. `[2026-10-29]` The prover shall resolve calls by signature and receiver: same-name methods on different - classes (the vault and p4 false alarms) and same-name overloads with different parameter lists shall stay - distinct, and an operation or entry declared on an abstract or base class shall attach only to paths whose - concrete class the repository defines (the mage-ai false alarm: `BaseDetailHandler.get` projected onto an - unrelated internal route). -10. `[2026-10-29]` A guard already recorded on a hop before a call shall be carried into the pair's trace and - dominance verdict; the prover shall not emit a finding whose own trace shows a dominating guard of the - required kind (the trigger.dev false alarm of gate 3). +1. When a touched function or reachable helper contains a protected operation, the prover shall construct caller + chains from recognised entries to that operation within the configured work budget. +2. When a call target can be identified by module, enclosing type, method and signature, the prover shall keep + that identity distinct from every other same-name target. +3. When more than one call target remains feasible, the prover shall preserve the finite candidate set and shall + mark the call incomplete rather than merge the candidates under a bare name. +4. If no bounded candidate set can be established, the prover shall mark the call unresolved and shall not use it + to create a final discharged or unguarded judgment. +5. When an operation or entry is declared on a base type, the prover shall attach it only to repository-defined + concrete descendants whose resolved identities support that attachment. +6. When a helper calls another helper that contains an operation or governing authorization evidence, the prover + shall continue the analysis through that call while budget remains. +7. When recursion is present, the prover shall terminate and shall preserve the accumulated operations, + authorization effects and incompleteness reasons for the recursive component. +8. If depth, fan-out, time or another work bound truncates exploration, the prover shall record the exact cutoff + reason and shall treat affected pairs as incomplete. +9. When a complete chain is materialised, the prover shall emit its hops from entry to operation with the call + site of every transition. +10. When multiple complete chains reach the same operation, the prover shall evaluate each chain independently so + that a guarded chain cannot hide an unguarded chain. -### Requirement 4: The verdict -**Objective:** As a developer about to push, I want a finding only when the tool can show an unguarded path to a -protected operation, so that every alarm names what to add and where. +### Requirement 4: Access-control verdicts +**Objective:** As a developer about to push, I want a finding only for a demonstrated unguarded path, so that every +alarm names a concrete security obligation and repair location. #### Acceptance Criteria -1. When a protected operation is reached by a path record and no witness of a required discharger kind - 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 - obligation facts, or whose framework is unrecognised; each such case shall be counted under its reason. -4. The prover shall make no model call. -5. The prover shall report findings in the hunt defect shape (`path`, `line`, `family`, `evidence`, - `function`), so the existing scoring, the proof arm and the pre-push admission consume them unchanged. -6. When a touched function holds no protected operation and reaches none, the prover shall emit nothing for it. +1. When a complete path reaches a protected operation, at least one required authorization kind is proven absent, + and every other required kind is proven either governing or absent, the prover shall judge the pair + `unguarded` and shall report each absent kind. +2. When every required authorization kind is proven to govern the operation on a complete path, the prover shall + judge the pair `discharged`. +3. If the evidence is insufficient for either final judgment, the prover shall judge the pair `indeterminate`. +4. When a pair is `unguarded`, the prover shall emit one finding per operation and missing authorization kind with + family `access_control`, exact source anchor, entry, hops and evidence. +5. When a pair is `discharged` or `indeterminate`, the prover shall emit no vulnerability finding for that pair. +6. The prover shall apply the recognised-entry-is-protected premise only in its explicit opt-in mode and shall + identify that premise in the evidence. +7. The prover shall make no model call and shall return findings in the existing hunt-defect contract. -### Requirement 5: Scoring as a rule arm on the pool -**Objective:** As a maintainer, I want the prover scored on the training pool with the standard metrics, so that -its number stands beside the hunter arms and decides whether it becomes a G1 arm. +### Requirement 5: Development measurement +**Objective:** As a maintainer, I want repeatable development measurements, so that changes to facts and analysis +can be attributed without being mistaken for admission evidence. #### Acceptance Criteria -1. The runner shall run the prover over every change of a pool slice on the training clones, one checkout per - change, and shall write one record per change in the replay record shape that `benchmarks.valid.metrics` - scores (id, kind, repo, status, findings, bytes read, seconds). -2. The runner shall report recall on fix changes and on verified locations with Wilson intervals, false alarms - per 100 ordinary pushes, precision, instrument failures, and seconds per change, and shall refuse to - summarise when any record read zero bytes of a tree git holds. -3. The runner shall report a per-framework and per-repository coverage table: entry points found, touched - functions reached, operations checked, functions unchecked by reason. -4. The runner shall checkpoint records per change and resume by skipping finished ones. -5. The record of a run shall carry counts, digests and framework names, never repository names of reserved - populations, as the reserved-repository guard requires. -6. `[2026-10-29]` The runner shall refuse to summarise a run whose findings anchor to a path that is not - present in the change's analysed tree, the same way it refuses zero-byte reads: a finding on an absent file - is an instrument defect, not a result (the crx stale anchor of gate 3). +1. When a development population is run, the runner shall write one resumable record per change with analyzer, + fact-set, population and input digests. +2. When development records are summarised, the runner shall report recall on fix changes and verified locations, + flagged ordinary pushes per 100, precision, vulnerable/fixed pair correctness, instrument failures and runtime + distributions with uncertainty intervals where defined. +3. The runner shall report a stage funnel from entry recognition through call resolution, operation discovery, + control-flow evaluation, witness matching and pair judgment. +4. The runner shall report per-target-family and per-repository coverage without disclosing reserved repository + identities in shared records. +5. When comparing an amended analyzer and amended facts, the runner shall support the four registered arms formed + by old/new analyzer crossed with old/new fact set. +6. If any record reads zero bytes for a file present in the analysed tree or anchors a finding outside files read, + the runner shall mark an instrument failure and shall refuse the summary. +7. The runner shall label results from populations used to choose facts or analyzer behavior as development or + regression evidence and shall not present them as admission evidence. -### Requirement 6: Budget -**Objective:** As a developer, I want the prover to finish inside the pre-push window, so that it can run on -every push. +### Requirement 6: Pre-push budget +**Objective:** As a developer, I want the prover to finish inside the pre-push window, so that eligible detection +can run on every push. #### Acceptance Criteria -1. The prover shall finish a change of the pool within 120 seconds on the development host, measured by the - runner, and the runner shall list every change over that bound. -2. The prover shall reuse the per-change context caches (product files, texts, call index, file IR, entry - points) and shall not walk or read the product tree more than once per change. +1. When a measured change exceeds 120 seconds, the runner shall fail the budget gate and shall identify the + change, stage and elapsed time. +2. The prover shall reuse per-change file, text, syntax, call, entry, symbol and summary caches and shall not read + the product tree more than once per change. +3. If analysis stops because of a deadline, the prover shall return incomplete coverage and indeterminate affected + pairs rather than a partial clean verdict. -### Requirement 7: Coverage statement -**Objective:** As a developer, I want the tool to say what it did not check, so that no finding count reads as a -clean bill. +### Requirement 7: Failure-visible coverage +**Objective:** As a developer, I want the tool to state what it could not decide, so that silence never reads as a +clean bill of health. #### Acceptance Criteria -1. The prover shall return, with its findings, the counts of files by language, files whose framework was - recognised, entry points found, touched functions reached and unreached, operations checked and discharged, - and functions unchecked by reason (`parse_failed`, `language_unsupported`, `framework_unrecognised`, - `unreached`, `no_facts`). -2. When the coverage statement shows zero recognised frameworks for a repository, the runner shall mark the - repository `uncovered` in its summary, and recall for that repository shall be reported separately from the - covered recall. -3. `[2026-10-29]` When a recognition or resolution pass over a file raises an exception, the coverage statement - shall count that file under a reason that names the exception class, and shall never fold it into - `framework_unrecognised` or any other quiet reason (the byobu ValueErrors of gate 3 surfaced only by - inspection of the record). +1. The prover shall report files by language, recognised entry families, entries, reached and unreached targets, + operations, discharged pairs, unguarded pairs and indeterminate pairs. +2. The prover shall count unchecked or incomplete work by specific reason, including parse failure, unsupported + language, unrecognised target, absent facts, unresolved registration, ambiguous or unresolved call, exploration + cutoff, unavailable control flow, unknown resource, unknown authority and analysis exception. +3. If no target family is recognised for a repository, the runner shall mark the repository `uncovered` and shall + report its recall separately from covered recall. +4. When a recognition, resolution, summary or judgment pass raises an exception, the prover shall record the + exception class at that stage and shall not fold it into a quiet coverage reason. +5. When the same pair has multiple incompleteness reasons, the prover shall preserve every reason in the trace and + aggregate each reason in coverage. +6. The runner shall report the indeterminate rate separately and shall not include indeterminate pairs in either + clean or discharged counts. ### Requirement 8: Proof-arm feed -**Objective:** As the proof arm, I want each finding to carry what a demonstration needs, so that a finding -can be proved or dismissed without re-deriving it. +**Objective:** As the proof arm, I want each unguarded finding to carry a complete analysis witness, so that a +demonstration can be attempted without re-deriving the decision. #### Acceptance Criteria -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. +1. When a finding is emitted, it shall carry the entry record, exact hop list, operation, missing authorization + kind, resource and authority relations, pair judgment, trace identifier and completeness evidence. +2. The finding identifier shall remain stable for the same operation, source anchor and missing authorization + kind across deterministic replays. +3. If the pair is indeterminate, the prover shall expose its trace only as diagnostic coverage and shall not send + it to the proof arm as a vulnerability finding. -### 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. +### Requirement 9: Ordered traces for every examined pair +**Objective:** As a maintainer, I want every examined pair represented by the same deterministic trace, so that +decisions and degradations can be inspected and compared. #### 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. +1. When the prover examines an entry-operation path, it shall emit one trace containing the entry, ordered hops, + operation, authorization witnesses, resource and authority relations, control-flow relations, completeness + state and pair judgment. +2. The prover shall emit traces for unguarded, discharged and indeterminate pairs alike. +3. When an argument or resource is forwarded through a call, the trace shall preserve its origin through the + resolved hop; if origin cannot be followed, the trace shall record `unknown`. +4. The trace shall carry target knowledge identifiers and source evidence needed to reproduce the judgment but + shall omit repository identity, file-size and repository-size features from decision input. +5. The trace shall serialise to one deterministic canonical text form and one deterministic canonical JSON form. +6. When a work bound or fallback would have been required, the trace shall record the cutoff or unavailable + semantic fact rather than silently substituting a weaker analysis. +7. The runner shall persist traces and their analyzer, fact-set and input digests with the corresponding record. -### 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. +### Requirement 10: Control-flow-sensitive dominance +**Objective:** As a maintainer, I want authorization evidence to count only when control flow guarantees it governs +the operation, so that avoidable or ignored checks do not discharge obligations. #### 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), - `branches` (the operation lies only inside the guard's passing branch), 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. +1. When authorization evidence appears before an operation, the prover shall determine whether every feasible + path to the operation passes that evidence. +2. When a guard's failing branch terminates or the operation exists only in the passing branch, the prover shall + record the guard effect and may treat it as governing the operation when resource and authority also match. +3. When a predicate result is ignored or appears only on some paths, the prover shall not treat it as a governing + authorization check. +4. When an operation is inside a loop, exception region or conditional branch, the trace shall record that control + context and any exception handling that can bypass the guard. +5. When route- or declaration-scoped authorization evidence covers the whole handler, the prover shall preserve + that declared scope without inventing a statement location. +6. If control-flow semantics or source-to-control-flow correspondence is unavailable, the prover shall mark the + affected relation unknown and the pair indeterminate rather than decide it by textual order. +7. The existing order-based checker mode shall remain available to callers that do not opt into prover semantics. +### Requirement 11: Three-way abstract judgment +**Objective:** As a maintainer, I want uncertainty to propagate monotonically through the analysis, so that losing +precision cannot manufacture a vulnerability or a discharge. + +#### Acceptance Criteria +1. The prover shall represent call resolution, path completeness, resource compatibility, authority compatibility + and dominance with values that distinguish definite, possible, absent and unknown evidence. +2. When all required evidence on a complete path is definite and at least one required obligation has no governing + witness, the prover shall produce `unguarded` and shall report every such obligation, including when other + required obligations are definitely governed. +3. When every required obligation has a definite governing witness on a complete path, the prover shall produce + `discharged` for that path. +4. If any required relation is possible or unknown, or path enumeration is incomplete, the prover shall produce + `indeterminate` unless another complete path already proves `unguarded`. +5. When multiple paths reach one operation, the prover shall aggregate them as `unguarded` if any complete path + is unguarded, `discharged` only if enumeration is complete and every path is discharged, and `indeterminate` + otherwise. +6. When analysis precision is reduced by adding an unresolved candidate or removing semantic information, a final + judgment shall remain unchanged or move to `indeterminate`; it shall not switch directly between `unguarded` + and `discharged`. +7. The prover shall keep abstract-domain operations deterministic and independent of target names. +8. The runner shall expose judgment counts and transitions between compared arms so that precision loss cannot be + hidden inside aggregate recall or false-alarm metrics. + +### Requirement 12: Label-isolated admission workflow +**Objective:** As a maintainer, I want admission measured on untouched, reviewed evidence after the analyzer and +facts are frozen, so that a better development score is not mistaken for generalisation. + +#### Acceptance Criteria +1. When an admission run is prepared, the workflow shall freeze the analyzer revision, promoted fact-set digest, + acquisition record, configuration and population manifest before opening admission labels. +2. While acquiring target knowledge for an admission repository, the workflow shall use repository source and + approved documentation without vulnerability, fix-location or ordinary-change labels. +3. If acquisition observes evaluation labels or is changed in response to an admission result, the workflow shall + mark that population spent and shall not use it for admission. +4. When ordinary changes are prepared for a false-alarm denominator, the benchmark workflow shall review and + remove or relabel changes that contain real missing-authorization defects before scoring. +5. When a vulnerable case has a fixed twin, the admission run shall require the expected unguarded trace on the + vulnerable side and quiet or discharged behavior at the corresponding fixed operation. +6. When an amended prover is considered for the G1 arm, the workflow shall measure it on untouched repositories + that were not used to choose facts, recognition strategies, abstract-domain behavior or thresholds. +7. The admission report shall include recall, verified-location recall, flagged ordinary pushes per 100, + precision, paired vulnerable/fixed correctness, indeterminate rate, coverage, runtime and instrument failures + with sample counts and uncertainty intervals. +8. If the budget gate, instrument gate or pre-registered quality criteria fail, the workflow shall return NO-GO + and shall not enable the arm in pre-push admission. +9. The workflow shall retain the current 23-repository population as development regression evidence and shall + require a separate untouched population for admission claims. diff --git a/.kiro/specs/access-control-prover/research.md b/.kiro/specs/access-control-prover/research.md index 1c2d0e6..6b62183 100644 --- a/.kiro/specs/access-control-prover/research.md +++ b/.kiro/specs/access-control-prover/research.md @@ -205,3 +205,72 @@ records the code survey behind the design amendment (same date tag). lane (deferred injection spec) is the designated place to grow type facts, not this spec. - `down_depth` widens target enumeration; the fan-out bound and the 120 s budget cap it. Per-repository seconds-per-change in the runner summary will show any cost. + +--- + +## Abstract judgment and admission amendment -- 2026-10-29 + +### Context + +The design review after the capability-level lift found that the proposed amendment still allowed two degraded +instruments to participate in binary decisions: unresolved receivers fell back to a bare-name call key, and +unavailable CFGs fell back to source order. It also found that the fact-initialization task used known development +misses and then remeasured the same population, which is valid regression work but cannot qualify an admission arm. + +### Synthesis + +1. **Generalization**: call certainty, path completeness, resource compatibility, authority compatibility and + dominance are instances of one evidence-relation problem. They share a finite domain + (`MUST | MAY | NO | UNKNOWN`) and one incompleteness record instead of separate booleans and counters. +2. **Build vs adopt**: the repository already owns the semantic IR, structural CFG, obligation checker and path + records. A small abstract-domain layer and monotone function summaries extend those contracts; adopting another + graph or abstract-interpretation engine would duplicate the current architecture and violate steering. +3. **Simplification**: the prover keeps one checker and one concrete trace. Function summaries accelerate and + stabilize interprocedural discovery, but final evidence remains a materialised path. No second verdict engine is + introduced. + +### Decisions + +#### Decision: three-way judgment +- **Selected approach**: every path and aggregate pair is `unguarded`, `discharged`, or `indeterminate`. +- **Invariant**: less precise evidence may preserve a verdict or move it to `indeterminate`; it may not switch + directly between the two final verdicts. +- **Algebra**: `MUST` and `NO` are incomparable, both below `MAY`, which is below `UNKNOWN`. Alternative + evidence uses the least-upper-bound table; dimensions of one witness use conjunction; witnesses for one + obligation use existential aggregation. These operations are distinct so `MUST + NO` on alternative paths + becomes `MAY`, while one definite governing witness remains sufficient for the obligation it covers. +- **Consequence**: prover mode does not use textual order as a semantic fallback. Legacy checker callers retain it. + +#### Decision: stable symbols and finite candidate sets +- **Selected approach**: identify repository declarations by module, enclosing type, method and available signature. + Partial resolution returns a finite candidate set plus incompleteness; unbounded resolution returns unresolved. +- **Rejected approach**: global bare-name fallback, because it conflates unrelated methods and can both invent paths + and borrow unrelated guards. + +#### Decision: resource and authority are separate abstract values +- **Selected approach**: match witness kind, scope, resource and authority independently, joining each relation into + the pair judgment. Request-global guards are valid only when the operation fact explicitly allows that scope. +- **Rejected approach**: `None` as a resource wildcard. It cannot distinguish intentionally global authentication + from missing resource evidence. + +#### Decision: summaries discover; concrete paths prove +- **Selected approach**: monotone summaries over strongly connected call components collect operations, witnesses, + call target sets and incompleteness. Concrete paths are materialised from exact edges for trace evidence. +- **Trade-off**: summary and path code add one engine boundary, but they remove recursion and depth handling from + ad-hoc traversal and make every cutoff explicit. + +#### Decision: development attribution before admission +- **Selected approach**: compare old/new analyzer crossed with old/new facts on the current development population, + then freeze analyzer, facts, acquisition record, configuration and a separate untouched population for admission. +- **Consequence**: the 2026-10-28 numbers remain the immutable baseline. A better rerun on the same repositories is + regression evidence, not a G1 admission claim. + +### Risks and mitigations +- **Indeterminate inflation**: strict uncertainty may initially lower apparent coverage. Report the stage funnel and + reason distribution; improve the dominant reason rather than weakening the lattice. +- **Summary cost**: a repository-wide symbol graph may threaten the pre-push budget. Reuse Context caches, use finite + summary sets, and fail the budget gate when any measured change exceeds 120 seconds. +- **Authority vocabulary growth**: permission implication can become target-specific code. Keep implications in + promoted facts and include the fact identifier in every match. +- **Admission scarcity**: the current pool is already development data. Source and review a separate population + through `valid-detection-benchmark`; do not relabel the current pool as untouched. diff --git a/.kiro/specs/access-control-prover/spec.json b/.kiro/specs/access-control-prover/spec.json index 5935d40..16982b2 100644 --- a/.kiro/specs/access-control-prover/spec.json +++ b/.kiro/specs/access-control-prover/spec.json @@ -1,15 +1,15 @@ { "feature_name": "access-control-prover", "created_at": "2026-10-14T13:48:18Z", - "updated_at": "2026-10-29T15:40:00Z", + "updated_at": "2026-10-29T12:16:52Z", "language": "en", - "phase": "requirements-generated", + "phase": "tasks-generated", "approvals": { - "requirements": {"generated": true, "approved": false}, - "design": {"generated": true, "approved": false}, + "requirements": {"generated": true, "approved": true}, + "design": {"generated": true, "approved": true}, "tasks": {"generated": true, "approved": false} }, "ready_for_implementation": false, "depends_on": ["authorization-obligations", "valid-detection-benchmark", "hunter-learning-loop"], - "approval_note": "2026-10-14 maintainer directive in session: spec the prover and queue implementation with Codex (fast-track; the three gates were passed on that instruction, review the documents before the second delivery). 2026-10-29: requirements amended after the 2026-10-28 gates 1-5 measurements (trace resolution, programmatic entry facts, failure visibility); requirements await re-approval, then design and tasks must be revisited against the amendment before implementation resumes. 2026-10-29 (later): maintainer instruction in session ('can you address the issues?') treated as requirements approval and as the directive to regenerate the design; design.md amended in merge mode against the amendment (resolution component, resource-bound and voter witnesses, programmatic Jetty registration, stale-anchor refusal, error reasons), tasks.md still to be regenerated after design approval. 2026-10-29 (latest): maintainer directives lifted the specification to the capability level -- per-target vocabulary is acquired data (one-time initialization job with extraction and proposal modes behind the facts gate), never enumerated in acceptance criteria; engine/target split, GoF pattern discipline, complexity caps, and idiomatic naming recorded in .kiro/steering/code-standards.md; breadth map added at .kiro/steering/breadth-map.md. requirements.md, design.md and tasks.md were re-lifted accordingly; all three phases re-opened for approval in order." + "approval_note": "2026-10-14 maintainer directive in session: spec the prover and queue implementation with Codex (fast-track; the three gates were passed on that instruction, review the documents before the second delivery). 2026-10-29: requirements amended after the 2026-10-28 gates 1-5 measurements (trace resolution, programmatic entry facts, failure visibility). 2026-10-29 (later): maintainer instruction in session ('can you address the issues?') treated as requirements approval and as the directive to regenerate the design. 2026-10-29 (capability lift): per-target vocabulary became acquired data; engine/target split, pattern discipline and complexity caps were recorded in steering; all phases reopened. 2026-10-29 (abstract-interpretation amendment): the maintainer accepted the design-review recommendations by asking to make the amendments. Requirements and design were regenerated with a three-way judgment, explicit evidence algebra, stable symbols, resource/authority domains, label-blind acquisition and separate admission measurement; that directive is recorded as approval to regenerate tasks. The merged task plan passed an independent task-graph sanity review after two design repairs. Tasks await human approval before implementation." } diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md index 90147f1..dd6b31b 100644 --- a/.kiro/specs/access-control-prover/tasks.md +++ b/.kiro/specs/access-control-prover/tasks.md @@ -1,321 +1,348 @@ # Implementation Plan -- [x] 1. Paths from the caller index -- [x] 1.1 Add `PathRecord` and `compose_paths` in `src/openultrasast/semantic/obligations/paths.py` (P) - - Upward walk through a `callers(path, function)` callable, depth and fan-out bounds, stop at the first entry, - chains kept per file, deduplicated; unreached targets returned - - Done when `tests/test_obligation_paths.py` covers depth 1 to 3, unreached, fan-out cut and same-name files, - and `check_obligations` accepts the records as `paths` (one test runs the checker with them) - - _Requirements: 3.1, 3.2, 3.3, 3.4, 3.5, 3.6_ - - _Boundary: obligations.paths_ +## Completed baseline -- [x] 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)_ +The completed work below produced the immutable 2026-10-28 development baseline. Amendment tasks 7-13 replace +its final resolution, dominance, fact-acquisition and measurement semantics without erasing the evidence. -- [x] 2. Entry recognisers -- [x] 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 - `AbstractHandler`, `HttpServlet`, JAX-RS resources; evidence strings; `public` only for `UnprotectedRootAction` - - Done when `tests/test_mapping_frameworks.py` names the entries of a fixture Descriptor, rejects a private - helper named `doX`, and the existing mapping tests still pass - - _Requirements: 1.1, 1.6, 1.7, 1.8_ - - _Boundary: mapping_ -- [x] 2.2 Symfony, Livewire and Laravel controller, Remix export and Tornado recognisers in `mapping.py` (P) - - Done when fixture files of each shape yield `route` entries with evidence and the negative fixtures yield none - - _Requirements: 1.2, 1.3, 1.4, 1.5, 1.7, 1.8_ - - _Boundary: mapping_ +- [x] 1. Baseline paths and checker premise +- [x] 1.1 Add bounded caller-index paths with concrete hop records + - Delivered depth/fan-out traversal, entry stopping, file-qualified hops and unreached targets. + - Baseline fixtures cover depth, fan-out, deduplication and multiple same-name files. + - The final call semantics are superseded by tasks 8-9. + - _Requirements: 3.1, 3.9, 3.10_ + - _Boundary: Concrete Paths_ +- [x] 1.2 Add the opt-in recognised-entry-is-protected premise + - Existing checker defaults remain unchanged; prover evidence identifies the premise. + - _Requirements: 4.6_ + - _Boundary: Obligation Checker_ -- [ ] 3. Enforcement witnesses and facts -- [x] 3.1 `semantic/obligations/enforcement.py` producing router and decorator `Discharge` witnesses (P) - - Laravel route middleware and controller `middleware`/`authorizeResource`; Symfony `IsGranted`, `Security`, - security.yaml `access_control`; Tornado `authenticated`; names listed in the facts headers - - Done when `tests/test_obligation_enforcement.py` shows a guarded Laravel route, a Symfony attribute and a - Tornado decorator each produce one witness that `OrderDominance` accepts for the handler's operation - - _Requirements: 2.1, 2.2, 2.5, 2.6_ - - _Boundary: obligations.enforcement_ -- [ ] 3.2 Operation and discharger rows for the pool's shapes in `ruleset/obligations/{java,php,python,typescript}.toml` (P) - - Java: credential lookups and outbound connection tests in `doTestConnection`-style handlers, item reads and - writes, `checkPermission`/`checkAnyPermission` as path guards, `hasPermission` as ownership check; - Remix: session requirements as path guards, record reads by request id as protected reads needing - `ownership_check`; Tornado: handler `open`/`get` as entries needing `path_guard`; Jetty service start as - privileged action. Every name checked in the clones or documentation, said in the header - - Done when `tests/test_obligation_facts.py` loads the files and one operation and one discharger per - language resolve - - _Requirements: 2.3, 2.4, 2.7_ - - _Boundary: ruleset/obligations_ +- [x] 2. Baseline entry recognition +- [x] 2.1 Add the first Java entry recognisers and evidence + - Delivered development cases for declared web methods, servlets, resources and handlers. + - _Requirements: 1.1, 1.5_ + - _Boundary: Mapping_ +- [x] 2.2 Add the initial PHP, JavaScript, TypeScript and Python entry recognisers + - Delivered positive and negative fixture coverage with entry evidence. + - _Requirements: 1.1, 1.5_ + - _Boundary: Mapping_ -- [x] 3.3 Handler-named operations: `handlers` and `framework` fields in the facts loader, `find_operations(..., handlers_of=)`, Stapler form-validation rows in `java.toml`, Tornado handler rows in `python.toml`, Remix action rows in `typescript.toml` - - Done when `tests/test_obligation_facts.py` loads a handler-named row, `tests/test_obligation_operations.py` - (or the existing operations test file) yields the operation at the declaration line only for listed - handlers, and the prover smoke on the 23 fixes reaches and checks the Jenkins form-validation methods - - _Requirements: 2.8_ - - _Boundary: obligations.facts, obligations.operations_ +- [x] 3. Baseline enforcement and operation facts +- [x] 3.1 Add route-, declaration- and policy-scoped enforcement witnesses + - Delivered initial external-handler witnesses and integration fixtures. + - _Requirements: 2.2, 2.4_ + - _Boundary: Enforcement Adapter_ +- [x] 3.2 Close the unfinished per-target fact inventory as superseded + - The partially completed inventory is not treated as complete implementation. + - Tasks 11.3-11.7 replace it with label-blind acquisition and promoted target knowledge. + - _Requirements: 2.1, 2.2, 2.9, 2.10_ + - _Boundary: Target Knowledge_ +- [x] 3.3 Add handler-named operation facts + - Delivered opt-in handler operations at declaration lines for recognised entries. + - _Requirements: 2.3_ + - _Boundary: Fact Interpreter_ -- [x] 4. The prover -- [x] 4.1 `hunt/prover.py`: `prove_change` over the hunter `Context`, `Coverage`, findings as hunt defects - - Touched functions from head lines, build output left out, targets include direct callees holding operations, - IRs of hop files passed to the checker, extra witnesses from enforcement, coverage counts by reason, no model - - Done when `tests/test_hunt_prover.py` shows: an unguarded Stapler handler calling `lookupCredentials` gives - one finding with entry, hops and missing `path_guard`; a `checkPermission` above the call gives none; a - guarded Laravel route gives none; an unrecognised framework gives coverage only; the finding dict has - `path`, `line`, `family`, `function`, `evidence`, `id` - - _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_ +- [x] 4. Baseline prover, traces and structural control flow +- [x] 4.1 Integrate entries, paths, operations and witnesses in the deterministic prover + - Delivered hunt-defect findings and failure-visible baseline coverage with no model calls. + - Final three-way judgment is superseded by task 10.6. + - _Requirements: 4.7_ + - _Boundary: Prover Integration_ +- [x] 4.2 Emit deterministic ordered traces and local argument provenance + - Delivered canonical text/JSON traces for discharged and unguarded baseline pairs. + - _Requirements: 9.1, 9.2, 9.3, 9.5_ + - _Boundary: Canonical Trace_ +- [x] 4.3 Attach traces to prover records and findings + - Delivered trace references through the replay envelope. + - _Requirements: 8.1, 9.7_ + - _Boundary: Prover Integration_ +- [x] 4.4 Build structural control-flow graphs + - Delivered branches, loops, exits, exception regions, dominators and control context. + - _Requirements: 10.1, 10.2, 10.3, 10.4_ + - _Boundary: Structural CFG_ +- [x] 4.5 Add baseline CFG dominance and guard effects + - Delivered value-only rejection and control-context trace fields. + - Strict unknown semantics are superseded by task 10.1. + - _Requirements: 10.1, 10.2, 10.3, 10.4, 10.5_ + - _Boundary: CFG Dominance_ -- [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_ -- [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_ +- [x] 5. Baseline replay arm + - Delivered checkpointed records, standard metrics, coverage tables, zero-byte refusal and immutable records. + - _Requirements: 5.1, 5.2, 5.4, 5.6_ + - _Boundary: Development Runner_ -- [x] 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_ -- [x] 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_ +- [x] 6. Baseline development measurement + - Measured 23 repositories and 483 changes: 65.2% fix-push recall, 15.0 flagged ordinary pushes per 100, + 0 instrument failures; recorded at benchmarks/measurements/2026-10-28-access-control-prover/. + - The population is development evidence only and remains immutable. + - _Requirements: 5.2, 5.7, 12.9_ + - _Boundary: Development Measurement_ -- [ ] 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 - locations, Wilson), false alarms per 100, precision, instrument failures, seconds per change and the list - over 120 s, per-repository and per-framework coverage, `uncovered` repositories; refuse on zero-byte reads - - Done when `tests/test_prover_arm.py` runs a two-change fixture pool end to end and the summary carries - every field above; a record with zero bytes read makes `summarize` refuse - - _Requirements: 5.1, 5.2, 5.3, 5.4, 5.5, 6.1, 7.2_ - - _Depends: 4.1_ +## Amendment implementation -- [ ] 6. Measurement (maintainer, not Codex) -- [x] 6.1 Run the arm on `benchmarks/valid/train/pool-train.toml` over the training clones; write - `benchmarks/measurements/-access-control-prover/` with NOTES, summary, coverage table; compare with the - DSPy and hunter arms of the same pool - - _Requirements: 5.2, 5.3, 7.2_ - - Done 2026-10-28: `benchmarks/measurements/2026-10-28-access-control-prover/` -- 23-repo - pool (483 changes, 93 locations), recall 65.2% (Wilson 44.9-81.2), 15.0 FA/100, 0 - instrument failures; on the 5 repos shared with the 2026-10-14 hunt arms, prover 4/5 vs - DSPy 2/5 and hunter 2/5 (union 4/5), including trigger.dev which neither arm found. +- [ ] 7. Abstract evidence foundation +- [ ] 7.1 Implement the evidence-relation algebra and completeness value + - Encode the specified precision order, complete join table, dimension conjunction and witness aggregation. + - Preserve every incompleteness reason deterministically and deduplicate reasons without losing stage identity. + - Done when exhaustive table tests and algebraic law tests pass for every relation pair. + - _Requirements: 11.1, 11.6, 11.7_ + - _Boundary: Abstract Evidence Domain_ +- [ ] 7.2 Add resource abstract values and operation-fact fields + - Represent exact resources, finite alias sets, request-global scope and unknown resources. + - Extend operation facts to state when a request-global guard is sufficient. + - Done when resource parsing and joins distinguish exact, alias, global and unknown fixtures. + - _Requirements: 2.1, 2.5, 2.6, 2.7, 11.1_ + - _Boundary: Resource Domain_ + - _Depends: 7.1_ +- [ ] 7.3 Add authority abstract values and promoted implication facts + - Represent exact, finite and unknown authorities separately from resources. + - Load authority implications from promoted facts and retain the supporting fact identifier. + - Done when sufficient, insufficient and unknown authority fixtures produce the specified relations. + - _Requirements: 2.1, 2.2, 2.5, 2.7, 2.8, 11.1_ + - _Boundary: Authority Domain_ + - _Depends: 7.1_ +- [ ] 7.4 Extend judgment, trace and coverage contracts with abstract state + - Add three-way judgments, completeness and evidence relations without changing legacy defaults. + - Add canonical serialization for resource and authority relations and all incompleteness reasons. + - Done when old trace fixtures remain stable in legacy mode and new fixtures round-trip all abstract fields. + - _Requirements: 7.1, 7.2, 7.5, 7.6, 9.1, 9.2, 9.6_ + - _Boundary: Judgment Contracts, Canonical Trace_ + - _Depends: 7.1, 7.2, 7.3_ -- [ ] 7. Resolution foundation `[2026-10-29]` -- [ ] 7.1 `CallSite` receiver capture: `receiver: str | None` field on `semantic/ir.py`'s `CallSite`, captured - in `semantic/cst.py` call extraction (receiver expression text for `$obj->method` and `x.y.z` shapes; `None` - for bare calls); every existing consumer unchanged - - Done when IR fixtures show receiver text carried through call extraction for PHP/TS shapes, `CallSite` still - constructs without it for existing callers, and all existing IR/cst tests pass unchanged - - _Requirements: 3.9_ - - _Boundary: semantic.ir, semantic.cst_ -- [ ] 7.2 (P) `obligations.resolution`: `ClassRecord`, `class_table(texts, language)` cached per change on the - hunter `Context`, `qualify(receiver, enclosing_class, name, arity, table)` returning `Class.name`, - `Class.name/arity`, or the bare name; base-class attachment rule (attaches to extending classes only) - - Done when `tests/test_obligation_resolution.py` covers: two same-name methods on different classes give - distinct keys; same name different arity gives distinct keys; an unresolvable receiver gives the bare name - with `receiver_unresolved` counted; an abstract-base method attaches to a subclass call and not to an - unrelated class - - _Requirements: 3.9_ - - _Boundary: obligations.resolution, hunt.producers (Context cache field only)_ - -- [ ] 8. Guard binding and policy witnesses `[2026-10-29]` -- [ ] 8.1 (P) Resource-bound witnesses: optional `resource` field on `Discharge` (additive, default `None`); - enforcement mints tokens (route path for router middleware, attribute/subject for a policy-layer guard, - `None` for auth-class guards); policy-layer witness scoped to the action with the attribute or subject as - resource (a policy decision -- voter, capability check, or equivalent -- reachable from the action or a - function it calls). Which constructs count as policy decisions comes from the facts rows (task 10), never - engine code - - Done when `tests/test_obligation_enforcement.py` shows a resource-mismatch fixture (guard binds another - object's resource, the operation stays undischarged under `resource_bound`) and a policy-witness fixture - yielding a witness scoped to the action with the attribute as resource - - _Requirements: 2.10_ - - _Boundary: obligations.enforcement, obligations.operations (dataclass field only)_ -- [ ] 8.2 Checker opt-in `resource_bound` and all-kind caller-hop re-judgement in `check.py`'s `_on_caller_hop`: - a witness with `resource` set suppresses only operations whose resource token matches; every discharger kind - is re-judged on earlier hops at the hop's call line; `guards_before_call` participates in the re-judgement - - Done when the existing checker tests pass unchanged and new tests show: keyword off keeps today's behaviour - (including the `assume_entries_protected`-gated hop re-judgement); keyword on, a mismatched-resource witness - does not suppress; a guard one call deeper than the handler discharges; a guard dominating before a hop - call yields no finding - - _Requirements: 2.10, 3.8, 3.10_ - - _Boundary: obligations.check (opt-in only)_ +- [ ] 8. Stable symbols and conservative call resolution +- [ ] 8.1 Capture call receiver and arity evidence in the semantic IR + - Preserve receiver expression and argument count for supported syntax while keeping existing constructors valid. + - Done when language fixtures retain receiver and arity evidence without regressing existing IR consumers. + - _Requirements: 3.2, 3.3_ + - _Boundary: Semantic IR_ +- [ ] 8.2 Build stable declaration identities and the per-change symbol index + - Identify declarations by module, enclosing type, name and available signature. + - Cache the symbol and inheritance indexes on the per-change context. + - Done when duplicate type names, same-name methods and overloads receive stable distinct identities. + - _Requirements: 3.2, 3.5, 6.2_ + - _Boundary: Symbol Index_ - _Depends: 8.1_ +- [ ] 8.3 Resolve exact, finite-candidate and unresolved call targets + - Return complete exact targets, incomplete finite candidate sets, or unresolved results with reasons. + - Remove global bare-name fallback from prover-mode resolution. + - Done when ambiguity never merges methods and unresolved calls cannot produce complete paths. + - _Requirements: 3.3, 3.4, 11.1, 11.6_ + - _Boundary: Call Resolution_ + - _Depends: 8.2_ +- [ ] 8.4 Resolve inheritance and base-declaration attachment + - Attach base operations and entries only through repository-defined descendant relations. + - Preserve ambiguous inheritance as incomplete rather than projecting to unrelated routes. + - Done when subclass and unrelated-class fixtures produce distinct attachments and judgments. + - _Requirements: 3.5_ + - _Boundary: Call Resolution_ + - _Depends: 8.2, 8.3_ -- [ ] 9. Recogniser registry `[2026-10-29]` -- [ ] 9.1 `mapping/` package with a recogniser registry (Strategy pattern): registry table consulted by the - language dispatch in `mapping.py`; the registration-sites strategy lands first -- call-site handler - registration resolved through `resolution.class_table`, entries at the registered class's request-method - declarations with `registered_by` evidence, registration-site vocabulary carried as fact data (task 10), not - engine code; the recogniser returns unresolved registrations alongside the entries so the prover can count - them - - Done when `tests/test_mapping_registration_sites.py` shows a registration-site fixture (vocabulary from - data rows) yielding entries at the registered class's file with registration evidence, an unresolved - registration returned as such (no entry), `mapping.py`'s dispatch consults the registry, and the existing - mapping tests pass unchanged - - _Requirements: 1.9_ - - _Boundary: mapping_ - - _Depends: 7.2_ -- [ ] 9.2 Migrate the first legacy recogniser family (Stapler) from `mapping.py`'s inline blocks into a - `mapping/` strategy module, proving the migration path; remaining families migrate per the breadth map, not - this task - - Done when Stapler entries come from `mapping/stapler.py` through the registry with the existing Stapler - tests unchanged, and `mapping.py` contains no Stapler-specific regex - - _Requirements: 1.1_ - - _Boundary: mapping_ +- [ ] 9. Interprocedural summaries and concrete paths +- [ ] 9.1 Extract local function summaries + - Collect each function's operations, witnesses, resolved calls and local completeness without traversing callers. + - Done when summaries are deterministic and contain no target names outside fact identifiers. + - _Requirements: 3.1, 3.6, 11.7_ + - _Boundary: Function Summaries_ + - _Depends: 7.4, 8.3_ +- [ ] 9.2 Compute monotone summaries over recursive call components + - Iterate finite summary sets over strongly connected components until stable. + - Done when direct recursion and mutual recursion terminate with stable accumulated evidence. + - _Requirements: 3.7, 11.6_ + - _Boundary: Function Summaries_ + - _Depends: 9.1_ +- [ ] 9.3 Add summary caches and explicit exploration cutoffs + - Reuse summaries per change and carry depth, fan-out, deadline and other cutoff reasons into completeness. + - Done when each cutoff fixture returns accumulated evidence plus the exact incomplete reason. + - _Requirements: 3.8, 6.2, 6.3, 7.2_ + - _Boundary: Function Summaries, Context Cache_ + - _Depends: 9.2_ +- [ ] 9.4 Materialise exact evidence paths from summaries + - Emit concrete entry-to-operation hops only through exact target edges. + - Preserve every complete chain independently and retain candidate-edge diagnostics separately. + - Done when guarded and unguarded paths to one operation remain separate and candidate edges never complete a path. + - _Requirements: 3.9, 3.10, 11.4, 11.5_ + - _Boundary: Concrete Paths_ + - _Depends: 9.3_ -- [ ] 10. Fact initialization job `[2026-10-29]` -- [ ] 10.1 (P) `tools/fact_init.py`: the one-time initialization pass per target. Extraction mode walks the - legacy `mapping.py` blocks and current TOML rows and extracts embedded target vocabulary into the acquirable - structures. Proposal mode takes an LLM or maintainer proposal for a target's vocabulary (entry shapes, - registration sites, handler-name families, policy-decision constructs). The gate: every row passes the facts - header discipline (source, version, region) and engine verification admits it (the row must match what the - target's code says); only then promoted to a closed row - - Done when `tests/test_fact_init.py` shows: extraction mode recovers the vocabulary of one legacy family - into rows; a proposal matching a fixture repository is promoted; a proposal the fixture contradicts is - rejected with the reason; nothing lands in the TOML files without passing the gate - - _Requirements: 2.7_ - - _Boundary: tools.fact_init, ruleset/obligations (rows it produces)_ -- [ ] 10.2 First initialization run for the training pool's target families: produce the handler-name rows for - webhook/build-trigger and data-exposure shapes, the registration-site vocabulary, and the policy-decision - constructs, as data rows admitted through the gate (names verified against the pool clones; header updated) - - Done when the pool's gate-1 miss shapes (Stapler webhook/data-exposure handlers, programmatic registration, - policy voters) are all carried as rows with headers, no engine module names a target, and - `tests/test_obligation_facts.py` loads each family - - _Requirements: 2.7, 2.9, 2.10, 1.9_ - - _Boundary: ruleset/obligations_ - - _Depends: 10.1, 9.1, 8.1_ +- [ ] 10. Strict authorization judgment +- [ ] 10.1 Return abstract dominance relations without prover fallback + - Return MUST, MAY, NO or UNKNOWN with guard effect and control context. + - Keep legacy order dominance unchanged, but return UNKNOWN in prover mode for unavailable graphs or line mappings. + - Done when no prover fixture is discharged or flagged solely through textual-order fallback. + - _Requirements: 10.1, 10.2, 10.3, 10.4, 10.5, 10.6, 10.7_ + - _Boundary: CFG Dominance_ + - _Depends: 7.1_ +- [ ] 10.2 Match witness kind, scope and resource + - Apply request-global sufficiency only when the operation fact declares it. + - Return NO for definite mismatch and UNKNOWN for unresolved resource compatibility. + - Done when same-resource, alias, global, mismatch and unknown fixtures match the design algebra. + - _Requirements: 2.1, 2.2, 2.5, 2.6, 2.7, 11.1_ + - _Boundary: Witness Matcher_ + - _Depends: 7.2, 10.1_ +- [ ] 10.3 Match authority and promoted implications + - Apply only promoted authority implications and preserve their evidence. + - Return NO for insufficient authority and UNKNOWN when compatibility cannot be decided. + - Done when stronger, weaker, unrelated and unknown authorities produce the expected relations. + - _Requirements: 2.2, 2.5, 2.7, 2.8, 11.1_ + - _Boundary: Witness Matcher_ + - _Depends: 7.3, 10.1_ +- [ ] 10.4 Compute one judgment per complete or diagnostic path + - Conjoin witness dimensions, aggregate witnesses per obligation and apply the mixed-obligation rule. + - Emit discharged only for all-MUST, indeterminate for any MAY/UNKNOWN, and unguarded for at least one NO. + - Done when MUST/NO, MAY/NO, UNKNOWN and empty-witness fixtures match the specified truth table. + - _Requirements: 4.1, 4.2, 4.3, 11.2, 11.3, 11.4_ + - _Boundary: Pair Judgment_ + - _Depends: 10.2, 10.3_ +- [ ] 10.5 Aggregate multiple paths in the opt-in checker mode + - Return unguarded if any complete path is unguarded, discharged only for complete all-discharged enumeration, + and indeterminate otherwise. + - Keep the legacy checker API and defaults unchanged. + - Done when mixed guarded, unguarded and incomplete path sets produce the specified aggregate. + - _Requirements: 3.10, 4.1, 4.2, 4.3, 4.4, 4.5, 11.5_ + - _Boundary: Obligation Checker_ + - _Depends: 9.4, 10.4_ +- [ ] 10.6 Integrate three-way judgments into the prover + - Emit hunt findings only for unguarded pairs and send no indeterminate pair to the proof arm. + - Carry all judgments, completeness reasons, resources, authorities and stable identifiers in traces and coverage. + - Record stage-specific exceptions without folding them into quiet coverage. + - Done when end-to-end fixtures distinguish unguarded, discharged and indeterminate records and findings. + - _Requirements: 4.4, 4.5, 4.6, 4.7, 7.1, 7.2, 7.3, 7.4, 7.5, 7.6, 8.1, 8.2, 8.3, 9.1, 9.2, 9.3, 9.4, 9.5, 9.6, 9.7_ + - _Boundary: Prover Integration, Canonical Trace_ + - _Depends: 7.4, 9.4, 10.5_ -- [ ] 11. Prover resolution integration `[2026-10-29]` -- [ ] 11.1 Target enumeration joins callees by qualified key with a `down_depth` budget (default 2, sharing the - fan-out bound) so operations one call deeper are reached; the `callers` adapter keeps only callers whose - receiver binds to the target's class or subclass; unresolvable receivers fall back to the bare name and are - counted `receiver_unresolved`; unresolved registrations from mapping are counted `registration_unresolved` in - `Coverage` - - Done when `tests/test_hunt_prover.py` shows: an operation one call deeper than the handler is reached and - checked; a same-name method on another class yields a separate verdict (no cross-contamination); coverage - carries `receiver_unresolved` when a receiver does not resolve and `registration_unresolved` when a - registration target is outside the repository - - _Requirements: 3.7, 3.9_ - - _Boundary: hunt.prover_ - - _Depends: 7.1, 7.2, 9.1_ +- [ ] 11. Target knowledge registry and acquisition +- [ ] 11.1 (P) Add the entry-recognition strategy registry + - Route mapping dispatch through one registry without embedding target names in engine modules. + - Done when a fixture strategy registers, runs and records its strategy identifier and evidence. + - _Requirements: 1.1, 1.5, 1.7_ + - _Boundary: Mapping Registry_ + - _Depends: 7.1_ +- [ ] 11.2 Add the generic call-site registration strategy + - Resolve repository-defined registered handlers through stable symbols and return unresolved registration coverage. + - Done when exact and unresolved registration fixtures produce entries or coverage respectively. + - _Requirements: 1.2, 1.3, 1.4, 1.5, 1.6_ + - _Boundary: Registration Adapter_ + - _Depends: 8.4, 11.1_ +- [ ] 11.3 (P) Extract existing target knowledge into candidate records + - Read legacy recognition strategies and current facts without changing promoted outputs. + - Done when extraction produces deterministic candidate records with source/version/region evidence. + - _Requirements: 2.9_ + - _Boundary: Fact Initialization_ + - _Depends: 7.1_ +- [ ] 11.4 Verify and promote proposed target knowledge + - Accept source- or approved-documentation proposals, reject contradictions, and write only verified outputs. + - Done when matching proposals promote and contradicted or evidence-free proposals leave promoted knowledge unchanged. + - _Requirements: 2.9, 2.10_ + - _Boundary: Fact Initialization_ + - _Depends: 11.3_ +- [ ] 11.5 Record acquisition provenance and enforce label-isolated mode + - Persist input revision, evidence digest, accepted/rejected proposals and output digest. + - Reject admission acquisition inputs containing vulnerability, fix-location or ordinary-change labels. + - Done when changed output after labels are opened marks the population spent. + - _Requirements: 12.1, 12.2, 12.3_ + - _Boundary: Fact Initialization, Admission Guard_ + - _Depends: 11.4_ +- [ ] 11.6 Migrate one legacy recogniser through the registry + - Move one development-evidence family out of inline dispatch without changing its entries. + - Done when old fixtures stay stable and inline target-specific matching is removed for that family. + - _Requirements: 1.1, 1.7_ + - _Boundary: Mapping Registry_ + - _Depends: 11.1_ +- [ ] 11.7 Run the first label-blind development acquisition + - Produce registration, handler-operation, enforcement, resource and authority knowledge through the gate. + - Treat the output as development data and record its acquisition digest; do not encode names in engine modules. + - Done when promoted outputs load, rejected proposals have reasons, and the old unfinished task 3.2 has no residue. + - _Requirements: 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 2.10, 5.7, 12.9_ + - _Boundary: Target Knowledge_ + - _Depends: 10.3, 11.2, 11.5, 11.6_ -- [ ] 12. Arm and coverage `[2026-10-29]` -- [ ] 12.1 (P) Recognition or resolution exceptions inside `prove_change` are recorded under - `error:` reason keys in coverage, never folded into `framework_unrecognised` or any - other quiet reason - - Done when a fixture raising inside a recognition or resolution pass counts under `error:` and - `framework_unrecognised` stays empty for that fixture - - _Requirements: 7.3_ - - _Boundary: hunt.prover_ -- [ ] 12.2 (P) Stale-anchor refusal in `prover_arm._prove`: every returned finding's `path` is validated - against the files actually read; an absent path marks the record `instrument_failure` with reason - `stale_anchor` and findings cleared; `summarize` refuses such runs listing the record ids - - Done when `tests/test_prover_arm.py` shows a fixture finding on an absent path makes `_prove` mark the - record and makes `summarize` refuse, mirroring the zero-byte refusal - - _Requirements: 5.6_ - - _Boundary: prover_arm_ +- [ ] 12. Development and admission runners +- [ ] 12.1 Materialise and verify baseline and candidate analyzer bundles + - Resolve analyzer revisions, fact sets, acquisition records and configurations to immutable digest-verified inputs. + - Refuse comparison when any bundle artifact is unavailable or mismatched. + - Done when the immutable baseline and a fixture candidate bundle can be reconstructed exactly. + - _Requirements: 5.1, 5.5, 12.1_ + - _Boundary: Run Manifests_ +- [ ] 12.2 Add record provenance, stage funnel and judgment transitions + - Persist analyzer, fact, acquisition, configuration, population and input digests per record. + - Summarise every analysis stage, completeness reason and transition between compared judgments. + - Done when a fixture run accounts for every record from entry recognition through final judgment. + - _Requirements: 5.1, 5.3, 5.4, 7.1, 7.6, 9.7, 11.8_ + - _Boundary: Development Runner_ + - _Depends: 10.6, 12.1_ +- [ ] 12.3 Enforce instrument and hard runtime gates + - Preserve zero-byte and stale-anchor refusal and add stage-aware deadline records. + - Fail the run if any measured change exceeds 120 seconds; never summarize the overrun as a passing result. + - Done when zero-byte, stale-anchor, deadline and 121-second fixtures all refuse the summary. + - _Requirements: 5.6, 6.1, 6.3_ + - _Boundary: Runner Gates_ + - _Depends: 12.2_ +- [ ] 12.4 Register the four-arm development comparison + - Run baseline/candidate analyzer crossed with baseline/candidate facts over identical inputs. + - Report metric deltas, stage-funnel deltas and judgment transitions without admission language. + - Done when fixture arms isolate a fact-only lift from an analyzer-only lift. + - _Requirements: 5.2, 5.5, 5.7, 11.8_ + - _Boundary: Development Runner_ + - _Depends: 12.1, 12.2, 12.3_ +- [ ] 12.5 Consume and validate an externally reviewed admission manifest + - Accept only a manifest produced by valid-detection-benchmark with review, isolation and immutable digest fields. + - Reject label exposure, changed acquisition output or a spent population. + - Done when valid, malformed, exposed and spent manifests produce deterministic accept/refuse results. + - _Requirements: 12.1, 12.2, 12.3, 12.6, 12.8_ + - _Boundary: Admission Runner_ + - _Depends: 11.5, 12.3_ +- [ ] 12.6 Add paired scoring and the admission report + - Score vulnerable/fixed twins, reviewed ordinary changes, indeterminate rate, coverage, runtime and instruments. + - Preserve sample counts and uncertainty intervals and return NO-GO on any pre-registered gate failure. + - Done when fixture pairs detect vulnerable-only, fixed-side regression and mislabeled-negative cases. + - _Requirements: 5.2, 12.4, 12.5, 12.7, 12.8, 12.9_ + - _Boundary: Admission Runner_ + - _Depends: 12.5_ -- [ ] 13. Measurement after the amendment (maintainer, not Codex) `[2026-10-29]` -- [ ] 13.1 Re-run the arm on `benchmarks/valid/train/pool-train.toml` after tasks 7-12 land; write - `benchmarks/measurements/-access-control-prover-v2/` with NOTES, summary, coverage table; compare - against the 2026-10-28 gate 1 run (recall 65.2%, FA 15.0/100) on the same pool - - _Requirements: 5.2, 5.3, 7.2_ +- [ ] 13. Cross-cutting validation and measurements +- [ ] 13.1 Validate abstract-domain and metamorphic laws + - Cover the full join table, conjunction, witness aggregation, monotonicity and mixed-obligation rule. + - Prove that type renaming preserves a judgment and adding ambiguity can only preserve it or make it indeterminate. + - Done when property and fixture tests pass deterministically across repeated runs. + - _Requirements: 11.2, 11.3, 11.4, 11.5, 11.6, 11.7_ + - _Boundary: Abstract Evidence Validation_ + - _Depends: 10.5_ +- [ ] 13.2 (P) Validate cross-component analysis scenarios + - Exercise helper guards, registration entries, base attachment, resource mismatch, authority insufficiency, + ambiguous calls, unavailable CFGs, recursion and budget cutoff. + - Done when every scenario yields the expected trace, coverage reasons and three-way judgment. + - _Requirements: 1.1, 1.2, 1.3, 2.1, 2.2, 2.5, 2.7, 3.4, 3.5, 3.6, 3.7, 3.8, 4.1, 4.2, 4.3, 10.6_ + - _Boundary: Prover Integration Validation_ + - _Depends: 10.6, 11.7_ +- [ ] 13.3 Run the four-arm development regression + - Run all four registered arms on the immutable current development population after proving nonzero input reads. + - Publish analyzer/fact attribution, stage funnel, three-way judgments, budget result and comparison to the + 2026-10-28 baseline; label the result development-only. + - Done when all arm records and summary digests are complete and no admission claim appears. + - _Requirements: 5.1, 5.2, 5.3, 5.4, 5.5, 5.6, 5.7, 6.1, 7.3, 11.8, 12.9_ + - _Boundary: Development Measurement_ + - _Depends: 12.4, 13.1, 13.2_ +- [ ] 13.4 Run admission from an externally prepared untouched manifest + - Consume a reviewed manifest from valid-detection-benchmark after analyzer and facts are frozen. + - Verify label isolation, paired vulnerable/fixed behavior, reviewed ordinary labels and every admission gate. + - Done when the report returns an evidence-backed GO or NO-GO without modifying facts, strategies or thresholds. + - _Requirements: 12.1, 12.2, 12.3, 12.4, 12.5, 12.6, 12.7, 12.8, 12.9_ + - _Boundary: Admission Measurement_ + - _Depends: 12.6, 13.3_ -### Task constraints `[2026-10-29]` +## Task constraints -From `.kiro/steering/code-standards.md`, binding on every task above: +- Complexity: McCabe at most 10 per touched function, at most 50 logical lines per function and 400 per new module. +- Engine/target split: abstract-domain, resolution, summary, judgment and trace modules contain no target names. +- Target knowledge: names enter only through promoted facts or registered target-aware strategies. +- Compatibility: legacy checker defaults and completed baseline records remain unchanged. +- Instrument rule: validation must prove nonzero input reads before interpreting any clean or zero result. -- Complexity caps: McCabe <= 10 per function; <= 50 LLOC per function; <= 400 LLOC per new module. A task is - not done while a function it touched exceeds a cap; split the function. -- Pattern discipline: tasks 9.1-9.2 implement Strategy + Registry; task 10.1 implements the acquisition - pipeline behind the Interpreter discipline (rows are the language); task 11.1 is the Adapter at the - engine seam. New recognisers land in `mapping/` strategy modules, never as `mapping.py` blocks. -- Idiomatic naming: names state what a value semantically is in the pipeline vocabulary; collections name - their elements (`entry_point_records`, `judgments_by_key`); booleans are predicates; no abbreviations like - `eps`, `recs`, `d2`. +## Baseline implementation record - -## Implementation Notes - -- Delivery A (2026-10-14) implements paths, the opt-in checker premise, Stapler/Jetty/Servlet/JAX-RS - entries, the Java facts, the deterministic prover and the checkpointed arm. No commit was made. -- Task 3.2 stays open for the PHP, Python and TypeScript facts. Task 4.1's delivery A core is delivered; - its full-spec checkbox stays open for delivery B's enforcement witnesses and guarded Laravel acceptance - case. This delivery intentionally passes `extra_witnesses=()` as required by the maintainer's brief. -- Default checker behavior is preserved. Only opt-in checking includes a caller's statement witness, - using the existing dominance contract at the outgoing call site. The prover checks each complete path - independently so a guarded chain cannot hide an unguarded chain to the same operation. -- Java additions were checked against actual Git HEAD source objects in the sparse training clones; - checked call sites are named in the Java TOML header. No network or model call was made. -- Mapping accepts cached source texts and an opt-out from external manifest scanning. Default callers - retain their previous behavior; the delivery A prover uses source entries and its Context caches. -- Delivery A review was performed in the main context because the brief forbids model calls. The exact - requested static gate passed (format, Ruff and mypy); the exact pytest gate passed with 112 passed, - zero failed, exit 0. UV_NO_SYNC=1 was set; UV_CACHE_DIR was placed under /tmp because the default - cache is outside the writable sandbox. The unchanged unjustified-path checker test remains intact. - -- Delivery B (2026-10-14) implements task 2.2's Symfony, Livewire/Laravel, Remix and Tornado - entries, task 3.1's scoped enforcement witnesses, task 3.3's handler facts and operation discovery, - and task 4.1's integration. Changes remain uncommitted as the brief requires. -- Handler facts are explicitly opt-in through file-qualified handler maps in the checker. The prover - uses handler obligations where a Stapler or Tornado entry reaches no listed call operation; existing - call-site findings and Delivery A tests remain unchanged. Remix retains its handler operation even - when listed calls exist, and independently requires a path guard and an ownership check. Public - access waives only the path guard for these handler facts. The checker default is unchanged. -- The prover supplies a local dominance adapter for handler facts: it checks guards within the handler - body while reporting the operation at its declaration. A final ordinary return does not turn a bare - permission predicate into a guard. OrderDominance and the existing producers and arms are unchanged. -- Remix arrow exports are named locally in the prover's IR copy, including TSX route modules. Symfony - recognises positional and named route paths and class prefixes. Tornado recognises local subclasses - and the pool terminal's terminado base when it explicitly invokes Tornado's WebSocketHandler method. -- PHP CST Point.row access crashed on the larger Kimai controller with the installed native parser. - New recognisers derive line numbers from byte offsets instead; a fixture past line 320 and the - 23-change source smoke complete without a crash. Existing CST code was not modified. -- Task 3.2 remains partially complete: TypeScript adds clone-verified requireUserId and - authenticateApiRequest, retaining requireUser and authorize; PHP rows are retained and their header - records enforcement sources. Python retains the existing authenticated decorator and gains the - Tornado handler operation. No get_current_user fact was added: Git searches of Mage HEAD, the pool - revision and websocket fix 66440e4d3 found neither that API nor an authenticated decorator use, and - local framework documentation was unavailable. The brief forbids network access and unsourced names. -- Review used the main-context fallback because the brief prohibits model calls. Verdict: APPROVED - for tasks 2.2, 3.1, 3.3 and 4.1; task 3.2 remains open for its source-verification gap. No new - placeholder markers, credentials, dependencies, producer edits or arm edits were introduced. -- Fresh verification: UV_NO_SYNC=1 and UV_CACHE_DIR=/tmp/ousast-uv. The exact static gate passed: - ruff format --check ., ruff check ., mypy src/openultrasast (178 source files). The exact requested - pytest gate plus test_obligation_operations.py passed with 145 passed, zero failed, exit 0. - Initial missing-feature tests produced 24 failed and 14 passed; integration tests initially produced - eight failed and 20 passed. No test_search_* test was run. -- A separate file-scoped smoke read immutable Git source objects for all 23 access-control changes, - validated their commit objects and source digests, and recorded nonzero input bytes for every change. - 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. +- Deliveries A-C implemented the baseline paths, recognisers, witnesses, handler facts, prover, traces and CFG with + static checks and focused tests passing at delivery time. +- The full development arm then processed all 483 changes with zero instrument failures. Its maximum runtime exceeded + the amended hard budget, so the baseline is evidence, not an eligible arm. +- The 2026-10-28 ablation identified call resolution, resource/authority precision and failure visibility as the + amendment levers. Those observations inform tasks 7-13 but are not admission labels. diff --git a/.kiro/steering/breadth-map.md b/.kiro/steering/breadth-map.md index 669adf7..084a567 100644 --- a/.kiro/steering/breadth-map.md +++ b/.kiro/steering/breadth-map.md @@ -5,23 +5,24 @@ One screen: every feature's lane, its state today, and its next move. Aligns `.k | lane | state today | next move | owner | |---|---|---|---| -| Engine: obligation checker + dominance | Stable; target-agnostic; checker owns verdicts | All-kind caller-hop re-judgement (task 8.2, opt-in keyword) | access-control-prover | -| Engine: resolution | Designed (class table + receiver/signature-qualified calls); code not started | Task 7.2 `obligations/resolution.py` | access-control-prover | -| Engine: paths / CFG / trace | Stable; `PathRecord` shape kept by design | No change; resolution plugs in before them | access-control-prover | -| Prover integration | `hunt/prover.py` proves changes; caller join is name-keyed | Receiver-qualified target join + down-depth budget (task 11.1) | access-control-prover | -| Runner | `prover_arm.py` metrics, coverage, zero-byte refusal; gate 1 = 65.2% recall, 15.0 FA/100 | Stale-anchor refusal (task 12.2); re-measure after 7-12 (task 13) | access-control-prover | +| Engine: obligation checker + dominance | Baseline checker stable; amended three-way judgment and strict CFG relation designed | Abstract domain + strict opt-in judgment (tasks 7, 10); legacy defaults unchanged | access-control-prover | +| Engine: resolution | Stable-symbol and finite-candidate design approved; code not started | IR/symbol/call resolution tasks 8.1-8.4 | access-control-prover | +| Engine: summaries / paths / trace | Baseline concrete paths and traces stable; uncertainty is not yet first-class | Monotone summaries + exact path materialization (task 9), abstract trace fields (7.4) | access-control-prover | +| Prover integration | `hunt/prover.py` proves changes with name-keyed joins and binary outcomes | Three-way finding/trace/coverage integration (task 10.6) | access-control-prover | +| Runner | Baseline arm: 65.2% recall, 15.0 flagged ordinary pushes/100; max runtime exceeded the amended 120s hard budget, so it is development evidence, not an eligible arm | Bundle/funnel/gate/four-arm work (task 12), then development and admission runs (task 13) | access-control-prover | | Judge (zero-shot over traces) | `judge_pass.py`; gate 2 measured: safe but inert (keeps 15/15 TPs, drops 5/69 FAs) | No tuning; revisit only if trace facts change the FA mix | roadmap (measured 2026-10-28) | -| Recogniser registry | Designed (Strategy+Registry, `mapping/` package); code not started | Task 9.1 registry + registration-sites strategy; 9.2 migrates Stapler as the proof | access-control-prover | +| Recogniser registry | Strategy+Registry approved; code not started | Registry + registration adapter + one-family migration (tasks 11.1, 11.2, 11.6) | access-control-prover | | mapping.py monolith | All framework families inline (1,200+ lines); WordPress/Python registration blocks included | Migrate family by family after Stapler: jetty, symfony, livewire, remix, tornado, then PHP/Python registration tables | breadth (this map) | -| Obligation facts (ruleset TOMLs) | Closed rows, hand-authored; header discipline enforced by loader | Extraction into acquirable structures via fact-init (task 10.1) | access-control-prover | -| Fact initialization job | Designed (`tools/fact_init.py`: extract + propose -> gate -> promote); code not started | Task 10.1 build; 10.2 first run for pool families as data rows | access-control-prover | +| Obligation facts (ruleset TOMLs) | Closed rows, hand-authored; resource/authority algebra designed but not implemented | Resource/authority fields (tasks 7.2-7.3), label-blind development acquisition (11.7) | access-control-prover | +| Fact initialization job | Label-blind extraction/proposal/verification/promotion and acquisition record approved; code not started | Tasks 11.3-11.5 | access-control-prover | | Fact-proposal lane (standing) | Roadmap-level: LLM proposes, engine verifies, repetition promotes | Stays deferred to injection-spec track (roadmap gate 5) | roadmap | | Injection-family object | Brief only (`engine-change-scoped-analysis`); taint flow + banks MVP exist as evidence | Spec after post-fix pilot holds recall | roadmap | | Complexity gate | Caps in `code-standards.md`, review-time only | Wire ruff C901 / xenon into CI; threshold per steering | breadth (this map) | | Idiomatic naming | Rule active for new/amended code; legacy debt un inventoried | Record rename inventory during family migrations; no drive-by renames | breadth (this map) | -| Training pool | pool-train 23 repos / 483 changes frozen 2026-10-14 | Pre-2019 negatives re-audit before any future run (3/12 sampled carry real missing-check bugs) | valid-detection-benchmark | +| Development pool | pool-train 23 repos / 483 changes frozen 2026-10-14; explicitly not admission evidence | Four-arm regression only after tasks 7-12; pre-2019 negatives still require review | access-control-prover | +| Admission population | Not yet supplied; current pool is spent for development | `valid-detection-benchmark` prepares a reviewed untouched manifest; access-control-prover only consumes it (task 13.4) | valid-detection-benchmark | | Pre-push safety net | Implementation 67/79; wiring unchanged by this work | Unaffected until prover recall/FA hold at pilot | pre-push-safety-net | -Migration order for mapping.py families is deliberate: Stapler first (task 9.2 proves the registry path on +Migration order for mapping.py families is deliberate: Stapler first (task 11.6 proves the registry path on the family the pool exercises most), then one family per migration, each deleting its legacy block from `mapping.py` in the same change.