spec(search-with-proof): requirements amended after two Codex reviews; design v2

False alarms count every visible finding; the verifier owns per-family oracles;
inconclusive on one-sided build failure; feasibility pilot separated from a
73-negative BLOCK qualification; coverage ceilings; spend reserved before calls;
key isolated from executed code; cluster model calls supersede the pool VM-only
rule for this arm only. Requirements approval reopened.

Co-Authored-By: Claude Opus 5.5 <[email protected]>

.kiro/specs/search-with-proof/design.md

@@ -0,0 +1,25 @@
+# Design: search with proof (v2, after two Codex reviews; the Claude Doc is the readable version)
+
+## Why: from scoring excerpts to proving findings
+BLOCK will mean a vulnerability was demonstrated and re-run by the system, not that a score passed a threshold. Every detection step so far classified one function excerpt, then tried to make the score precise enough to block. Same wall in every experiment: LLM programs (exp-005 A) within-pair AUC 0.762, pooled gate needs >=73 clean flags; trained logistic 0.721 (tie, CI spans zero); gradient boosting 0.597 (worse). Cairn (AGPL, design only) treats a security problem as directed search with a checkable goal. Three things follow: (1) objective goal: test/PoC fails on vulnerable, passes on fixed; needs no calibration or training data, so it carries over to unseen repos; (2) exploration with tools (read other files, follow callers, build, run); (3) search state: facts and intents accumulate on a board per search.
+
+## Architecture
+VM coordinates and is the only writer to the board (memory store); every model call and execution runs as an AX Task on kube-ax. Triage (quick rules, engine, classifier) -> top K candidates -> first facts on the board. Reason task (reads snapshot, returns complete or <=3 intents) <-> board; Explore tasks (one per intent; read, grep, run, write demo/; return one fact) <-> board; Verify task (fresh sandbox, planted canary, vulnerable vs fixed / head vs base) -> outcome: BLOCK only if demonstrated, else advisory or silent. Scheduler and budgets on the VM check caps before every dispatch. Tasks read/write via presigned links; store credentials stay on the VM. VM is fallback lane, kind local fallback, same image.
+
+## The demonstration contract (v2)
+The verifier, not the agent, observes the effect, on one side and not the other, consistently, in fresh sandboxes. Artefact: demo/ with build.sh and attack.sh (or a request file) touching only the documented external interface; its exit code and output are ignored. Oracles owned by the verifier per family: injection SQL = canary row seen in verifier's query log/response capture; path = canary file outside root read, seen by file-access watch; XSS = script executes in verifier's headless browser; SSRF = request arrives at verifier's in-sandbox listener; injection (command) = canary side effect seen by process watch. Deserialisation, access control, config/secrets: no owned oracle yet -> plausible_unproven at most. Attacker boundary excludes source tree, dependencies, runtime, fixtures; checkout and dependencies read-only during run; untracked files, dependency swaps, runtime patching refused. Differential: fix pair vulnerable-vs-fixed; push head-vs-base. Both sides must build and pass readiness independently; each side 3 runs from fresh state; inconsistent runs rejected; a side that fails to build or start => inconclusive, never a pass. Outcomes: demonstrated (BLOCK once the family is qualified), plausible_unproven (advisory, a visible finding), could_not_build/could_not_run/inconclusive (advisory if facts support, else silent; never "not vulnerable"), no_oracle (as plausible_unproven), no_evidence (silent). REGRESS's nonzero-exit-is-triggerable rule (regress/verdict.py) is not reused for proof; its sandbox plumbing is.
+
+## Agent worker and sandbox tools
+Own small tool loop in src/openultrasast/search/ via the existing OpenAI-compatible client (provider swappable, spend metered, Apache-2.0). Image ousast-search-task from the AX task runner, toolchains for Python, Node and TypeScript, PHP, Java; repo fetched over HTTPS. Tools: list_files, read_file (400 lines/call), grep (200 matches), run (per-call timeout, truncated output), write_demo (only write, under demo/), finish (one fact or recorded failure). Engine evidence (taint path, sinks, missing guards) is in the explore prompt. Reason step uses no tools.
+
+## Triage, budgets and model access (v2)
+Top K per push (K=3); candidate carries family hint + engine evidence as first facts. Caps (ceilings, not estimates): reason rounds 4/search, intents 3/round, explore 15 min/intent, $0.50/search, $1.50/push, 3 demos x 2 sides x 3 runs. Spend reserved before each model call at max cost and settled after (plane/budget.py gets a reservation step); per-task memory/disk/cleanup limits sized to workers (~3 vCPU, 5-5.75 GiB, two heavy lanes); total run wall-time and retry cap. Worst case 120 task-hours for 40 searches (~60 h on two lanes); a 1,300-change slice at K=3 could reach $1,950. First 3 pilot searches measure real cost; pilot ceiling set from that and asked for. Model key: operator scoped secret (AX injects only GEMINI_API_KEY; operator decides mechanism); never in manifest/log/board/record; repository code cannot read it: model client runs in a separate process as its own user.
+
+## Pilot, qualification, then the unseen pool (v2)
+1. Feasibility pilot: 20 dev-corpus pairs (never v3/pool), the four pool families with an owned oracle (injection, path, output encoding, untrusted destination), across the pool's five languages (Python, JS, TS, PHP, Java). Candidate = labelled function (measures proof, not triage); advantages recorded; fixed-side search never sees the vulnerable revision or its demo. Reported: demonstrated rate per family/language, false proofs, could_not_build/run/inconclusive/no_oracle rates, spend/tasks/wall. Exit: >=1 family with >=5 verified demonstrations and zero false proofs, else stop.
+2. BLOCK qualification per family: 0/20 still allows 16.1% (Wilson 95%); a family BLOCKs only after >=73 negative-side searches (fixed revisions + ordinary changes) with zero demonstrated (upper bound 5%, same bar as the pooled gate). Until then demonstrations show as advisories.
+3. G1 arm on the unseen pool: triage top K on every replayed change in a fresh slice; scored with the pool's rules on every visible finding incl. advisories, family + location match; 1/5/10% FA budgets beside classifier arms; adopted only under the no-regression rule. No evaluation label, fixing revision or evaluation board is ever an input to unseen search.
+Every run reports the coverage ceiling (true candidate x owned oracle x both sides runnable x genuine differential, build failures in the denominator) next to catch. Delayed results go via push/background.py and are scored separately from push-time results.
+
+## Decisions, risks and open questions
+Largest risk: environment failure caps the demonstrated rate. Risks: builds fail; agent games oracle (mitigated by re-run, canary, differential, tracked-file check); repo code misuses egress (gVisor; ask operator for no-egress verify class); cost (hard caps); minutes per search too slow for synchronous hook (decide product path after pilot). Open: operator key mechanism + no-egress class; own tool loop vs CLI agent; pilot go-ahead $20; how a minutes-long search reaches the pre-push user.

.kiro/specs/search-with-proof/requirements.md

@@ -57,13 +57,21 @@ known instead of restarting.
 #### Acceptance Criteria
 
 1. A demonstration is an executable artefact (test, script or request sequence) that the system, not the agent,
-   re-runs in a fresh sandbox: it fails (shows the vulnerable behaviour) on the vulnerable revision and passes on the
+   re-runs in fresh sandboxes. The **verifier observes the effect itself** through a per-family oracle it owns (for
-   fixed revision for a labelled pair; for a push it shows the behaviour on head (and not on base where the change
+   example a request log, a planted resource it watches, a browser execution check for XSS); the artefact's own exit
-   introduced it).
+   code or output is never the oracle.
-2. Only a re-verified demonstration counts as a demonstrated finding. The agent's own claim of success is never enough.
+2. Each family's oracle states the attacker boundary (what the artefact may touch: only the documented external
-3. Outcomes are recorded as `demonstrated`, `plausible_unproven` (evidence but no passing demonstration),
+   inputs of the code under analysis, never the verifier's fixtures, the source tree, dependencies or the runtime).
-   `could_not_build` / `could_not_run` (environment failures), or `no_evidence`; none of the failure outcomes is ever
+   Inputs are immutable during a run; untracked files, dependency replacement and runtime patching are refused.
-   reported as "not vulnerable".
+3. Differential: for a labelled pair the effect is observed on the vulnerable revision and not on the fixed one; for a
+   push, on head and not on base. Both sides must build and pass a readiness check independently; a side that fails
+   to build or start makes the result **inconclusive**, never a pass. Each side is run at least three times from fresh
+   state; inconsistent runs are rejected.
+4. Only a verified demonstration counts as `demonstrated`. Outcomes: `demonstrated`, `plausible_unproven`,
+   `could_not_build`, `could_not_run`, `inconclusive`, `no_oracle` (family without an owned oracle), `no_evidence`;
+   none of the failure outcomes is ever reported as "not vulnerable".
+5. Families without an owned oracle (for now: deserialisation, access control, configuration and secrets) can reach
+   `plausible_unproven` at most until an oracle is specified and reviewed.
 
 ### Requirement 4: Triage and budget
 
@@ -74,7 +82,9 @@ known instead of restarting.
 1. Candidates come from the existing layers (quick rules, engine, classifier scores); only the top K per push or per
    pair side are searched; K and the per-search and per-push budgets (model spend, task count, wall time) are
    configuration, enforced by the coordinator.
-2. Every search records its model spend, task count and wall time; a budget is never exceeded.
+2. Every search records its model spend, task count and wall time. Spend is **reserved before each model call** (the
+   call's maximum cost) and released after; wall time, memory, disk and retries are capped per task and in total; a
+   budget is never exceeded, including by calls in flight.
 3. Paid runs need the maintainer's budget go-ahead with a ceiling, as all paid steps do.
 
 ### Requirement 5: Model access in the cluster
@@ -85,19 +95,45 @@ known instead of restarting.
 
 1. The agents' model key is a scoped, budget-limited key provided by the operator inside the cluster (AX v0.3.1
    injects only `gemini-api-secret` as `GEMINI_API_KEY`; the design names the exact mechanism agreed with the
-   operator). Store credentials stay out of the cluster (presigned links, as today).
+   operator). Store credentials stay out of the cluster (presigned links, as today). For this arm, model calls inside
-2. The key never appears in a manifest, a log, a board entry or a record.
+   the cluster supersede `unseen-repo-evaluation` Req 4.4 (model calls on the VM); that boundary is unchanged for all
+   other arms. *(maintainer decision 2026-10-05: scoped key in the cluster)*
+2. The key never appears in a manifest, a log, a board entry or a record, and is not readable by the repository code
+   the sandbox executes (the model client and the executed code are separated).
 
-### Requirement 6: Pilot, then the unseen pool
+### Requirement 6: Feasibility pilot, false-proof qualification, then the unseen pool
 
-**User Story:** As the maintainer, I want to know quickly whether search with proof works before scaling it.
+**User Story:** As the maintainer, I want to know quickly whether search with proof works, and to admit BLOCK only on
+evidence that meets the 95% precision bar.
 
 #### Acceptance Criteria
 
-1. Pilot: about 20 known fix pairs across families and languages; for each, search runs on the vulnerable side and
+1. **Feasibility pilot** (amended 2026-10-05 after review): about 20 known fix pairs from development corpora. It
-   on the fixed side under the same budget. Reported: demonstrated rate on vulnerable sides, any demonstration on a
+   measures feasibility only and is reported as such: demonstrated rate on vulnerable sides, false proofs on fixed
-   fixed side (a false proof, which must be zero), environment-failure rate, spend and wall time per search.
+   sides, `could_not_build` / `could_not_run` / `inconclusive` / `no_oracle` rates, spend, tasks and wall time. Its
-2. Exit of the pilot: at least one family with demonstrations on vulnerable sides and zero false proofs; otherwise
+   advantages (known location, labelled family, runnable-project bias) are stated in the record. Fixed-side searches
-   the result is recorded and the arm is not scaled.
+   never receive the vulnerable revision or its demo.
-3. Then a registered G1 arm on the unseen-repo pool: catch rate at the pool's false-alarm budgets, with BLOCK only on
+2. Before any paid search, an infrastructure probe without model calls proves each owned oracle works inside a gVisor
-   demonstrated findings, compared with the classifier arms.
+   AX Task (database fixture for SQL, in-sandbox listener for SSRF, headless browser for XSS, file and process
+   watches), that the artefact cannot reach the observers directly, and records image size, RAM and the full
+   verification cost (up to 3 demos x 2 sides x 3 runs per search). Pilot exit: at least one family with at least 5 verified demonstrations on vulnerable sides and zero false proofs;
+   otherwise the result is recorded and the arm is not scaled.
+3. **BLOCK admission per family** (deferred until the pilot passes; not part of the first tasks) requires a false-proof
+   qualification. A **negative** is a search on code that should be safe: a fixed revision searched on its own (the
+   search never sees the vulnerable revision), or an ordinary change. A **false proof** is the verifier observing the
+   effect on that safe code, confirmed by adjudication (an ordinary-change alarm may be a real new bug and is
+   adjudicated before it counts either way). Qualification needs zero false proofs over at least 73 negatives drawn
+   from at least 73 distinct repositories, so the Wilson 95% upper bound on the false-proof rate per negative is at
+   most 5%. This bounds the false-proof rate, not precision among flags; precision is reported separately from the
+   pool. Repeated runs and repeated searches of one repository are one negative.
+4. **Coverage ceilings**: every run reports, separately, (a) the demonstrated ceiling: the share of vulnerable changes
+   with a true candidate selected, an owned oracle, both sides runnable and a genuine differential, build and run
+   failures in the denominator; and (b) the advisory ceiling: the share with a true candidate selected. Families
+   without an owned oracle (access control, deserialisation, configuration and secrets) have a demonstrated and BLOCK
+   ceiling of zero today; their advisory ceiling need not be zero.
+5. **G1 arm on the unseen pool**: scored with the pool's rules on **every visible finding** (BLOCK and advisory), with
+   its family and location match; catch at the 1%, 5% and 10% false-alarm budgets; compared with the classifier arms;
+   adopted only under the pool's no-regression rule on a fresh slice. No evaluation label, fixing revision or board
+   from evaluation searches is ever an input to unseen search.
+6. Delayed results (a search finishing after the push) reach the user through the existing background delivery and
+   are scored separately from results available at push time.

.kiro/specs/search-with-proof/spec.json

@@ -1,16 +1,16 @@
 {
   "feature_name": "search-with-proof",
   "created_at": "2026-10-05T12:00:00Z",
-  "updated_at": "2026-10-05T12:30:00Z",
+  "updated_at": "2026-10-05T15:00:00Z",
   "language": "en",
-  "phase": "requirements-approved",
+  "phase": "design-generated",
   "approvals": {
     "requirements": {
       "generated": true,
-      "approved": true
+      "approved": false
     },
     "design": {
-      "generated": false,
+      "generated": true,
       "approved": false
     },
     "tasks": {