Mélodie

A runtime proof harness: replay an exploit in a sealed Nebius Token Factory sandbox and get PROVEN or NOT PROVEN, decided by a fresh canary, never by a model.

Comment

Inspiration

Security teams drown in scanner findings. A scanner matches package versions; it never runs the exploit, so "critical" often means "maybe". In CTEM terms, the hard step is validation: proving which findings actually fire in your code, so you fix what's proven first. Meanwhile, LLMs are increasingly asked to judge exploitability, and a model's confidence is not evidence. I wanted a verdict that nobody, including the model, can fake.

What it does

Mélodie is a runtime proof harness for a known finding in a supported vulnerability class. You submit an exploit input; Mélodie replays it in a sealed Nebius Token Factory Sandbox against a fresh database that holds a freshly planted random secret (a canary):

  • canary leaks into the output → PROVEN
  • canary stays put → NOT PROVEN (never "safe")

The canary is new on every run, so a PROVEN can't come from a recording or a cached answer, and you can type your own payload to check. The live demo runs the ormar SQL injection (CVE-2026-26198): the example payload is PROVEN, a harmless input (price) is NOT PROVEN, and every verdict shows the 6 real steps it took.

Scope, stated plainly: exploit validation for a known finding in a supported class. Not discovery, not a scanner, not arbitrary-CVE coverage.

How I built it

  • Nebius Token Factory Sandboxes (ConTree): every live verdict is a real, disposable microVM run from a pre-baked image (python:3.12-slim + ormar). Pipeline: pre-flight gates → boot sandbox + fresh DB → harden SQLite → plant canary + deliver input as a file → replay → observe the canary in stdout. The input is delivered as data, never shell-interpolated; SQLite extension loading and ATTACH are disabled; 25 s budget per run.
  • NVIDIA Nemotron 3 Super via the Token Factory API: the agent I measured. Given a vulnerability claim and a sandbox, it locates the flaw and proposes exploit payloads; the same sealed replay judges every proposal. Nemotron proposes. The replay judges. Super for the agent loop; Nano, Lightning and Ultra only for comparison, with every call's tokens (including reasoning tokens) cost-logged.
  • Tavily: the agent's advisory tool. CVE lookups are pinned to authoritative sources (GitHub Advisories, NVD, OSV, cve.org) twice over: Tavily's include_domains in restrict mode, then our own URL allowlist. The agent gets at most 2 lookups per run, and every source's URL, title and relevance score is recorded by our code, not by the model. Tavily grounds context; it is never a verdict input. That separation is the point: retrieval informs, execution decides.
  • Serving: one AWS Lambda behind a public Function URL serves the React/TypeScript UI and the model-free /api/verify; secrets live in SSM + KMS. The live path makes zero model or Tavily calls, so it costs essentially nothing to keep online through judging.
  • Release engineering: CI (lint, type-check, 40 Python checks, 23 Vitest tests, build), a daily black-box check of the live URL (example → PROVEN, price → NOT PROVEN, fresh canary, build identity), build identity in the UI footer, and immutable GitHub releases. The demo serves v1.0.2 · acb81cf.

Measured honestly

29 valid receipts (2 excluded and disclosed), Wilson 95% intervals, about 0.43 USD in total (217 Nemotron calls ≈ 0.21 USD + 28 Tavily credits ≈ 0.22 USD). Reproducible from a fresh clone with python -m prover.eval_report, and visible in the demo via /eval.

  • Harness discrimination: the patched version returns NOT PROVEN on all 4 targets (1/1 each).
  • Nemotron, unaided: Starlette path traversal located 4/5 and weaponised 4/5; GitPython command injection weaponised 0/4. The limit is shown, not hidden.
  • Fix verification: FIX VERIFIED on Starlette, GitPython and ormar.

Challenges I ran into

  • Making a verifier credible, not just able to say PROVEN. I added a model-free matched negative control: the same exploit against the fixed version must return NOT PROVEN, or the harness is broken.
  • Model wording vs evidence. On a patched target, Nemotron concluded the code "effectively prevents" the attack, a universal safety claim no run can support. So the product never says "safe".
  • No client-side timeout in the sandbox SDK: a slow image bake looked exactly like a hang. I wrapped every run in a wall-clock budget (reported in my feedback).
  • Keeping a public, no-login demo cheap and safe: model-free live path, input caps, rate limits, a concurrency ceiling and a budget alert.

Accomplishments that I am proud of

  • A live, public proof that anyone can re-run with their own payload, getting a new canary every time.
  • An honest evaluation that publishes its own failure (GitPython 0/4) next to its successes.
  • A sealed release: a fresh-clone audit reproduces the eval and the tests, gitleaks finds no secrets in the history, and the demo is checked daily.

What I learned

Model confidence is not evidence; execution is. Small-n results need intervals, not percentages. And a second run finds what a first run can't: the two-run witness caught a display bug before release.

What's next for Mélodie

More live classes (path traversal and command injection already work as recorded replays), persisted receipts for every live run, a CI gate that blocks a merge only when a finding is PROVEN, and the existing MCP server (verify_proof) so coding agents can ask the harness instead of guessing.

Fresh project

Built solo during the Submission Period. The first commit (30 Sep 2026) is the learning phase (kept in archive/); the product was built 5–29 Oct 2026. Nothing pre-existing is reused beyond open-source dependencies and the third-party libraries used as vulnerable targets (Starlette, GitPython, ormar, pinned and unmodified).

Built With

Share this project:

Updates

Submission history