From c3820e184cee6fe073c4a84b5d3b26bdd4e8b96f Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Mon, 5 Oct 2026 13:35:18 +0200 Subject: [PATCH] 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 --- .kiro/specs/search-with-proof/design.md | 25 +++++++ .kiro/specs/search-with-proof/requirements.md | 74 ++++++++++++++----- .kiro/specs/search-with-proof/spec.json | 8 +- 3 files changed, 84 insertions(+), 23 deletions(-) create mode 100644 .kiro/specs/search-with-proof/design.md diff --git a/.kiro/specs/search-with-proof/design.md b/.kiro/specs/search-with-proof/design.md new file mode 100644 index 0000000..fd01df7 --- /dev/null +++ b/.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. diff --git a/.kiro/specs/search-with-proof/requirements.md b/.kiro/specs/search-with-proof/requirements.md index 956cd58..4d7e3f2 100644 --- a/.kiro/specs/search-with-proof/requirements.md +++ b/.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 - fixed revision for a labelled pair; for a push it shows the behaviour on head (and not on base where the change - introduced it). -2. Only a re-verified demonstration counts as a demonstrated finding. The agent's own claim of success is never enough. -3. Outcomes are recorded as `demonstrated`, `plausible_unproven` (evidence but no passing demonstration), - `could_not_build` / `could_not_run` (environment failures), or `no_evidence`; none of the failure outcomes is ever - reported as "not vulnerable". + re-runs in fresh sandboxes. The **verifier observes the effect itself** through a per-family oracle it owns (for + example a request log, a planted resource it watches, a browser execution check for XSS); the artefact's own exit + code or output is never the oracle. +2. Each family's oracle states the attacker boundary (what the artefact may touch: only the documented external + inputs of the code under analysis, never the verifier's fixtures, the source tree, dependencies or the runtime). + Inputs are immutable during a run; untracked files, dependency replacement and runtime patching are refused. +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). -2. The key never appears in a manifest, a log, a board entry or a record. + operator). Store credentials stay out of the cluster (presigned links, as today). For this arm, model calls inside + 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 - on the fixed side under the same budget. Reported: demonstrated rate on vulnerable sides, any demonstration on a - fixed side (a false proof, which must be zero), environment-failure rate, spend and wall time per search. -2. Exit of the pilot: at least one family with demonstrations on vulnerable sides and zero false proofs; otherwise - the result is recorded and the arm is not scaled. -3. Then a registered G1 arm on the unseen-repo pool: catch rate at the pool's false-alarm budgets, with BLOCK only on - demonstrated findings, compared with the classifier arms. +1. **Feasibility pilot** (amended 2026-10-05 after review): about 20 known fix pairs from development corpora. It + measures feasibility only and is reported as such: demonstrated rate on vulnerable sides, false proofs on fixed + sides, `could_not_build` / `could_not_run` / `inconclusive` / `no_oracle` rates, spend, tasks and wall time. Its + advantages (known location, labelled family, runnable-project bias) are stated in the record. Fixed-side searches + never receive the vulnerable revision or its demo. +2. Before any paid search, an infrastructure probe without model calls proves each owned oracle works inside a gVisor + 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. diff --git a/.kiro/specs/search-with-proof/spec.json b/.kiro/specs/search-with-proof/spec.json index 64738ac..0e9813c 100644 --- a/.kiro/specs/search-with-proof/spec.json +++ b/.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": {