Open_Ultra_SAST/.kiro/specs/access-control-prover/requirements.md

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:<operation kind>:<path>:<line>:<missing> as the checker already emits.