Hello, I’m Minsun Kim, a cryptography researcher at HexaLabs.
Recently, we analyzed vulnerabilities related to zkVMs disclosed by OtterSec and solved the CTF-style Challenge, which targets earlier versions provided for exploitation.
zkVMs are drawing attention as powerful tools that can prove the correctness of program execution. However, as proof systems become more complex, even a small mistake in implementation details can collapse the entire set of assumptions.
OtterSec’s Challenge covered two zkVM systems: Jolt and Nexus. In both cases, the core issue was that values that must be absorbed into the Fiat–Shamir transcript were missing. As a result, an attacker could tune the equations checked by the verifier in a favorable way.
In this post, through these two cases, we examine why transcript design is itself the security boundary of a proof system.
What is the Fiat–Shamir transform?
The Fiat–Shamir transform is a technique that converts an interactive proof—where the prover and verifier must interact and exchange randomness—into a non-interactive proof using a hash-based transcript. During proving, values that affect verification, such as commitments, intermediate claims, and public inputs, are accumulated into the transcript in order, and subsequent challenges are derived from this transcript.
If some value influences the verification equation but is not included in the transcript, then even after the challenge is fixed, an attacker can still adjust that value to their advantage. At that moment, the soundness guarantee that Fiat–Shamir is supposed to provide can break down.
In both issues, important verification values were not bound to the transcript, those values entered the verification equations linearly, and the attacker could adjust them in the needed direction to forge a proof. For both issues, we will walk through how to generate proofs for arbitrary incorrect witnesses.
Jolt (a16z)
Jolt is a zkVM built for RISC-V programs. The proof structure in Jolt looks roughly as follows.
JoltProof {
commitments: Vec<Commitment>,
opening_claims: Map<OpeningId, Claim>,
proofs: Map<Stage, SumcheckProof>,
...
}
In the OtterSec blog post, opening_claims is described as a variable that is not absorbed into the transcript, and the attacker can forge it to keep the derived randomness unchanged while still satisfying the checked equalities.
The Jolt exploit proceeded in two main steps. First, the internal verification process contained five sumcheck equations and one Dory check. The Dory side was relatively easy to bypass as long as the transcript state was aligned appropriately. In theory, it would also have been possible to modify the prover side to ignore failures, but rather than heavily altering prover logic, I chose to make the transcript itself match the state expected by the verifier.
First, I observed how the sumcheck verification equations respond as opening_claims changes. In the verification code, it originally returned an error immediately if output_claim and expected_output_claim differed. I temporarily changed that part to print both values so I could see how each moved.
println!("a = {:?}", output_claim);
println!("b = {:?}", expected_output_claim);
if output_claim != expected_output_claim {
// return Err(ProofVerifyError::SumcheckVerificationError);
}
This makes it possible to directly track which side is fixed or how it changes linearly when a particular opening_claims value is adjusted.
Let’s look at one example. Consider the code immediately before the check that compares output_claim and expected_output_claim.
let expected_output_claim = sumcheck_instances
.iter()
.zip(batching_coeffs.iter())
.map(|(sumcheck, coeff)| {
// If a sumcheck instance has fewer than `max_num_rounds`,
// we wait until there are <= `sumcheck.num_rounds()` left
// before binding its variables.
// So, the sumcheck *actually* uses just the last `sumcheck.num_rounds()`
// values of `r_sumcheck`.
let r_slice = &r_sumcheck[max_num_rounds - sumcheck.num_rounds()..];
if let Some(opening_accumulator) = &opening_accumulator {
// Cache polynomial opening claims, to be proven using either an
// opening proof or sumcheck (in the case of virtual polynomials).
sumcheck.cache_openings_verifier(
opening_accumulator.clone(),
sumcheck.normalize_opening_point(r_slice),
);
}
let claim = sumcheck.expected_output_claim(opening_accumulator.clone(), r_slice);
claim * coeff
})
.sum();
This is the computation of expected_output_claim, and we can see it is computed as a linear combination of claim * coeff. These claim values are extracted from opening_claims during verification, so by changing one value in opening_claims, we can adjust expected_output_claim linearly. By making it equal to output_claim, we can bypass the check.
Because opening_claims consists of multiple values, after observing enough times to collect each value’s influence on expected_output_claim, I organized the relationships as a system of linear equations over a finite field and computed values that satisfy all five sumcheck conditions simultaneously. In this process, I used SageMath to solve the system over the relevant curve field.
Jolt uses the bn128 curve field, whose modulus is the curve order
21888242871839275222246405745257275088548364400416034343698204186575808495617. Finding a solution over this field resolves the issue.
For example, suppose the following results were observed for two linearly acting opening_claims variables \(o_1, o_2\).
opening_claims\(o_1, o_2\) → the following checks fail \(a_1 = b_1, a_2 = b_2\)opening_claims\(o_1 + 1, o_2\) → the following checks fail \(a_1 = c_1, a_2 = c_2\)opening_claims\(o_1, o_2 + 1\) → the following checks fail \(a_1 = d_1, a_2 = d_2\)
When \(o_1\) increases by 1, the right-hand side of the first check increases by \(c_1 - b_1\), and the right-hand side of the second check increases by \(c_2 - b_2\). Similarly, when \(o_2\) increases by 1, the right-hand side of the first check increases by \(d_1 - b_1\), and the right-hand side of the second check increases by \(d_2 - b_2\).
To satisfy both checks, we can solve for the increments using the following linear system.
$$\begin{bmatrix}c_1 - b_1 & d_1 - b_1 \\c_2 - b_2 & d_2 - b_2\end{bmatrix} \cdot\begin{bmatrix}o\_increment_1 \\o\_increment_2\end{bmatrix} = \begin{bmatrix}a_1 - b_1 \\a_2 - b_2\end{bmatrix}$$
Adding the resulting \(o\_increment_i\) values to the original \(o_i\) gives a solution. In practice, you proceed similarly while accounting for five checks. Note, however, that not all opening_claims values act linearly in the equations.
Aligning the transcript itself was simpler than expected. The prover’s reduce_and_prove and the verifier’s reduce_and_verify generate challenges along the same flow, but if the absorbed byte sequences diverge, they reach different transcript states. So you can inspect the verifier’s transcript state at a certain point and then insert bytes on the prover side that produce the same effect at the corresponding position, reproducing the state the verifier expects. In practice, it was sufficient to dump the verifier transcript state at one point and transplant it to the corresponding point on the prover side to make the Dory check match.
pub fn reduce_and_prove<ProofTranscript: Transcript, PCS: CommitmentScheme<Field = F>>(
&mut self,
mut polynomials: HashMap<CommittedPolynomial, MultilinearPolynomial<F>>,
mut opening_hints: HashMap<CommittedPolynomial, PCS::OpeningProofHint>,
pcs_setup: &PCS::ProverSetup,
transcript: &mut ProofTranscript,
) -> ReducedOpeningProof<F, PCS, ProofTranscript> {
tracing::debug!(
"{} sumcheck instances in batched opening proof reduction",
self.sumchecks.len()
);
// 2. Re-fix the transcript using the dumped state here
...
pub fn reduce_and_verify<ProofTranscript: Transcript, PCS: CommitmentScheme<Field = F>>(
&mut self,
pcs_setup: &PCS::VerifierSetup,
commitment_map: &mut HashMap<CommittedPolynomial, PCS::Commitment>,
reduced_opening_proof: &ReducedOpeningProof<F, PCS, ProofTranscript>,
transcript: &mut ProofTranscript,
) -> Result<(), ProofVerifyError> {
#[cfg(test)]
if let Some(prover_openings) = &self.prover_opening_accumulator {
assert_eq!(prover_openings.len(), self.len());
}
// 1. Dump the transcript state here
The state implementation of Blake2bTranscript used in this issue is as follows.
pub struct Blake2bTranscript {
/// 256-bit running state
pub state: [u8; 32],
/// We append an ordinal to each invocation of the hash
n_rounds: u32,
#[cfg(test)]
/// A complete history of the transcript's `state`; used for testing.
state_history: Vec<[u8; 32]>,
#[cfg(test)]
/// For a proof to be valid, the verifier's `state_history` should always match
/// the prover's. In testing, the Jolt verifier may be provided the prover's
/// `state_history` so that we can detect any deviations and the backtrace can
/// tell us where it happened.
expected_state_history: Option<Vec<[u8; 32]>>,
}
Because the transcript state is determined by the state array of 32 8-bit integers and the n_rounds value, it can be manipulated by dumping and storing those values.
In summary, in Jolt we could adjust opening_claims that were not bound to the transcript, and by exploiting the fact that each sumcheck verification equation responded linearly to those values, we ultimately constructed a forged proof that satisfied all checks. The Dory check was handled by manually aligning transcript states, and the remaining core verification equations were passed by solving them via linear algebra.
Nexus (StarkWare)
In the case of Nexus, the structure was much simpler than Jolt. Unlike Jolt, where multiple verification equations had to be satisfied simultaneously, here it was essentially enough to steer a single core check in the desired direction. According to OtterSec’s explanation, claimed_sum only needs to satisfy the constraint that the overall sum is zero, and this value is also not absorbed into the transcript. Therefore, from an attacker’s perspective, it is natural to consider adding \(k\) to one term and subtracting \(k\) from another so that the total sum remains unchanged, while observing how the verification equation changes.
Since the goal is to generate a proof even when no correct witness exists, the first step was to make the execution result match what the verifier expects so that proof generation can proceed to completion. To do so, I added code to k_trace in vm/src/trace.rs to directly fill in the public output so it matches the output format and values expected by the verifier.
// Must match verify_expected encoding exactly.
let mut out = postcard::to_stdvec_cobs(&Some(true)).expect("encode Some(true)");
let padded_len = (out.len() + 3) & !3;
out.resize(padded_len, 0x00);
if let Some(layout) = view.memory_layout {
view.output_memory = out
.iter()
.enumerate()
.map(|(i, b)| emulator::PublicOutputEntry {
address: layout.public_output_start() + i as u32,
value: *b,
})
.collect();
}
This allows proving to continue even with an invalid witness, up to the point where only stwo’s ConstraintsNotSatisfied error remains. If you ignore the point where that error is raised, proof generation can still be completed even for incorrect witnesses.
{
// return Err(ProvingError::ConstraintsNotSatisfied);
}
If you attempt to verify the generated proof as-is, the following part—the only equality check—fails. While multiple equalities fail during proving, in verification they are combined linearly into a single final check. Just like Jolt, verification completes only if a equals b.
let a = composition_oods_eval;
let b = components.eval_composition_polynomial_at_point(
oods_point,
&proof.sampled_values,
random_coeff,
);
println!("{}", a);
println!("{}", b);
In Jolt, because multiple equations had to be satisfied at once, it was necessary to collect and solve a system of linear equations. In Nexus, because it was effectively a single check, it wasn’t necessary to do computations that complex. Since the constraint that the total claimed_sum is zero was already satisfied, it is enough to add \(k\) to one value and subtract \(k\) from another in a way that makes the single equality hold.
One tricky part in implementation, however, was that Nexus uses an unusual QM31 field rather than a typical prime field. Therefore, the correction value had to be computed accurately over that field as well, and I used a separate SageMath script to match the arithmetic. In other words, although the essence of the attack was a very simple linear adjustment, in the actual exploit you must follow the structure of the field where the operations occur in order to finally pass verification. Below is a SageMath implementation of the QM31 field.
p = 2^31 - 1
Fp = GF(p)
# i^2 = -1
R.<X> = PolynomialRing(Fp)
CM31.<i> = Fp.extension(X^2 + 1)
# u^2 = 2 + i
S.<Y> = PolynomialRing(CM31)
QM31.<u> = CM31.extension(Y^2 - (CM31(2) + i))
Because it is a field where the four basic arithmetic operations are well-defined, there is no issue solving linearly in the same way—but note that the resulting value is represented as four components each less than \(2^{31} - 1\).
(2042649430*i + 1471302658)*u + 384541130*i + 1645951658
In summary, in Nexus we could manipulate claimed_sum that was not bound to the transcript, and by exploiting the fact that it affects a single verification equation linearly, it was possible to make a proof for an invalid witness pass. The structure was simpler than Jolt, but that simplicity made it an even clearer example of how transcript omission leads directly to a soundness issue.