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 <[email protected]>
This commit is contained in:
Marius Ciepluch
2026-10-07 13:25:52 +02:00
co-authored by Claude Opus 4.8
parent ecd1372568
commit 8de0c2732b
6 changed files with 114 additions and 7 deletions
+37 -1
View File
@@ -2,7 +2,43 @@
State at handoff, for resuming on the search problem and abstract interpretation. 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 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`. happened yet**, and the remaining gap is narrow and reproducible at **$0 model cost** via `demo_replay`.
+10 -3
View File
@@ -1,7 +1,7 @@
{ {
"feature_name": "search-with-proof", "feature_name": "search-with-proof",
"created_at": "2026-10-05T12:00:00Z", "created_at": "2026-10-05T12:00:00Z",
"updated_at": "2026-10-05T15:30:00Z", "updated_at": "2026-10-07T13:30:00Z",
"language": "en", "language": "en",
"phase": "tasks-generated", "phase": "tasks-generated",
"approvals": { "approvals": {
@@ -18,5 +18,12 @@
"approved": false "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)"
}
}
+15
View File
@@ -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. 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 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. 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.
+16
View File
@@ -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 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; 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. 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/`.
@@ -1,6 +1,12 @@
{ {
"record": "2026-10-07 FIRST CLUSTER DEMONSTRATION for search-with-proof", "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...", "image": "ghcr.io/norandom/ousast-search-task@sha256:e2c8b460...",
"side": "vulnerable", "side": "vulnerable",
"outcome": "demonstrated", "outcome": "demonstrated",
@@ -18,5 +24,23 @@
"served-root guidance: wire the served dir to ${served_root}", "served-root guidance: wire the served dir to ${served_root}",
"oracle prefix-bypass coverage: sibling canary for startswith-without-separator vulns", "oracle prefix-bypass coverage: sibling canary for startswith-without-separator vulns",
"control-signal feedback: served-root hint so the agent self-corrects wiring" "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."
}
}
+9
View File
@@ -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. from repository names. The selected manifest's pair 1 currently lacks this metadata.
Live transport, provider authentication/cost, real project buildability, and AX Live transport, provider authentication/cost, real project buildability, and AX
oracle operation must still be measured; an offline probe cannot establish them. 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.