From 7ab5c2ab2d552cd982344d24d51e366249d1c591 Mon Sep 17 00:00:00 2001
From: Marius Ciepluch <11855163+norandom@users.noreply.github.com>
Date: Mon, 12 Oct 2026 11:46:26 +0200
Subject: [PATCH] measure(g2): proof-arm on the 3 fair hits -- push-time lift
 0/3 (structural), proof is async

All 3 hits have a runtime oracle (search FAMILY_ORACLES: injection->sql/command, ssrf for
untrusted_destination -- corrects the earlier families.toml-based 'dcmcp unprovable'). But
search/verify.verify() needs an AUTHORED runnable demo + both head/base building OFFLINE + a
sandbox differential (3/3 affected vs 0/3 safe). The scan/push path reaches only suspicion/
static_corroboration; no code path from a scan suspicion to exploit_demonstrated, no Coordinator
caller from the push flow. So proof-arm lift AT PUSH TIME = 0/3 -- proving is a per-target,
offline-build, runtime, differential operation that can't run inside a pre-push hook (prior
per-pair demos were mostly inconclusive on this wiring).

Strategic consequence: proof/BLOCK is an ASYNC lane (CI/plane/triage with authored demos), not
pre-push. Honest pre-push product = advisory-with-conditions (bet #2); proof arm = async BLOCK
lane (bet #3). Local sandbox exists (userns).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 .../engine-change-scoped-analysis/brief.md    | 29 +++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/.kiro/specs/engine-change-scoped-analysis/brief.md b/.kiro/specs/engine-change-scoped-analysis/brief.md
index f69dd76..d754098 100644
--- a/.kiro/specs/engine-change-scoped-analysis/brief.md
+++ b/.kiro/specs/engine-change-scoped-analysis/brief.md
@@ -433,3 +433,32 @@ Deep scan on the 5 app-shaped+sound targets (`benchmarks/measurements/2026-10-12
 Detection appears on fair targets; release-grade BLOCK still needs (a) proof-arm elevation (suspicion→proven) and
 (b) family coverage (template XSS/SSTI) + the DSPy hint loop for misses. Next: recompute a floor on an app-shaped
 sound subset / real app corpus (VAmPI, NodeGoat, DjanGoat, vibe-py), and measure the proof arm's suspicion→proven lift.
+
+## PROOF-ARM MEASUREMENT on the 3 fair-target hits (2026-10-12) — push-time lift 0/3, structural
+
+Measured whether the proof arm can elevate the 3 fair-target suspicions (graphiti, mcp-remote, dcmcp) to
+`exploit_demonstrated`.
+- **Correction:** the search arm's `FAMILY_ORACLES` (search/demo.py) differs from families.toml's `verifier`.
+  All 3 hits HAVE a runtime oracle: injection→(sql,command), untrusted_destination→(ssrf). (deserialization/
+  access_control/config_secrets have NONE — empty tuple → `no_oracle`.) So dcmcp IS provable in principle
+  (earlier "unprovable" was a families.toml misread).
+- **But proving is a runtime differential:** `search/verify.verify()` requires (1) an AUTHORED declarative demo
+  (start the app on a port, run exploit steps, fill oracle placeholders: sql→database_path, command→marker_dir,
+  ssrf→callback_url), (2) BOTH head AND base runnable with OFFLINE deps (`pip --no-index`, `npm ci --offline`),
+  (3) a sandbox differential "owned effect in 3/3 affected runs and 0/3 safe runs". Local host has a sandbox
+  (`isolation_mode: userns`); the plane supplies a task-boundary dispatcher.
+- **The scan/push path reaches only `suspicion`/`static_corroboration`** (verification.py levels) — there is NO code
+  path from a scan suspicion to `exploit_demonstrated`, and no caller wires the search Coordinator from the push
+  flow. So **proof-arm lift at push time = 0/3**: not because the vulns are unreal, but because proving is a
+  per-target, offline-build, runtime, differential operation that cannot run inside a pre-push hook. (Prior
+  per-pair demo attempts were mostly inconclusive on this exact wiring — app startup, offline deps, oracle plumbing.)
+
+**Strategic consequence (resolves the three-bet fork):** proof/BLOCK is an ASYNC capability (CI / plane / triage
+with authored demos + a runnable sandbox), NOT a pre-push one. At push time the honest ceiling is corroborated
+suspicion. So:
+- **Bet #2 (advisory-with-conditions) is the honest PRE-PUSH product**: surface corroborated suspicions ("change
+  introduces a flow that looks like X; reachable if untrusted Y reaches it"), let the dev / coding-agent (who has
+  the app context) judge — matching the "oversee coding agents" framing and the suspicion-rung reality.
+- **Bet #3 (the proof arm) is the ASYNC BLOCK lane**: run `search/verify` on the plane/CI for the suspicions worth
+  proving, with authored (eventually DSPy-authored) demos. Worth an empirical run on one tractable target
+  (mcp-remote) to confirm the arm demonstrates on a real unseen vuln — a bounded, separate effort.