diff --git a/noir-examples/basic-4/Nargo.toml b/noir-examples/basic-4/Nargo.toml new file mode 100644 index 000000000..4fc5adbfc --- /dev/null +++ b/noir-examples/basic-4/Nargo.toml @@ -0,0 +1,5 @@ +[package] +name = "basic" +type = "bin" +authors = [""] +compiler_version = ">=0.22.0" diff --git a/noir-examples/basic-4/Prover.toml b/noir-examples/basic-4/Prover.toml new file mode 100644 index 000000000..b7a496768 --- /dev/null +++ b/noir-examples/basic-4/Prover.toml @@ -0,0 +1,2 @@ +a = "5" +b = "3" diff --git a/noir-examples/basic-4/src/main.nr b/noir-examples/basic-4/src/main.nr new file mode 100644 index 000000000..cf5106503 --- /dev/null +++ b/noir-examples/basic-4/src/main.nr @@ -0,0 +1,9 @@ +// Basic arithmetic: addition, subtraction, multiplication. +// Proves knowledge of (a, b) such that (a + b) * (a - b) == result. +// Mathematically: result = a^2 - b^2. +// Honest inputs: a = 5, b = 3 -> result = 16. +fn main(a: Field, b: Field) -> pub Field { + let sum = a + b; + let diff = a - b; + sum * diff +} diff --git a/provekit/common/src/prefix_covector.rs b/provekit/common/src/prefix_covector.rs index c7ab3cd72..6989606ce 100644 --- a/provekit/common/src/prefix_covector.rs +++ b/provekit/common/src/prefix_covector.rs @@ -1,3 +1,4 @@ + use { crate::FieldElement, ark_std::{One, Zero}, @@ -167,16 +168,17 @@ pub fn expand_powers(values: &[FieldElement]) -> Vec PrefixCovector { +pub fn make_public_weight(x: FieldElement, num_public_inputs: usize, m: usize) -> PrefixCovector { + let n = num_public_inputs + 1; let domain_size = 1 << m; - let prefix_len = public_inputs_len.next_power_of_two().max(2); + let prefix_len = n.next_power_of_two().max(2); let mut public_weights = vec![FieldElement::zero(); prefix_len]; let mut current_pow = FieldElement::one(); - for slot in public_weights.iter_mut().take(public_inputs_len) { + for slot in public_weights.iter_mut().take(n) { *slot = current_pow; current_pow *= x; } @@ -218,17 +220,19 @@ pub fn compute_alpha_evals( .collect() } -/// Compute the public weight evaluation `⟨[1, x, x², …], poly⟩` without -/// allocating a [`PrefixCovector`]. +/// Compute the public weight evaluation `⟨[1, x, x², …, x^N], poly[0..=N]⟩` +/// without allocating a [`PrefixCovector`]. Covers the R1CS constant at +/// position 0 and `num_public_inputs` public input positions. #[must_use] pub fn compute_public_eval( x: FieldElement, - public_inputs_len: usize, + num_public_inputs: usize, polynomial: &[FieldElement], ) -> FieldElement { + let n = num_public_inputs + 1; let mut eval = FieldElement::zero(); let mut x_pow = FieldElement::one(); - for &p in polynomial.iter().take(public_inputs_len) { + for &p in polynomial.iter().take(n) { eval += x_pow * p; x_pow *= x; } diff --git a/provekit/verifier/src/whir_r1cs.rs b/provekit/verifier/src/whir_r1cs.rs index df3ede792..d0cce37e1 100644 --- a/provekit/verifier/src/whir_r1cs.rs +++ b/provekit/verifier/src/whir_r1cs.rs @@ -149,6 +149,7 @@ impl WhirR1CSVerifier for WhirR1CSScheme { let public_1: FieldElement = arthur .prover_message() .map_err(|_| anyhow::anyhow!("Failed to read public_1"))?; + verify_public_input_binding(public_1, x, public_inputs)?; weights_1.insert(0, make_public_weight(x, public_inputs.len(), self.m)); vec![public_1, evals_1[0], evals_1[1], evals_1[2]] } else { @@ -216,6 +217,7 @@ impl WhirR1CSVerifier for WhirR1CSScheme { let public_eval: FieldElement = arthur .prover_message() .map_err(|_| anyhow::anyhow!("Failed to read public eval"))?; + verify_public_input_binding(public_eval, x, public_inputs)?; weights.insert(0, make_public_weight(x, public_inputs.len(), self.m)); vec![public_eval, evals[0], evals[1], evals[2]] } else { @@ -309,28 +311,23 @@ pub fn run_sumcheck_verifier( }) } -/// Verify that `challenge_eval == Σ xⁱ · challenges[i]`. -/// -/// The prover sends `challenge_eval` as a transcript-bound message, and WHIR -/// verifies that it equals the inner product of `make_challenge_weight(x, …)` -/// with the committed w2 polynomial. This function independently recomputes -/// the expected value from the Fiat-Shamir `challenges` (which the verifier -/// already knows) and checks equality, ensuring the committed w2 polynomial -/// stores the correct challenge values at the declared offsets. -fn verify_challenge_binding( - challenge_eval: FieldElement, +/// Verify that the prover's claimed public evaluation matches the known public +/// inputs. The weight covers positions `[0, 1, ..., N]` where position 0 is the +/// R1CS constant `1` and positions `1..=N` are the public inputs. +fn verify_public_input_binding( + public_eval: FieldElement, x: FieldElement, - challenges: &[FieldElement], + public_inputs: &PublicInputs, ) -> Result<()> { - let mut expected = FieldElement::zero(); - let mut x_pow = FieldElement::one(); - for &ch in challenges { - expected += x_pow * ch; + let mut expected = FieldElement::one(); + let mut x_pow = x; + for &pi in &public_inputs.0 { + expected += x_pow * pi; x_pow *= x; } ensure!( - challenge_eval == expected, - "Challenge binding check failed: prover's challenge_eval does not match expected value" + public_eval == expected, + "Public input binding check failed: expected {expected:?}, got {public_eval:?}" ); Ok(()) } diff --git a/tooling/provekit-bench/tests/compiler.rs b/tooling/provekit-bench/tests/compiler.rs index 8643bcfba..8420588d9 100644 --- a/tooling/provekit-bench/tests/compiler.rs +++ b/tooling/provekit-bench/tests/compiler.rs @@ -86,3 +86,49 @@ pub fn compile_workspace(workspace_path: impl AsRef) -> Result fn case(path: &str) { test_compiler(path); } + +/// Verify that the verifier rejects a proof whose public inputs have been +/// tampered with. +#[test] +fn test_public_input_binding_exploit() { + use provekit_common::{witness::PublicInputs, FieldElement}; + + let test_case_path = Path::new("../../noir-examples/basic-4"); + + compile_workspace(test_case_path).expect("Compiling workspace"); + + let nargo_toml_path = test_case_path.join("Nargo.toml"); + let nargo_toml = std::fs::read_to_string(&nargo_toml_path).expect("Reading Nargo.toml"); + let nargo_toml: NargoToml = toml::from_str(&nargo_toml).expect("Deserializing Nargo.toml"); + let package_name = nargo_toml.package.name; + + let circuit_path = test_case_path.join(format!("target/{package_name}.json")); + let witness_file_path = test_case_path.join("Prover.toml"); + + let schema = NoirProofScheme::from_file(&circuit_path).expect("Reading proof scheme"); + let prover = Prover::from_noir_proof_scheme(schema.clone()); + let mut verifier = Verifier::from_noir_proof_scheme(schema.clone()); + + // Prove honestly (a=5, b=3 -> result = (5+3)*(5-3) = 16) + let mut proof = prover + .prove(&witness_file_path) + .expect("While proving Noir program statement"); + + // Sanity: honest proof should verify + { + let mut honest_verifier = Verifier::from_noir_proof_scheme(schema); + honest_verifier + .verify(&proof) + .expect("Honest proof should verify"); + } + + // Tamper: the committed polynomial encodes result=16 at position 1, but we + // claim result=42. The verifier should reject this. + proof.public_inputs = PublicInputs::from_vec(vec![FieldElement::from(42u64)]); + + let result = verifier.verify(&proof); + assert!( + result.is_err(), + "Verification should fail when public inputs are tampered, but it succeeded", + ); +}