From 74a529825de3d4c23f2d1cb06b80fa77964f1901 Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Wed, 14 Oct 2026 15:51:25 +0200 Subject: [PATCH] spec: access-control prover (requirements, gap analysis, design, tasks) A deterministic check that a protected operation is reachable from an entry point without a check dominating the path, per framework, built on the existing obligations checker, caller index and entry mapper; scored as a rule arm on the access-control training pool. Follows the maintainer's finding that the hunter's features describe shape and cannot decide unsafety. Co-Authored-By: Claude Fable 5.1 --- .kiro/specs/access-control-prover/design.md | 226 ++++++++++++++++++ .../access-control-prover/requirements.md | 172 +++++++++++++ .kiro/specs/access-control-prover/research.md | 128 ++++++++++ .kiro/specs/access-control-prover/spec.json | 15 ++ .kiro/specs/access-control-prover/tasks.md | 69 ++++++ 5 files changed, 610 insertions(+) create mode 100644 .kiro/specs/access-control-prover/design.md create mode 100644 .kiro/specs/access-control-prover/requirements.md create mode 100644 .kiro/specs/access-control-prover/research.md create mode 100644 .kiro/specs/access-control-prover/spec.json create mode 100644 .kiro/specs/access-control-prover/tasks.md diff --git a/.kiro/specs/access-control-prover/design.md b/.kiro/specs/access-control-prover/design.md new file mode 100644 index 0000000..36afee1 --- /dev/null +++ b/.kiro/specs/access-control-prover/design.md @@ -0,0 +1,226 @@ +# 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, 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. + +### 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. +- Coverage stated per repository: what was recognised, reached, checked, and left unchecked by reason. + +### 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). + +## Boundary Commitments + +### This Spec Owns +- Entry recognisers for Stapler, Jetty handlers, Symfony attributes, Livewire and Laravel controllers, Remix + exports, Tornado handlers (`mapping.py` blocks, each with evidence). +- `semantic/obligations/paths.py`: `PathRecord` and `compose_paths` over the caller index. +- `semantic/obligations/enforcement.py`: router and decorator witnesses from route files and attributes. +- `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`. + +### Out of Boundary +- The facts loader and schema, the checker's decision rules, `OrderDominance` (owned by `authorization-obligations`). +- 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. + +### 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`. +- No new third-party dependency. + +### Revalidation Triggers +- A change to `EntryPointRecord` fields or `Discharge` scopes. +- A change to the replay record shape `benchmarks.valid.metrics` scores. +- A change to the hunt defect shape (`defect_from`). + +## 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. + +### Architecture Pattern & Boundary Map +```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] --> C + P --> PA[obligations.paths.compose_paths] + P --> EN[obligations.enforcement.witnesses] + PA --> CK[obligations.check.check_obligations] + EN --> CK + F[ruleset/obligations/*.toml\noperations, dischargers] --> CK + CK --> P + P --> R[benchmarks/valid/prover_arm.py\nrecords, metrics, coverage] + 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. + +### 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 | + +## File Structure Plan +``` +src/openultrasast/ +├── mapping.py # + recognisers: _stapler_entries, _jetty_entries, _symfony_entries, +│ # _livewire_entries, _remix_exports (extend), _tornado_entries +├── semantic/obligations/ +│ ├── 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 +benchmarks/valid/prover_arm.py # run / summarize; records per change; coverage table +tests/test_mapping_frameworks.py, tests/test_obligation_paths.py, tests/test_obligation_enforcement.py, +tests/test_hunt_prover.py, tests/test_prover_arm.py +``` + +### Modified Files +- `src/openultrasast/mapping.py`: new recogniser blocks, registered where `analyze_entry_points` dispatches by + language and path; `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. + +## 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. + +## Requirements Traceability +| Requirement | Components | +|---|---| +| 1.1-1.8 | mapping recognisers | +| 2.1-2.7 | enforcement.witnesses, facts rows, checker (existing) | +| 3.1-3.6 | paths.compose_paths | +| 4.1-4.6 | hunt.prover.prove_change | +| 5.1-5.5 | prover_arm | +| 6.1-6.2 | prover_arm timing, Context caches | +| 7.1-7.2 | Coverage in prove_change, prover_arm summary | +| 8.1-8.2 | finding shape in prove_change | + +## 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 | + +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`. + +### 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 + +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.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. + +### 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 + +@dataclass(frozen=True) +class ProverResult: findings: tuple[dict, ...]; coverage: Coverage; degradations: tuple[dict, ...] + +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 their direct callees that hold a protected operation (one hop down through + the IR's calls and the call index). +- 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`. + +### 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. + +## Error Handling +- Exceptions inside `prove_change` per file are recorded as `unchecked_by_reason[type name]`; 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). + +## 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. +- 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. +- Runner: a two-change fixture pool produces records the metrics summarise; a zero-byte read refuses. diff --git a/.kiro/specs/access-control-prover/requirements.md b/.kiro/specs/access-control-prover/requirements.md new file mode 100644 index 0000000..c7c052e --- /dev/null +++ b/.kiro/specs/access-control-prover/requirements.md @@ -0,0 +1,172 @@ +# 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. + +## 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. + +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`. + +## 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); 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`). +- **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. + +## 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. + +#### 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. + +### 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. + +#### 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. +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. + +### 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. + +#### 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. + +### 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. + +#### 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. +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. + +### 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. + +#### 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. + +### 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. + +#### 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. + +### 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. + +#### 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. + +### 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. + +#### 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. diff --git a/.kiro/specs/access-control-prover/research.md b/.kiro/specs/access-control-prover/research.md new file mode 100644 index 0000000..989ba2b --- /dev/null +++ b/.kiro/specs/access-control-prover/research.md @@ -0,0 +1,128 @@ +# Research & Design Decisions + +## Summary +- **Feature**: `access-control-prover` +- **Discovery Scope**: Extension of `authorization-obligations` (checker, facts, dominance) and the hunter's + per-change context; gap analysis against the code on 2026-10-14 (commit 9feb8f1). +- **Key Findings**: + - The checker already takes `paths` and `entries` and already decides reached-ness and along-path dominance + (`semantic/obligations/check.py::_reached`, `dominance.py::_dominates_along`); nothing supplies paths today, + so every operation outside an entry handler is invisible to it. + - The entry-point mapper (`mapping.py`) recognises Flask, Django, Express, Laravel routes, WordPress hooks, + Next and Remix route modules partially, and nothing for Java: no Stapler `doXxx` web method, no Servlet or + Jetty handler, no JAX-RS resource. Seventeen of the pool's 23 fixes are Stapler web methods. + - The hunter's `Context` (hunt/producers.py) caches product files, texts, file IR, a call index and the + repository's entry points per change; `source.callers_of` gives one hop of callers from the index. A bounded + upward walk from a function to an entry point is a loop over that, no new index. + - Enforcement outside the function fits the existing `Discharge` scopes `router` and `decorator`, which + `OrderDominance.dominates` accepts without a line, through the checker's `extra_witnesses` parameter. No + schema change to the facts loader is needed for them; the facts files gain operation rows only. + - `benchmarks/valid/metrics.py` scores replay-shaped records with `benchmarks.unseen.score`; the hunter arm + (`benchmarks/valid/hunter_arm.py`) writes that shape. A prover arm writing the same shape is scored by the + same code, so its recall and false alarms per 100 stand beside the hunter arms. + - The pool's fixes by shape: 17 Jenkins web methods (`doTestConnection`, `doFill...Items`, `doCheck...`, + `doValidate...`, `doChangeSubmit`, `doNotifyCommit`, `doPython`, `persistValue`, `create`) missing + `checkPermission`; one Jetty service without authentication (CWE-306); one Tornado terminal websocket open + without authentication (CWE-306); one Laravel Livewire `store` without authorization (CWE-285); one Symfony + controller action (CWE-284); one Remix action deactivating a schedule by id without an ownership check + (CWE-639); one Flarum JavaScript extension (CWE-863, out of reach for this prover: client-side permission + gating, counted as uncovered). + +## Research Log + +### Which checker parameters exist and what they expect +- **Context**: avoid a second checker. +- **Sources Consulted**: `src/openultrasast/semantic/obligations/check.py` (`check_obligations`, `_reached`, + `_relevant`), `dominance.py` (`OrderDominance`, `_dominates_along`, `_hop_index`), the approved design of + `authorization-obligations` (Dominance, Checker, EntryPoints sections). +- **Findings**: `paths` is a sequence of objects with a `hops` attribute; each hop is `"path::function"` or a + `(node, line)` pair; a path reaches an operation when its last hop equals `f"{op.path}::{op.function}"`. With + no paths, only operations inside entry handlers (`entries`) are reached. A witness of scope `hop` on an + earlier hop dominates along the path. Witness scopes `decorator` and `router` dominate without a line. +- **Implications**: the prover produces `PathRecord(hops=(...))` objects ending at the operation's function and + passes them as `paths`; it produces router and decorator witnesses as `extra_witnesses`; it needs no change to + the checker's logic. One gap: the checker builds `operations` from the IRs it is given, so the prover passes the + IR of every file on a path, not only the touched file. + +### Where entry points come from +- **Sources Consulted**: `src/openultrasast/mapping.py` (`analyze_entry_points`, `_entry`, the per-framework + recognisers around lines 260-930), `EntryPointRecord` fields. +- **Findings**: recognisers are code, one block per framework, each calling `_entry(target, start, end, handler, + name, kind, access, trust_boundary, evidence, conditions, ...)`. No Java recogniser exists. `frameworks.toml` is + a lexicon for priors and stratification, not for entry recognition. +- **Implications**: add recognisers in `mapping.py` following the existing block pattern (Stapler, Jetty, + Symfony attributes, Livewire, Tornado, Remix exports where missing). Each names its evidence. + +### How a rule arm is scored +- **Sources Consulted**: `benchmarks/valid/metrics.py` (`summarize`, `scoring_records`), `benchmarks/unseen/score.py` + (`catches`, `location_match`, `false_alarm`, `coverage`), `benchmarks/valid/hunter_arm.py` (`run`, record + writing), `src/openultrasast/hunt/metric.py::search_outcome`. +- **Findings**: a record needs `id`, `kind`, `repo`, `family`, the change's `path`/`function_lines` (copied from + the pool), `findings` with `path`, `line`, `family`, and `coverage` fields the scorer reads; a push is caught + when a finding of the change's family lands within the tolerance of a verified location. +- **Implications**: the prover arm copies the hunter arm's record envelope and instrument fields (bytes read per + changed file, head verified), writes per-change files, and calls `benchmarks.valid.metrics.summarize`. + +### Budget +- **Findings**: the second screen's feature table took 53 minutes for 483 changes with every producer, 7 seconds + per change on average and 117 seconds for the slowest seatunnel change; the caller index is the dominant cost + and is already cached per change. A depth-3 upward walk adds a few index lookups per function. +- **Implications**: the 120-second bound of Requirement 6 is realistic; the runner measures it per change. + +## Architecture Pattern Evaluation + +| Option | Description | Strengths | Risks / Limitations | Notes | +|---|---|---|---|---| +| Extend the checker's inputs (chosen) | Supply paths, entries and witnesses to `check_obligations` from the hunter's context | One checker, one dominance rule, facts stay closed data | Order dominance is textual inside a function; nesting-aware dominance (`guard-dominance-regime`) never existed | Honest for "check present before operation"; the Jenkins shape | +| New prover module with its own graph | Build a call graph and CFG per change | Precise dominance | Weeks of work, duplicates the checker, no CFG for Java or PHP in the tree | Rejected for this increment | +| Joern engine | Dataflow and call graph from the engine | Precise | 225 s per batch, pilot produced no findings, no PHP in the budget | Rejected as the gate; usable later as a proof backend | + +## Design Decisions + +### Decision: paths from the caller index, not a call graph +- **Context**: Requirement 3. +- **Alternatives Considered**: a per-change call graph over all product files; the engine's call graph. +- **Selected Approach**: an upward walk from the function through `source.callers_of` on the cached index, + bounded by depth and fan-out, stopping at the first entry point of each chain. +- **Rationale**: the index exists, is cached per change, and the pool's shapes are shallow (the operation is in the + web method or one helper below it). +- **Trade-offs**: name-based caller resolution conflates same-named functions across files; chains are kept per + file but a caller of `save` in another class may be a false hop. Accepted and visible in the evidence. +- **Follow-up**: measure how many positives are reached at depth 1, 2 and 3 on the pool. + +### Decision: framework enforcement as router and decorator witnesses +- **Context**: Requirement 2. +- **Selected Approach**: a small recogniser per framework reads route registrations and attributes and emits + `Discharge` witnesses with scope `router` or `decorator` for the handlers they cover; passed through + `extra_witnesses`. +- **Rationale**: the dominance rule already accepts those scopes; the facts files stay about calls. +- **Trade-offs**: coverage is as wide as the recognisers; an unrecognised middleware name means a finding on a + guarded route. Every recogniser lists its names in the facts header and the coverage statement counts routes + with unrecognised middleware. + +### Decision: no model call inside the prover +- **Context**: Requirement 4.4; the maintainer's direction after the engine pilot: the model's job is the trust + boundary question the static side cannot answer, asked after a static result exists. +- **Selected Approach**: the prover is deterministic; the intent adjudication hook of the checker stays off in + the arm; a later increment may wire it as a separate, measured arm. + +## Risks & Mitigations +- Jenkins web methods whose protected operation is an outbound connection test with stored secrets + (`doTestConnection`) call no listed operation name — mitigate by adding operation rows for credential + lookups and HTTP client calls used in those handlers, checked in the clones, and by counting the handlers the + facts do not cover. +- Textual order dominance inside a function misses a check in an `else` branch — accepted for this increment; + recorded as a degradation when a witness exists but does not dominate. +- Same-name conflation in callers — chains kept per file; evidence names the hop files. +- Over-wide entry recognition (every `doXxx`) raises false alarms on helper methods — the Stapler recogniser + requires a public method on an exposed type or a Stapler-typed parameter; the pool's ordinary pushes measure + the rate. + +## References +- Jenkins AccessControlled: https://javadoc.jenkins.io/hudson/security/AccessControlled.html +- Stapler web methods: https://www.jenkins.io/doc/developer/security/form-validation/ and + https://www.jenkins.io/doc/developer/security/secrets-and-credentials/ +- Laravel authorization and route middleware: https://laravel.com/docs/authorization, https://laravel.com/docs/middleware +- Symfony security: https://symfony.com/doc/current/security.html +- Remix route module API: https://remix.run/docs/en/main/route/action +- Tornado authentication: https://www.tornadoweb.org/en/stable/guide/security.html diff --git a/.kiro/specs/access-control-prover/spec.json b/.kiro/specs/access-control-prover/spec.json new file mode 100644 index 0000000..a1812a9 --- /dev/null +++ b/.kiro/specs/access-control-prover/spec.json @@ -0,0 +1,15 @@ +{ + "feature_name": "access-control-prover", + "created_at": "2026-10-14T13:48:18Z", + "updated_at": "2026-10-14T13:48:18Z", + "language": "en", + "phase": "tasks-generated", + "approvals": { + "requirements": {"generated": true, "approved": true}, + "design": {"generated": true, "approved": true}, + "tasks": {"generated": true, "approved": true} + }, + "ready_for_implementation": true, + "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)" +} diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md new file mode 100644 index 0000000..d3209d7 --- /dev/null +++ b/.kiro/specs/access-control-prover/tasks.md @@ -0,0 +1,69 @@ +# Implementation Plan + +- [ ] 1. Paths from the caller index +- [ ] 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_ + +- [ ] 2. Entry recognisers +- [ ] 2.1 Stapler and Jetty recognisers in `mapping.py` (P) + - Public `do[A-Z]...` methods on exposed types or with Stapler-typed or `@QueryParameter` parameters; Jetty + `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_ +- [ ] 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_ + +- [ ] 3. Enforcement witnesses and facts +- [ ] 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_ + +- [ ] 4. The prover +- [ ] 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_ + +- [ ] 5. The arm +- [ ] 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_ + +- [ ] 6. Measurement (maintainer, not Codex) +- [ ] 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_