Void

Challenge

A TCP/TLS service asks for input, modulus (both u128, range 2<=modulus<2^96, 0<input<modulus<2^96), then a base64-encoded STARK proof. The service:

1. Rejects the request immediately unless gcd(input, modulus) == 1 — i.e. you must pick an invertible pair (the “impossible claim”).
2. Checks the proof’s public claim: program hash (blake2s over the bytecode words) must match the shipped challenge.executable.json, and the public output must decode to exactly [input, modulus].
3. Shells out to a pristine, freshly-cloned upstream stwo-cairo verify binary (verify --proof_path <f> --channel_hash blake2s) and requires exit 0.

challenge.cairo runs circuit_inverse(input, modulus). Cairo’s circuit codegen (build_try_into_circuit_modulus/build_failure_guarantee_verify in cairo-lang-sierra-to-casm) is supposed to make the CASM prove either “here is the real inverse” or “here is a nullifier n with 0 < n < modulus and input*n ≡ 0 (mod modulus), so no inverse exists.” You win by getting a STARK proof, accepted by the real verifier, that a genuinely invertible pair (gcd==1) took the second (“no inverse”) branch — a soundness break.

Dead end (this session, twice) → the actual lesson

Two separate local toolchains gave false negatives before this was solved:

• An earlier full pass concluded the local toolchain “cannot even prove an honest circuit program” (Constraints not satisfied / debug_assert_eq!(lookup_sum,0) failing) and shelved the challenge as intractable.
• Revisiting this session, a from-scratch build (matching cairo-lang-executable = 2.15.0, the version stwo-cairo itself pins) still failed with “Constraints not satisfied” — even for a 100% honest, non-adversarial run of the real challenge.executable.json.

Root cause: an unfixed upstream bug, tracked as (real, open) stwo-cairo issue/PR #1666 — crates/adapter/src/adapter.rs hardcodes

let public_segment_context = PublicSegmentContext::bootloader_context(); // assumes all 11 builtins present

but challenge.executable.json’s Standalone entrypoint only declares 5 of 11 builtins (output, range_check, range_check96, add_mod, mul_mod). The hardcoded bootloader-context assumption misaligns builtin memory segments for any #[executable]/circuit program with a non-default builtin set — completely independent of the CTF’s own vulnerability. This is exactly the wrong-source-version trap from Fork, wearing a different hat: “my STARK proof failed” was a toolchain bug, not a verdict on the exploit hypothesis. Fixing it (one-line patch, PublicSegmentContext::new(runner.get_program_builtins())) is required just to get an honest proof of the challenge program to go through at all. (This fix only matters for the prover/adapter path — the verify binary does pure JSON deserialization + AIR checks and never touches the adapter, so a locally-patched prover produces proofs the real, unpatched, pristine verify on the server accepts unchanged.)

With that fix, and [patch.crates-io] pinning cairo-lang-executable/cairo-lang-utils/cairo-lang-runner all to the same local v2.15.0 checkout (needed to avoid a cairo_lang_casm type-mismatch from mixed crates.io/path dependency resolution), an honest baseline proof of challenge.executable.json finally proved and verified — the first time in this challenge’s entire investigation history.

The vulnerability: off-by-one in the failure-guarantee range check

An earlier pass had (with the broken toolchain!) tried forcing the “nullifier” hint value to nullifier == modulus and observed ConstraintsNotSatisfied, and recorded this as disproving an off-by-one hypothesis in u96_limbs_less_than_guarantee_verify (i.e. concluding the AIR correctly enforces strict <). Per the user’s explicit prompt to re-verify direction before continuing to dig, this was retested from scratch with the now-working, honest-baseline-capable toolchain — and the earlier “disproof” was itself a toolchain artifact (the #1666 bug corrupts every circuit-program proof attempt, honest or forged, so the earlier “ConstraintsNotSatisfied” proved nothing).

Patched cairo-lang-runner’s hint-filling (invert_or_nullify in crates/cairo-lang-runner/src/casm_run/circuit.rs, the interpreter that supplies the CASM’s nondeterministic nullifier value) via an env-var override (VOID_FORCE_NULLIFIER) to force an arbitrary nullifier regardless of the true gcd, then swept values:

• Any in-range wrong nullifier (0 < n < modulus, but not a real annihilator) → deep segfault inside stwo-cairo’s witness generation (AtomicMultiplicityColumn::increase_at, an intentionally-unsafe/unchecked function per its own doc comment, receiving a wildly out-of-bounds range_check_18 address derived from the now-inconsistent mul_mod carry math) — confirmed deterministic and tied specifically to mathematical falseness across 18+ (input, modulus, nullifier) combinations. A real, reportable stwo-cairo memory-safety bug, but not itself flag-yielding: crash-free completion of that path would still leave an invalid range_check_18 LogUp sum, which the AIR is specifically designed to catch.
• Nullifier values > modulus (e.g. modulus+1, 2*modulus) → correctly rejected by CASM at pc=0:354 (the build_failure_guarantee_verify less-than check works fine here).
• nullifier == modulus exactly → input*modulus ≡ 0 (mod modulus) is always true, so the mul_mod arithmetic stays completely honest (no huge carries, no crash) — and the only thing standing between this and a valid “no inverse” proof is the boundary of the “less-than” check. It went through cleanly: prove + verify both succeeded, for input=3, modulus=5 (gcd(3,5)=1, real inverse 2 exists) claiming no inverse exists.

Independently re-verified the resulting proof with the plain verify --proof_path ... --channel_hash blake2s (matching exactly how the live server invokes its pristine build) — ✅ Proof verified successfully!, exit 0. Confirmed the proof’s public output decodes to [3, 5] as required by the server’s validate_public_claim.

This is a genuine off-by-one soundness bug in Cairo’s circuit failure-guarantee gadget: the “nullifier must satisfy 0 < n < modulus” check accepts n == modulus (a spurious “annihilator” that’s mathematically trivial and proves nothing about actual invertibility), letting a prover claim non-invertibility for any input/modulus pair whatsoever, invertible or not.

Exploit

1. Pick any invertible pair, e.g. input=3, modulus=5.
2. Run the (locally #1666-patched) prover with cairo-lang-runner’s nullifier hint forced to nullifier = modulus for the relevant circuit gate.
3. Prove challenge.executable.json on [input, modulus] — completes cleanly, output [3, 5].
4. Verify locally with the plain (unpatched) verify binary to confirm server-equivalence.
5. Connect to the live instance, send input, modulus, then base64(proof.json) → server returns the flag.

Tooling

• Fresh clones: starkware-libs/cairo @ v2.15.0 tag, starkware-libs/stwo-cairo @ main (unpinned upstream, matching the challenge Dockerfile’s own unpinned git clone).
• One-line patch to crates/adapter/src/adapter.rs (stwo-cairo) for the #1666 PublicSegmentContext bug (prover-only, doesn’t affect the deployed verify).
• Cargo.toml [patch.crates-io] redirecting cairo-lang-executable/cairo-lang-utils/cairo-lang-runner to the local v2.15.0 checkout, all three needed together to avoid a cairo_lang_casm type mismatch.
• VOID_FORCE_NULLIFIER env-var hook added to invert_or_nullify in cairo-lang-runner’s circuit.rs to force an arbitrary nullifier value for testing/exploitation.
• Methodology takeaway (validated twice this session, on Fork and Void independently): a failed local reproduction is not evidence against an exploit hypothesis until the toolchain itself has been proven to reproduce the honest baseline correctly. Both challenges’ “walls” turned out to be version/build mismatches, not real obstacles.