Venus v0.3.3

Venus v0.3.3

Summary

Venus v0.3.3 is a security release. It binds the publics of the SNARK wrapper's recursivef STARK, binds airgroup values to the Fiat-Shamir transcript, and closes soundness gaps in the memory, MemAlign, Main, Arith, Binary, Blake2br, Poseidon2 and DMA state machines. It also hardens the guest library's hinted computations, the native and SNARK verifiers, the assembly emulator, and the host-side handling of ELF files and hints. Two crashes in the SNARK path are fixed.

The proving key and the SNARK key must be regenerated. Program verification keys change, and proofs produced by earlier versions are not accepted by the new verifiers.

Security Fixes

SNARK wrapper publics binding

The recursivef STARK, which verifies vadcop_final inside the on-chain SNARK, was still generated by the upstream JavaScript recursion templates. Its constraint polynomial had no public operand: the publics entered the transcript but were not bound to the trace, so the final circuit could be fed publics that the vadcop_final proof does not attest. This is the same gap that v0.3.2 closed for the other recursion layers.

recursivef is now generated by the native setup (generate-key-rs --snark) with the same public binding as the other recursion AIRs, and its rootC input is pinned to the vadcop_final verification key, so a SNARK proof is valid only for that key. make generate-snark-key PTAU=<file> generates the whole SNARK key, and the setup no longer offers the JavaScript path for recursivef. The rootCVadcopFinal argument of the Solidity verifier must equal getRootCVadcopFinal(); any other value fails verification.

Airgroup values in the Fiat-Shamir transcript

The airgroup values of a basic AIR proof (its bus sum) were used by the quotient check but never absorbed into the transcript. The check is affine in each airgroup value, so a prover could fix the trace, read the challenges and solve for a value that passes. They are now absorbed right after the stage-2 root, identically in the CPU and GPU provers, the native verifier and the recursion circuits (port of pil2-proofman#619). The setup rejects proof values, airgroup values and air values that no transcript binds before the challenges they feed.

State machine constraints

• Memory clock wrap-around. A segment could advance the memory clock by up to 2^38 per row outside the bus, so enough segments wrapped it around p and ordered a read after a later write of the same address. The step handed to the next segment is now range checked below 2^38 (upstream #1332).
• MemAlign stores. sel_prove was not tied to the program row, so a program could perform the aligned writes of an unaligned store that Main never executed. It is now fixed by the ROM (upstream #1142).
• Indirect jumps. The upper half of a computed jump target was ignored, so a jump to an invalid 64-bit address could be proven as a jump to a valid one (upstream #1146).
• First row of a memory area. The first row could continue the address group of the previous area's initial values and read a word of another area as 0. The first row of the first segment of every memory except free input must now open a new address (upstream 8d3bffa53).
• Signed products. Arith did not bind the sign of a signed product to the operand signs, so MUL, MULH and MULSUH could return the absolute product (for example MUL(1, -1) = 1).
• LT_ABS_NP. The comparison dropped the carry of the negation, so DIV(-256, 256) could return 0 with remainder -256 (upstream #1091). The binary table and VirtualTable0 grow accordingly.
• Blake2br. Message words could be exchanged between two calls; the permutation now carries the call's main step (upstream fc391b799).
• Poseidon2. Output elements could be written in a non-canonical encoding (x + p). They are now range-checked 16-bit limbs with a canonical-encoding check (upstream 4984315a1).
• DMA. An operation with count 0 is now accepted with a 64-bit address, whose high part must otherwise be zero (upstream #1318).

Guest library

The guest library takes prover-supplied hints for big-integer arithmetic, square roots, inverses and elliptic-curve operations. These checks were missing or incomplete:

• Remainder and bit-decomposition lengths are bounded before they are copied (a long hint overwrote the guest stack), and long division verifies the whole remainder.
• The MODEXP exponent decomposition is checked before the loop can exit early, and squaring propagates every carry.
• Square-root and inverse hints must be canonical, and msb_pos hints are bounded before use.
• Elliptic-curve additions and doublings handle the identity and equal points, subgroup checks and cofactor clearing use the complete group law, Miller loops reject degenerate line hints, and pairing and MSM inputs are validated.
• ECDSA signature and public key inputs are validated, and hinted points are bound instead of only rejecting the signature.
• The bump allocator checks for address overflow.

Verifiers

• The native verifier reads proofs with checked bounds and requires an exact shape and canonical field elements, so a malformed proof is rejected instead of panicking, and each proof has one encoding.
• The setup refuses to derive a native verifier for a setup it cannot verify.
• Malformed SNARK proofs are rejected before conversion and can no longer abort the process.
• cargo-zisk verify and verify-snark report the statement they accept and can pin it to a program with -e <elf> or --program-vk; make verify passes the guest ELF.
• Public outputs above 32 bits are rejected.

Assembly emulator

A malicious guest could make the fast assembly emulator read or write host memory: dynamic jumps, precompile operand pointers, fcall parameters and results, loads, stores and DMA operations were not bounds-checked. All of them are now confined to the guest's regions, and a violation stops the execution with an error code. The emulator services listen on the loopback interface only.

Host-side inputs

• ELF file names could inject commands into the assembly build; names are now sanitized.
• A small ELF could force huge allocations; code is bounded to the ROM window and budget.
• ELF sections lost their last bytes when their size was not a multiple of 4, and constructor arrays were not loaded.
• ebreak, writes to read-only CSRs and a non-zero exit code now terminate the execution as a failure (upstream #1359, #1362), and several RISC-V decoding bugs are fixed (c.fldsp, FENCE, CSR immediates).
• The hint reorder buffer is bounded, and MODEXP hint sizes use checked arithmetic.

Setup

The fixed columns of the basic AIRs now come from the PIL compiler output instead of a separate Rust reimplementation of every table, so the PIL sources are their only definition. The setup also rejects quotient openings without xi, ambiguous custom-commit evaluations, and recursion setups that recursive2 could not verify with one circuit. None of these occurs in the current PIL.

CI

Pull requests from forks no longer run on the self-hosted runner. The binary installation test, which installed upstream ZisK on that runner with a write token, and the CLA bot, which passed all repository secrets to a third-party workflow, are removed.

Bug Fixes

• SNARK proofs crashed while computing the final witness: the witness library's entry point fell off the end of a function returning int. A failed build of that library now fails the setup.
• With --snark, the final PLONK prover could write past the STARK prover's GPU buffer when it was smaller than the 28 GiB the final circuit needs; the overflow now gets an allocation of its own.
• prove-snark no longer runs out of GPU memory, and it writes the same proof format as prove --snark, which verify-snark reads.
• The BN128 grinding kernel failed to launch, and the BN128 transcript faulted on misaligned shared memory.
• Unaligned reads that span two words were merged and counted incorrectly, and their width was misreported to the memory bus.
• DMA planner fixes (upstream #1251), and DMA inputcpy is proven only with the full Dma and DmaPrePost AIRs.

Performance

Proof time on the same RTX 5090 machine, v0.3.2 against v0.3.3 (mean of three runs after a warm-up):

Ethereum mainnet block	v0.3.2	v0.3.3	Change
24628607 (66 txs, ~7 Mgas)	18.051s	17.879s	-0.172s (-1.0%)
24628590 (478 txs, ~49 Mgas)	78.650s	78.850s	+0.200s (+0.3%)

The soundness fixes add little proving work: one constraint each in Main and Arith, a wider binary table, a few range checks, and three more transcript elements per basic proof. The GPU evaluators of the changed constraint polynomials are regenerated. With --snark, the SNARK wrapper adds about 2 seconds.

Compatibility

• Regenerate the proving key (make setup) and the SNARK key (make generate-snark-key PTAU=<file>). Program verification keys change.
• verify-snark takes -k <proving key> and -w <SNARK key> and reads the proof that prove --snark and prove-snark write.
• ziskos successive commit calls append to the public outputs instead of overwriting them.
• Public outputs above 32 bits are rejected.
• The assembly emulator services listen on 127.0.0.1 only.

Known Issues

• Guest stack overflow is not trapped: the 4 MiB stack sits above .bss, so deeper recursion overwrites .bss, .data and the output area. Upstream ZisK moved the stack to the bottom of RAM (#1162); porting it changes the guest memory map and toolchain linker script and is planned for a later release.
• Under a stricter accounting of the FRI folding and batching errors, the conjectured security of the current STARK parameters is about 126 bits, not the 128 bits the setup reports. The parameters will be adjusted in a later release.