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

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's existing fields, OrderDominance, and the checker's existing decision rules (owned by authorization-obligations). Two extensions are allowed and owned here: the handler-named operation fields (handlers, framework) in the facts, and the assume_entries_protected keyword and the unguarded_path label (see the checker block below); default off, every existing checker test unchanged.
• The feature table, the DSPy and hunter arms, the ablation (hunter-learning-loop).
• The proof arm's demonstration logic (search-with-proof); this spec only shapes the finding.

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

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

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

@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.

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.

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).

trace: the ordered serialisation (owned here)

@dataclass(frozen=True)
class Guard: kind: str; scope: str; line: int | None; provenance: str; fact_id: str
@dataclass(frozen=True)
class Hop: function: str; call_line: int | None; guards_before_call: tuple[Guard, ...]; forwarded: tuple[str, ...]
@dataclass(frozen=True)
class Trace:
    entry_kind: str; boundary: str; access: str; parameters: tuple[str, ...]
    hops: tuple[Hop, ...]                     # entry first; the last hop holds the operation
    operation_kind: str; fact_id: str; operation_line: int
    arguments: tuple[tuple[str, str], ...]   # (argument text, provenance) in call order
    guards_after: tuple[Guard, ...]
    requires: tuple[str, ...]; dominating: tuple[str, ...]; missing: str | None
    def text(self) -> str: ...               # one component per line, in order
    def record(self) -> dict: ...            # canonical JSON

Argument provenance: within each hop's function, follow the IR's binds backwards from the operation's argument identifiers to the function's parameters or to a request-source fact (request_input), to an identity source (authenticated_context), or to a literal (constant); a parameter that the previous hop's call site fills from its own request-derived values keeps request_input; anything the walk cannot follow is unknown. No inter-procedural dataflow beyond the call sites on the path. The trace never carries language, framework, repository, size or count fields.

obligations.enforcement

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

@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 <sha256(change id)>.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.