From 8de0c2732b625ddf4083cb4ac9da4999bfaa6376 Mon Sep 17 00:00:00 2001 From: Marius Ciepluch <11855163+norandom@users.noreply.github.com> Date: Wed, 7 Oct 2026 13:25:52 +0200 Subject: [PATCH] spec+docs(search-with-proof): record first cluster demonstration + fixed-side negative [skip ci] Feed the milestone back into the spec and steering. HANDOFF: the open "first demonstrated" question is RESOLVED -- xiaomusic (path, prefix-check-bypass) demonstrated on the vulnerable side (3/3 affected, 0/3 safe) and the blind fixed-side search produced 0 false proofs; pair total $1.22. Records the six-fix chain that enabled it (parity, verify-time-only, fair-share budget, served-root guidance, oracle prefix-bypass coverage, control-signal feedback) plus the keystone. tasks.md: implementation note; pilot (6.2/6.3) in progress. spec.json: pilot status. safety-net steering: proof-based BLOCK mechanism reached first execution-backed demonstration (feasibility-pilot scope, not release readiness; pilot exit + 73-negative qualification open; classifier stays triage). search README: status note. Payload-free; demos/boards stay gitignored. Co-Authored-By: Claude Opus 4.8 --- .kiro/specs/search-with-proof/HANDOFF.md | 38 ++++++++++++++++++- .kiro/specs/search-with-proof/spec.json | 13 +++++-- .kiro/specs/search-with-proof/tasks.md | 15 ++++++++ .kiro/steering/safety-net.md | 16 ++++++++ .../record.json | 30 +++++++++++++-- benchmarks/search/README.md | 9 +++++ 6 files changed, 114 insertions(+), 7 deletions(-) diff --git a/.kiro/specs/search-with-proof/HANDOFF.md b/.kiro/specs/search-with-proof/HANDOFF.md index 6ee5eae..82577c1 100644 --- a/.kiro/specs/search-with-proof/HANDOFF.md +++ b/.kiro/specs/search-with-proof/HANDOFF.md @@ -2,7 +2,43 @@ State at handoff, for resuming on the search problem and abstract interpretation. -## The one open question +## RESOLVED 2026-10-07 — the one open question is CLOSED: first cluster demonstration achieved + +The "first `demonstrated`" question below is answered. search-with-proof produced its first autonomous +`demonstrated` finding end to end on kube-ax, and a blind negative confirmed no false proof. + +- **Pair:** hanxi/xiaomusic (pilot pair 13), family `path`, vulnerability class **prefix-check bypass** + (`startswith(root)` without a trailing separator; the fix adds `os.sep`). Image `e2c8b460`. +- **Vulnerable side:** `demonstrated` — owned effect in 3/3 affected runs, 0/3 safe runs. $0.37, 55 calls. +- **Fixed side (blind negative, Req 6.3):** `inconclusive`, **0 false proofs**. $0.56, 85 calls. +- **Pair total:** $1.22. Record: `benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/`. + +**The original pair-6 both-sides-false was a TWO-part diagnosis, both now fixed:** the demo did not reach the +observable (demo/agent), and — the decisive one — the path oracle only modelled **classic parent traversal** while +many real path CVEs (xiaomusic included) are **prefix-bypass**, which reaches a sibling that string-extends the served +dir, not the parent. The oracle now also plants a prefix-sibling canary. + +**Fix chain that enabled the demonstration (each merged to main and validated by a paid run):** +1. Parity — agent is told the observable's location (path oracle reached parity with command/ssrf). +2. Verify-time-only — the observable is injected at verify time and absent during exploration; stop the explore-time + reachability trap that burned budget without authoring a demo. +3. Fair-share pilot budget — each search gets a fair share of `--ceiling-usd` with rollover, so one expensive search + no longer starves the rest. +4. Served-root guidance — the demo MUST set the app's served directory to the `${served_root}` placeholder. +5. Oracle prefix-bypass coverage — plant a sibling canary for the `startswith`-without-separator class. +6. Control-signal feedback — the keystone control (does the app serve `${served_root}`?) is fed back to the agent as a + `served-root` hint so it self-corrects its wiring. This was the decisive last step. + +**Keystone (honest measurement), merged earlier:** the verifier runs a benign positive control; a broken or mis-wired +app yields `could_not_run`/annotation, never a silent clean-looking `inconclusive`. + +**Next toward the pilot exit (Req 6.2):** fan out the path family to ≥5 demonstrations with 0 false proofs, then the +≥73-negative BLOCK qualification (Req 6.3). The glance pair (classic traversal) also demonstrates once its npm +dependency build-break (`filed`→`mime@4`) is pinned. + +--- + +## The one open question (HISTORICAL — resolved above) The full chain runs end to end on kube-ax. Every execution layer is cleared. The **first `demonstrated` has not happened yet**, and the remaining gap is narrow and reproducible at **$0 model cost** via `demo_replay`. diff --git a/.kiro/specs/search-with-proof/spec.json b/.kiro/specs/search-with-proof/spec.json index 7ca3530..2a75c39 100644 --- a/.kiro/specs/search-with-proof/spec.json +++ b/.kiro/specs/search-with-proof/spec.json @@ -1,7 +1,7 @@ { "feature_name": "search-with-proof", "created_at": "2026-10-05T12:00:00Z", - "updated_at": "2026-10-05T15:30:00Z", + "updated_at": "2026-10-07T13:30:00Z", "language": "en", "phase": "tasks-generated", "approvals": { @@ -18,5 +18,12 @@ "approved": false } }, - "ready_for_implementation": false -} + "ready_for_implementation": false, + "pilot": { + "status": "in_progress", + "first_cluster_demonstration": "2026-10-07", + "pair": "xiaomusic (path, prefix-bypass)", + "false_proofs": 0, + "exit_remaining": "path family >=5 demonstrations / 0 false proofs (Req 6.2), then >=73-negative BLOCK qualification (Req 6.3)" + } +} \ No newline at end of file diff --git a/.kiro/specs/search-with-proof/tasks.md b/.kiro/specs/search-with-proof/tasks.md index 8af56de..f33abcf 100644 --- a/.kiro/specs/search-with-proof/tasks.md +++ b/.kiro/specs/search-with-proof/tasks.md @@ -113,3 +113,18 @@ gates, runs every networked or paid step. Ruff and changed-source mypy pass; audit: 166 load-bearing, six standalone, zero orphaned. No network or commits. The requested main merge could not update read-only Git metadata; HEAD and main had identical file trees. Live AX/Docker executor smoke and oracle probes remain unmeasured. + +- **FIRST CLUSTER DEMONSTRATION (2026-10-07) — pilot is live (6.2/6.3 in progress).** search-with-proof produced its + first autonomous `demonstrated` finding end to end on kube-ax: pair 13 (hanxi/xiaomusic, path, prefix-check-bypass + class), vulnerable side `demonstrated` (3/3 affected, 0/3 safe, $0.37), fixed side blind negative `inconclusive` + with 0 false proofs ($0.56); pair total $1.22, image e2c8b460. Record: + `benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/`. This closes the handoff's open question. + The infra probe (3.2) passed earlier; the pilot (6.x) has run many times. Enabling fix chain, each merged + paid-run + validated: (1) parity (name the observable to the agent), (2) verify-time-only (observable injected at verify time, + absent in exploration — ends the explore reachability trap), (3) fair-share pilot budget (no starvation across + searches), (4) served-root guidance (demo MUST serve `${served_root}`), (5) oracle prefix-bypass coverage (sibling + canary for `startswith`-without-separator path traversal), (6) control-signal feedback (served-root hint so the + agent self-corrects wiring). Plus the keystone (positive control → `could_not_run`, never a silent clean-looking + `inconclusive`). NEXT: fan out the path family to ≥5 demonstrations / 0 false proofs (6.2 exit), then the + ≥73-negative BLOCK qualification (6.3). glance (classic traversal) also demonstrates once its npm `filed`→`mime@4` + build-break is pinned. diff --git a/.kiro/steering/safety-net.md b/.kiro/steering/safety-net.md index 1d5e68e..0048415 100644 --- a/.kiro/steering/safety-net.md +++ b/.kiro/steering/safety-net.md @@ -142,3 +142,19 @@ promising but does not qualify security queries or hook latency. The contributor vendor/correspondence completeness vetoes, and query-to-operation identity as the next shared-contract work. Resolving a boundary requires evidence of its relevance and scope; do not simply drop completeness checks to increase admissions. Rollout remains NO-GO. + +On 2026-10-07, the **search-with-proof** arm reached its first milestone: an autonomous, +execution-backed `demonstrated` finding end to end on the kube-ax cluster. On a real CVE +fix-pair (hanxi/xiaomusic, path traversal of the prefix-check-bypass class), the agent +found the vulnerability, authored a declarative demo, and the differential verifier +confirmed the owned effect on the vulnerable revision and its absence on the fixed one; +a blind search of the fixed revision produced zero false proofs. This is the proof-based +BLOCK mechanism the maintainer directed after classification hit a precision wall: a BLOCK +rests on a demonstrated finding with a direct execution trace, not a confidence score. +Scope note: this is feasibility-pilot evidence on a development-corpus pair (known location, +labelled family, runnable-project selection bias), not release readiness. The pilot exit +(≥5 demonstrations in one family with 0 false proofs, Req 6.2) and the ≥73-negative BLOCK +qualification (Req 6.3) remain open, and no capability is enabled. The decision/classification +engine is retained as a triage ranker (it could not prove 95% precision as a gatekeeper); +proof is the BLOCK gate. See `search-with-proof/HANDOFF.md` and +`benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/`. diff --git a/benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/record.json b/benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/record.json index d7cca32..d9cb020 100644 --- a/benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/record.json +++ b/benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/record.json @@ -1,6 +1,12 @@ { "record": "2026-10-07 FIRST CLUSTER DEMONSTRATION for search-with-proof", - "pair": {"index": 13, "repo": "hanxi/xiaomusic", "family": "path", "class": "prefix-check-bypass (startswith without separator)", "language": "python"}, + "pair": { + "index": 13, + "repo": "hanxi/xiaomusic", + "family": "path", + "class": "prefix-check-bypass (startswith without separator)", + "language": "python" + }, "image": "ghcr.io/norandom/ousast-search-task@sha256:e2c8b460...", "side": "vulnerable", "outcome": "demonstrated", @@ -18,5 +24,23 @@ "served-root guidance: wire the served dir to ${served_root}", "oracle prefix-bypass coverage: sibling canary for startswith-without-separator vulns", "control-signal feedback: served-root hint so the agent self-corrects wiring" - ] -} + ], + "both_sides": { + "vulnerable": { + "outcome": "demonstrated", + "settled_usd": 0.3686, + "verify_tasks": 18, + "model_calls": 55 + }, + "fixed_blind_negative": { + "outcome": "inconclusive", + "false_proof": false, + "settled_usd": 0.5632, + "verify_tasks": 18, + "model_calls": 85, + "note": "Agent searched the FIXED (safe) revision blind (no vuln knowledge); authored demos but the verifier found no effect -> no false proof (Req 6.3 negative)." + }, + "pair_total_settled_usd": 1.224, + "verdict": "True positive on the vulnerable revision, zero false proof on the fixed revision." + } +} \ No newline at end of file diff --git a/benchmarks/search/README.md b/benchmarks/search/README.md index 12271f8..d0ef55e 100644 --- a/benchmarks/search/README.md +++ b/benchmarks/search/README.md @@ -131,3 +131,12 @@ manifest; without a subtype verification returns `no_oracle`. No subtype is gues from repository names. The selected manifest's pair 1 currently lacks this metadata. Live transport, provider authentication/cost, real project buildability, and AX oracle operation must still be measured; an offline probe cannot establish them. + +## Status (2026-10-07) + +The feasibility pilot achieved its first cluster `demonstrated` finding (xiaomusic, path / +prefix-check-bypass): vulnerable side demonstrated, fixed side blind search produced no +false proof. See `benchmarks/measurements/2026-10-07-search-first-cluster-demonstration/`. +Outcomes and spend are aggregates only; stored demos and boards stay in the gitignored +`benchmarks/search/private/` area. Pilot exit (≥5 demonstrations / 0 false proofs per +family) and the ≥73-negative BLOCK qualification remain open.