Skip to content

Harden verifier boundaries and transcript binding#1382

Open
quangvdao wants to merge 2 commits intoa16z:mainfrom
quangvdao:quang/upstream-verifier-boundaries-and-transcript-binding
Open

Harden verifier boundaries and transcript binding#1382
quangvdao wants to merge 2 commits intoa16z:mainfrom
quangvdao:quang/upstream-verifier-boundaries-and-transcript-binding

Conversation

@quangvdao
Copy link
Copy Markdown
Contributor

Posted by Cursor assistant (model: GPT-5.4) on behalf of the user (Quang Dao) with approval.

Summary

  • validate trace_length and ram_K before verifier size math and allocations
  • bind rw_config, one_hot_config, and dory_layout into Fiat-Shamir
  • return typed verifier errors for missing openings and malformed opening state
  • make opening exhaustiveness always-on, add a Dory runtime guard, and tighten related regressions

Validation

  • cargo fmt -q
  • cargo clippy -p jolt-core --features host --message-format=short -q --all-targets -- -D warnings
  • cargo clippy -p jolt-core --features host,zk --message-format=short -q --all-targets -- -D warnings
  • cargo nextest run -p jolt-core verifier_ --cargo-quiet --features host
  • cargo nextest run -p jolt-core verifier_ --cargo-quiet --features host,zk
  • cargo nextest run -p jolt-core muldiv --cargo-quiet --features host
  • cargo nextest run -p jolt-core muldiv --cargo-quiet --features host,zk
  • cargo nextest run -p jolt-core advice_e2e_dory --cargo-quiet --features host

Copy link
Copy Markdown
Collaborator

@0xAndoroid 0xAndoroid left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code review: 5 findings (2 medium, 3 low). Net positive PR for security — adds boundary validation, Fiat-Shamir binding, typed errors, and always-on exhaustiveness. Findings are defense-in-depth improvements, not exploitable vulnerabilities.

// Verify unified address (these should hold by construction after Stage 2 alignment).
debug_assert_eq!(r_address_raf, r_address_rw);
debug_assert_eq!(r_address_raf, r_address_val);
assert_eq!(r_address_raf, r_address_rw);
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Score 50/100 — Medium] Interaction with record_missing_opening dummy values.

Upgrading debug_assert_eq!assert_eq! is the right call for release-mode safety. However, record_missing_opening (opening_proof.rs:654) now returns dummy all-zero points when an opening is missing. If a malformed proof is missing one of the three RamRa openings (but not all three), the dummy's all-zero r_address won't match the real openings' r_address, causing this assert_eq! to panic before take_missing_opening_error() gets a chance to surface the typed MissingOpening error.

The verifier still safely rejects (panic = rejection), but this violates the intent of the deferred error pattern introduced in this PR. In practice, the three RamRa openings are populated by stages 2-4, and take_missing_opening_error() after each stage would catch them first — so this is only reachable if sumcheck verification in stages 2-4 somehow succeeds with dummy values.

Consider either:

  • Guarding with a fallible check (if r_address_raf != r_address_rw { ... }) that returns a dummy Self so take_missing_opening_error() can surface the real error, or
  • Adding a comment that this path is unreachable due to inter-stage error checks

"inconsistent duplicate opening claims: {key:?} vs {existing_id:?}"
));
}
return;
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Score 50/100 — Medium] Defense-in-depth: inconsistent opening leaves stale value accessible.

When inconsistent duplicate claims are detected, this records the MalformedProof error and returns without inserting or aliasing the new key. The original opening (at existing_id) remains in the accumulator with its first-seen claim value.

This is sound — take_missing_opening_error() catches the MalformedProof after the stage, and sumcheck/Fiat-Shamir binding independently rejects. However, as defense-in-depth, consider also poisoning the existing opening so that any subsequent get_* for either key triggers record_missing_opening:

// After recording malformed error:
self.openings.remove(&existing_id);

This ensures the verifier never uses a claim value from a proof with internally inconsistent openings, even within a single stage.

pub fn acquire_runtime_guard() -> DoryRuntimeGuard {
let mutex = DORY_RUNTIME_GUARD.get_or_init(|| Mutex::new(()));
DoryRuntimeGuard {
_guard: mutex.lock().unwrap(),
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Score 25/100 — Low] unwrap() on mutex lock — poisoning propagation.

If a thread panics while holding DoryRuntimeGuard, the mutex is poisoned and all future acquire_runtime_guard() calls will also panic. This is arguably correct (a panic during proving indicates a logic error), but it makes the process permanently broken rather than allowing recovery.

Consider lock().unwrap_or_else(|e| e.into_inner()) to recover from poisoned state, or use parking_lot::Mutex which doesn't support poisoning.

if missing.is_none() {
*missing = Some(key);
}
let dummy_len = self.log_T.max(1) + 128;
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Score 25/100 — Low] Magic number 128 in dummy point length.

The + 128 ensures the dummy point is long enough for any downstream split_at(log_K) call (since LOG_K for RV64 is at most 128). Consider documenting this derivation or using a named constant to make the intent clear and prevent it from silently becoming wrong if max address-space sizes change.

use ark_bn254::Fr;

#[test]
fn verifier_accumulator_reports_missing_opening() {
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Score 25/100 — Low] Missing test coverage for MalformedProof path.

This test exercises the MissingOpening error path via record_missing_opening. Consider adding a companion test for the MalformedProof path — triggered by inserting two openings at the same point with different claims via populate_or_alias_opening (line 728). This would exercise the priority ordering in take_missing_opening_error() where MalformedProof takes precedence over MissingOpening.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants