바인딩되지 않은 Uni-Skip 클레임으로 Jolt의 검증 도구 깨기

I found a soundness bug in Jolt’s transparent/non-ZK verifier that allowed a forged proof to verify for an execution that never actually happened (X post). The issue was fixed quickly in PR #1474 after I disclosed it privately. At a high level, the verifier trusted a proof-provided intermediate claim without checking that it was actually produced by the previous polynomial message. That missing equality was enough to let a malicious prover splice together two locally consistent proof components into one globally false proof. Bug Summary Jolt’s uni-skip verifier accepted a proof-provided output claim without checking that it matched the submitted univariate polynomial evaluated at the verifier’s challenge. The missing check was essentially: claimed_output == uni_poly.evaluate(r0) where r0 is the Fiat–Shamir challenge sampled after the first-round univariate polynomial. Without this check, the first-round uni-skip proof and the remainder proof could each look valid while silently referring to different statements. In other words, the verifier checked both sides of the bridge, but forgot to check that the bridge itself was connected. What Uni-Skip Is Uni-skip is a prover-side optimization for sumcheck. The paper Speeding Up Sum-Check Proving describes it as an optimization that modifies the protocol by replacing part of the usual sumcheck flow with a higher-degree univariate step. In Jolt, this is used as part of the optimized Spartan prover path. In an ordinary sumcheck, the prover reduces a large multilinear claim one variable at a time. After the prover sends a univariate polynomial for the current round, the verifier samples a challenge r , evaluates that polynomial at r , and uses the result as the next claim. Uni-skip compresses some of that work. Instead of walking through several small Boolean rounds in the usual way, the prover sends a larger univariate polynomial that represents a packed slice of the computation. The verifier then samples a challenge r0 , and the protocol continues with a remainder sumcheck from the value of that univariate polynomial at r0 . Uni-skip changes how the first part of the sumcheck is represented, but it does not change what the verifier must learn from it: after sampling r0 , the verifier must use the submitted univariate polynomial evaluated at r0 as the next claim for the remainder sumcheck. In this bug, the verifier checked that the submitted univariate polynomial had the correct total sum, and it also checked the remainder proof starting from a claimed output value. But it passed to check that the claimed output value was actually the polynomial evaluated at r0 . That missing check is the entire bug: claimed_output == uni_poly.evaluate(r0) The Two Affected Uni-Skip Paths There were two relevant uni-skip paths: SpartanOuter SpartanProductVirtualization Both had the same missing boundary check, but they sit in different parts of the verifier. α_outer α_outer is the output claim of the SpartanOuter uni-skip path. It becomes the input claim to the Stage 1 outer remainder sumcheck. Stage 1: SpartanOuter uni-skip -> α_outer SpartanOuter remainder -> input claim = α_outer This path is especially important because SpartanOuter is where Jolt’s outer R1CS layer checks VM execution semantics: instruction behavior, register values, RAM accesses, store/load consistency, and related constraints. So if a forged proof can arrange for the only remaining mismatch to be an execution-semantics violation, that mismatch naturally lands in Stage 1. α_product α_product is the output claim of the SpartanProductVirtualization uni-skip path. It goes into Stage 2, but not as the whole Stage 2 claim. Stage 2 batches several sumcheck instances together: Stage 2: 0. RAM read/write checking 1. Spartan product remainder u64 { x } input: 1333337 valid output: 1333337 claimed output: 1333338 unpatched verifier: accepts patched verifier: rejects That is the core failure mode of a zkVM soundness bug: the verifier accepts a public output that the guest program did not produce. Patch The fix is conceptually simple: after sampling r0 , compare the proof-provided output claim with the actual evaluation of the submitted univariate polynomial. let expected_output = proof.uni_poly.evaluate(&r0); let claimed_output = sumcheck_instance.expected_output_claim(opening_accumulator, &[r0]); if claimed_output != expected_output { return Err(ProofVerifyError::UniSkipVerificationError); } The important part is that this check happens before the claimed output is used as the input claim for the remainder proof. PoC See more details and a working PoC at jolt-uni-skip-exploit. Thanks to young (coo) for cheering me on during the hunt.