diff --git a/.kiro/specs/proof-arm-opencode/brief.md b/.kiro/specs/proof-arm-opencode/brief.md new file mode 100644 index 0000000..e727674 --- /dev/null +++ b/.kiro/specs/proof-arm-opencode/brief.md @@ -0,0 +1,87 @@ +# Brief: OpenCode-MCP proof arm (follow-up to search-with-proof) + +Status: brief / not yet specced. Proposed 2026-10-07 by the maintainer. Builds on +`search-with-proof` (see `../search-with-proof/verification-architecture.md`). + +## Motivation + +The search arm (directed, Cairn-inspired) works. The **proof-authoring** last mile is the drag: + +1. **Safety-classifier refusals.** Authoring exploit demos repeatedly tripped a safety classifier + this session when exploit payloads or step-by-step attack prose passed through the model or a + tool prompt. The mitigation so far (keep payloads on disk, treat demos as opaque) is a workaround, + not a fix, and it limits how directly the proof model can reason about the exploit. +2. **Nondeterministic wiring.** The agent authors a demo but intermittently mis-wires the app to + the oracle fixture (served directory for path, database URL for SQL), so a demonstrable pair + comes back inconclusive until a retry. Each miss has cost a paid run. + +Proposal: drive the proof with an **agentic coding tool (OpenCode MCP)** running **inside gVisor**, +using a model chosen for exploit authoring rather than one that refuses it, and **learn** the +proof-authoring policy with DSPy from **traces logged in OpenObserve**. + +## Shape + +- **Search model:** DeepSeek (current). Good at the directed fact/intent search. +- **Proof model:** GLM 5.3 (Anthropic-recommended) and/or an abliterated model via + `ABLITERATION_BASE_URL` (`abliterated large v2`). The abliterated model authors exploit **demos** + without the refusals that block a safety-trained model on this defensive task. +- **Proof driver:** OpenCode MCP (github.com/AlaeddineMessadi/opencode-mcp) as the agentic + demo-author, running inside the gVisor verification task so the exploit-authoring is sandboxed. +- **Learning:** DSPy compiles/optimizes the proof-authoring program (demo schema, wiring, steps) + from past traces, instead of the per-family hand-guidance we keep adding (which is now hitting + the prompt character budget — a signal the hand-rule approach is near its limit). Matches the + maintainer's "learned decisions, not hand-tuning" direction. +- **Tracing:** proof runs (reason/explore/author/verify, timings, outcomes, error classes) log to + **OpenObserve AI** at `OPENOBSERVE_URL` (org `OPENOBSERVE_ORG`, stream `OPENOBSERVE_TRACES_STREAM`). + DSPy consumes these traces as its training signal. +- **Credentials:** stored in `.env` like the existing keys, referenced by name only: + `ABLITERATION_API_KEY`, `ABLITERATION_BASE_URL`, `ABLITERATION_MODEL`, `OPENOBSERVE_URL`, + `OPENOBSERVE_ORG`, `OPENOBSERVE_TRACES_STREAM`, `OPENOBSERVE_TOKEN`. No secret value ever enters a + tracked file, a prompt, a log stream, or a commit. + +## The trust-domain decision (must be resolved first) + +The current design keeps the **model key on the VM only**; cluster tasks carry no secrets and have +restricted egress (verify tasks reach the files host only). Running the proof **model** inside gVisor +(as OpenCode MCP would) breaks both: the task would hold a model key and need egress to the model +API host. Two options: + +- **A. Scoped key + egress in the cluster (operator-managed).** Inject a spend-limited proof-model + key into the proof task (like the existing `gemini-api-secret` slot) and add a per-host egress + allowlist for the proof-model API. Keeps the fully-sandboxed agentic authoring the maintainer + wants; requires an operator change and widens the cluster's secret/egress surface. +- **B. Brain on the VM, execution in gVisor (current split preserved).** OpenCode MCP and the proof + model run on the VM; only the DAST execution stays in gVisor. No new cluster secret or egress; + but the agentic authoring loop is not itself sandboxed. + +Recommendation: start with **B** (no trust-domain change, fastest to try the abliterated proof model +and DSPy loop), and move to **A** only if sandboxing the authoring loop itself proves necessary. + +## Security scope (why an abliterated model is in-scope here) + +This is authorized **defensive** work: authoring proof-of-concept demos for **known CVE fix-pairs** +in a **gVisor-isolated** corpus, to demonstrate a regression before push. Guardrails to keep: + +- Demos are **data**, not agent code; they stay in the gitignored private area, never echoed. +- No real-world or third-party live targets; only the frozen fix-pair corpus and owned oracles. +- gVisor is the execution boundary; the abliterated model never runs code itself, it only writes a + declarative demo the trusted verifier executes. +- The abliterated model is confined to proof-authoring; the search and all reporting stay on the + normal models. + +## Open questions for the spec + +1. A or B for the trust domain (above). +2. Does the abliterated proof model actually raise the demonstrated rate and remove the wiring + misses, measured on the pairs already shown demonstrable (xiaomusic, glance)? Qualify before scaling. +3. DSPy program shape: what is the proof-authoring signature (inputs: candidate + oracle contract; + output: a valid, wired demo), and what metric does it optimize (demonstrated rate at zero false + proofs) from OpenObserve traces? +4. Does OpenCode MCP fit the existing executor/verifier task contract (no-secret, presigned I/O, + scratch/egress limits), or does it need a new task kind? +5. Cost envelope per proof vs the current DeepSeek authoring. + +## Not in scope + +Changing the search arm, the oracle differential, or the abstract-interpretation triage. This brief +is only about the **proof-authoring** driver and its learning loop. diff --git a/.kiro/specs/proof-arm-opencode/spec.json b/.kiro/specs/proof-arm-opencode/spec.json new file mode 100644 index 0000000..7946b47 --- /dev/null +++ b/.kiro/specs/proof-arm-opencode/spec.json @@ -0,0 +1,10 @@ +{ + "feature_name": "proof-arm-opencode", + "created_at": "2026-10-07T14:40:00Z", + "updated_at": "2026-10-07T14:40:00Z", + "language": "en", + "phase": "brief", + "approvals": {"requirements": {"generated": false, "approved": false}, "design": {"generated": false, "approved": false}, "tasks": {"generated": false, "approved": false}}, + "ready_for_implementation": false, + "summary": "OpenCode-MCP proof-authoring arm for search-with-proof: abliterated/GLM proof model, DSPy-optimized from OpenObserve traces; trust-domain decision (A scoped-key-in-cluster vs B brain-on-VM) must be resolved first. Creds in .env by name." +} diff --git a/.kiro/specs/search-with-proof/verification-architecture.md b/.kiro/specs/search-with-proof/verification-architecture.md new file mode 100644 index 0000000..b813ed0 --- /dev/null +++ b/.kiro/specs/search-with-proof/verification-architecture.md @@ -0,0 +1,52 @@ +# Search-with-proof: where each stage runs (verification architecture) + +Recorded 2026-10-07. search-with-proof has two stages across a trust boundary: a Cairn-inspired +directed state-space **search**, then a DAST-style **proof (verification)**. + +## The two stages + +1. **Search (Cairn-inspired).** A blackboard of facts, intents and hints. A reasoner proposes + independent, non-overlapping intents; tool-using explorers each confirm one fact against the + code. The goal is a declarative demo (a candidate PoC), never proof by itself. +2. **Proof (DAST verification).** The verifier builds and starts the app, drives the demo's steps + through the app's real interface, and watches a verifier-owned canary for a **differential** + between the vulnerable and fixed revisions: the owned effect appears on the vulnerable side and + not on the fixed side (3/3 vs 0/3). Only this differential earns `demonstrated`. + +## Trust boundary — what runs where + +The brain runs on the VM; the agent's tool executions and the DAST proof run as isolated tasks in +the kube-ax cluster. Secrets never enter the cluster. + +| Component | Location | Notes | +|-----------|----------|-------| +| Coordinator, board, budgets | VM (host) | Orchestrates the search; owns the global budget. | +| Reasoner + explorer **model calls** | VM (host) | The model key lives only on the VM. This is the brain. | +| Explorer **tool runs** (`list_files`, `read_file`, `grep`, `run`, build) | kube-ax AX Task (gVisor) | Carry no secrets; inputs/results via presigned object links. | +| **DAST proof / verification** | kube-ax AX Task (gVisor) | Builds, starts, attacks and observes the app. One task per revision. | + +- **gVisor is the isolation boundary.** The proof runs untrusted exploit code against a running + app, so it is sandboxed per-task in the cluster. +- **Secrets stay on the VM.** Executor and verifier tasks carry no credentials; they exchange + checkout archives, demos and results through presigned object-store links. Per-host egress is + restricted (verify tasks reach the files host only). + +## Verification lanes (the `--verify-lane` choice) + +- **`ax` (default for paid pilot runs):** verification runs **inside kube-ax** as gVisor AX Tasks, + one per side. This is how every paid pilot run this session executed the proof. +- **`vm` (local):** verification runs in **Bubblewrap on the host**, no cluster. Used for the + zero-cost ceiling proofs (a hand-authored demo verified locally with no model and no cluster), + which is how glance and xiaomusic were confirmed demonstrable before any spend. +- **`docker` (replay):** `benchmarks.search.demo_replay` runs a stored demo with no model calls in + a local Docker lane. + +## Why the proof is dynamic, not abstract interpretation + +Abstract interpretation (the static engine and the decision model) is the cheap, generalizable +**triage/ranker**: it selects and orders candidate regions across any repo without executing. It +plateaued as a **blocking** gate because it could not prove the required precision. search-with-proof +is the **dynamic** confirmation: a demonstrated finding is ground truth by execution, so it earns a +block without calibration. The per-app harness cost (building and running the app, wiring its served +directory or database to the oracle fixture) is the price of the dynamic proof and is why proof pays +off where a runnable harness exists, with abstract interpretation remaining the static backbone.