Fix audit findings from 2026-04-15 report#1442
Draft
0xAndoroid wants to merge 1 commit into
Draft
Conversation
Three hardening / documentation fixes from Justin Thaler's audit notes. No soundness bugs found; fixes are all completeness / maintenance grade. - tracer: remove default body from `RISCVInstruction::has_side_effects`. Direct impls must now declare their side-effect status explicitly, preventing a future instruction from silently being replaced with a NOP when `rd = x0` lowering runs. `VirtualAdvice` gains an explicit `false` declaration (rd-only write). - zkvm/ram/val_check.rs: promote the RamVal / RamValFinal address-point alignment check from `debug_assert_eq!` to a runtime `assert_eq!` on both prover and verifier. The check runs once per proof — cost is negligible — and the invariant underpins the unified RAM sumcheck's claim space, so debug-only enforcement was fragile. - zkvm/r1cs/constraints.rs: document the RV64 wrap completeness limitation of the LD/SD `RamAddress = Rs1Value + Imm` constraint. Computed in the BN254 field, not modulo 2^64 — honest programs that wrap addresses cannot be proved. Soundness unaffected; real programs use addresses near `0x80000000`, far from the wrap boundary. Two findings deferred: `DoryGlobals` process-wide mutable state (large refactor, blocks only concurrent in-process proof generation which is not a supported workflow) and Dory transcript label flattening (requires Transcript API change, no soundness impact). See `AUDIT_ANALYSIS.md` for full per-finding reasoning. Verified: `cargo clippy --all --features host` and `...host,zk` clean; `cargo nextest run -p jolt-core muldiv` passes in both modes.
Contributor
|
Warning This PR has more than 500 changed lines and does not include a spec. Large features and architectural changes benefit from a spec-driven workflow. If this PR is a bug fix, refactor, or doesn't warrant a spec, feel free to ignore this message. |
6 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Addresses Justin Thaler's 2026-04-15 audit notes (with Claude assistance, delivered
jolt-audit-report.html). Report header: "No soundness vulnerabilities found." All five findings were completeness / hardening / crypto-hygiene items.Three fixed, one documented, two deferred with rationale. See
AUDIT_ANALYSIS.mdfor per-finding reasoning.Fixed
has_side_effects()default (tracer). Removed the trait default body so every direct impl must declare its side-effect status.VirtualAdvicegets an explicitfalse. Prevents a future instruction from silently being replaced with a NOP under therd = x0lowering.debug_assert(jolt-core/zkvm/ram). Promoted the prover + verifier alignment check betweenRamValandRamValFinaladdress points to runtimeassert_eq!. One check per proof — cost is negligible, invariant is load-bearing.Documented (not changed)
RamAddress = Rs1Value + Immconstraint is evaluated in the BN254 field (~254 bits), not mod 2^64. LD/SD are the only load/store ops not decomposed into virtual sequences, so they are directly exposed. This is a completeness limitation only — a malicious prover cannot exploit it. Real programs use addresses near0x80000000, far from the 2^64 wrap boundary. Added a block comment at the constraint site explaining the limitation. Closing the gap requires bit-decomposition + conditional 2^64 subtraction, a soundness-sensitive R1CS change that we elected not to make as part of this audit pass.Deferred (noted for follow-up)
DoryGlobalsprocess-wide mutable state. Real, but fixing it requires threading aDoryContexthandle through the entire commitment / opening / streaming call graph. Would only trigger if concurrent in-process proof generation becomes a supported workflow. Single-proof-per-process usage is safe.Transcript::append_*requirelabel: &'static [u8], while Dory passes&[u8]. Fixing properly means adding a dynamic-label variant across all Transcript impls (Blake2b / Keccak / Poseidon) and invalidating existing serialized proofs. No soundness concern per audit. Deferred as a transcript-API design question.Uncertainty flags
Draft because Finding 1's document-vs-fix call is a maintainer decision.
Test plan
cargo clippy --all --features host -q --all-targets -- -D warnings— cleancargo clippy --all --features host,zk -q --all-targets -- -D warnings— cleancargo nextest run -p jolt-core muldiv --cargo-quiet --features host— passcargo nextest run -p jolt-core muldiv --cargo-quiet --features host,zk— pass