From 44758846c44c5d7950fa83554d2a453c8bf2129f Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Thu, 17 Aug 2023 11:29:22 +0800 Subject: [PATCH] fix soundness: use last_augmented_circuit_index consistently --- src/gadgets/r1cs.rs | 23 ++++++ src/supernova/circuit.rs | 149 ++++++++++++++++++++++----------------- src/supernova/utils.rs | 77 ++++++++++++-------- 3 files changed, 154 insertions(+), 95 deletions(-) diff --git a/src/gadgets/r1cs.rs b/src/gadgets/r1cs.rs index 3d41f33d..4ab4ddf9 100644 --- a/src/gadgets/r1cs.rs +++ b/src/gadgets/r1cs.rs @@ -385,6 +385,29 @@ pub fn conditionally_select_alloc_relaxed_r1cs< Ok(c) } +/// c = cond ? a: b, where a, b: vec[AllocatedRelaxedR1CSInstance] +pub fn conditionally_select_vec_allocated_relaxed_r1cs_instance< + G: Group, + CS: ConstraintSystem<::Base>, +>( + mut cs: CS, + a: &[AllocatedRelaxedR1CSInstance], + b: &[AllocatedRelaxedR1CSInstance], + condition: &Boolean, +) -> Result>, SynthesisError> { + a.iter() + .enumerate() + .zip(b.iter()) + .map(|((i, a), b)| { + a.conditionally_select( + cs.namespace(|| format!("cond ? a[{}]: b[{}]", i, i)), + b, + condition, + ) + }) + .collect::>, _>>() +} + /// c = cond ? a: b, where a, b: AllocatedPoint pub fn conditionally_select_point::Base>>( mut cs: CS, diff --git a/src/supernova/circuit.rs b/src/supernova/circuit.rs index 13beb5d9..53424551 100644 --- a/src/supernova/circuit.rs +++ b/src/supernova/circuit.rs @@ -17,7 +17,9 @@ use crate::{ gadgets::{ ecc::AllocatedPoint, r1cs::{ - conditionally_select_alloc_relaxed_r1cs, AllocatedR1CSInstance, AllocatedRelaxedR1CSInstance, + conditionally_select_alloc_relaxed_r1cs, + conditionally_select_vec_allocated_relaxed_r1cs_instance, AllocatedR1CSInstance, + AllocatedRelaxedR1CSInstance, }, utils::{ alloc_const, alloc_num_equals, alloc_scalar_as_base, alloc_zero, conditionally_select_vec, @@ -155,8 +157,6 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC ), SynthesisError, > { - // NOTE `last_augmented_circuit_index` could just be aux without any constraint. - // The reason is prover can only produce valid running instance by folding u into correct U_i[last_augmented_circuit_index] let last_augmented_circuit_index = AllocatedNum::alloc(cs.namespace(|| "last_augmented_circuit_index"), || { Ok(self.inputs.get()?.last_augmented_circuit_index) @@ -253,7 +253,7 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC &self, mut cs: CS, u: AllocatedR1CSInstance, - last_augmented_circuit_index: &AllocatedNum, + last_augmented_circuit_index_checked: &AllocatedNum, num_augmented_circuits: usize, ) -> Result>, SynthesisError> { let mut cs = cs.namespace(|| "alloc U_i default"); @@ -282,7 +282,7 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC let equal_bit = Boolean::from(alloc_num_equals( cs.namespace(|| format!("check equal bit {:?}", i)), &i_alloc, - last_augmented_circuit_index, + last_augmented_circuit_index_checked, )?); let default = &AllocatedRelaxedR1CSInstance::default( cs.namespace(|| format!("Allocate U_default {:?}", i)), @@ -318,7 +318,14 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC last_augmented_circuit_index: &AllocatedNum, program_counter: Option>, num_augmented_circuits: usize, - ) -> Result<(AllocatedRelaxedR1CSInstance, AllocatedBit), SynthesisError> { + ) -> Result< + ( + AllocatedNum, + Vec>, + AllocatedBit, + ), + SynthesisError, + > { // Check that u.x[0] = Hash(params, i, program_counter, U[], z0, zi) let mut ro = G::ROCircuit::new( self.ro_consts.clone(), @@ -353,7 +360,7 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC )?; // Run NIFS Verifier - let U_to_fold = get_from_vec_alloc_relaxed_r1cs( + let (last_augmented_circuit_index_checked, U_to_fold) = get_from_vec_alloc_relaxed_r1cs( cs.namespace(|| "U to fold"), U, last_augmented_circuit_index, @@ -368,7 +375,31 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC self.params.n_limbs, )?; - Ok((U_fold, check_pass)) + // update AllocatedRelaxedR1CSInstance on index match augmented circuit index + let U_next: Vec> = U + .iter() + .enumerate() + .map(|(i, U)| { + let mut cs = cs.namespace(|| format!("U_i+1 non_base conditional selection {:?}", i)); + let i_alloc = alloc_const( + cs.namespace(|| "i allocated"), + scalar_as_base::(G::Scalar::from(i as u64)), + )?; + let equal_bit = Boolean::from(alloc_num_equals( + cs.namespace(|| "check equal bit"), + &i_alloc, + &last_augmented_circuit_index_checked, + )?); + conditionally_select_alloc_relaxed_r1cs( + cs.namespace(|| "select on index namespace"), + &U_fold, + U, + &equal_bit, + ) + }) + .collect::>, _>>()?; + + Ok((last_augmented_circuit_index_checked, U_next, check_pass)) } } @@ -377,6 +408,24 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC self, cs: &mut CS, ) -> Result<(AllocatedNum, Vec>), SynthesisError> { + // NOTE `last_augmented_circuit_index` is aux without any constraint. + // Reason is prover can only produce valid running instance by folding u into proper U_i[last_augmented_circuit_index] + // However, there is crucial pre-asumption: `last_augmented_circuit_index` must within range [0, num_augmented_circuits) + // otherwise there will be a soundness error, such that maliculous prover can choose out of range last_augmented_circuit_index. + // The soundness error depends on how we process out-of-range condition. + // + // there are 2 possible solution + // 1. range check `last_augmented_circuit_index` + // 2. if last_augmented_circuit_index out of range, then by default select index 0 + // + // For current version we choose 2, due to its simplicify and fit well in last_augmented_circuit_index use case. + // Recap, the only way to pass running instance check is folding u into respective U_i[last_augmented_circuit_index] + // So, a circuit implementing to set out-of-range last_augmented_circuit_index to index 0 is fine. + // The illegal running instances will be propogate to later phase and finally captured with "high" probability on the basis of Nova IVC security. + // + // Although above "informal" analysis implies there is no `malleability` on statement (malleability refer `NARK.8 Malleability of Nova’s IVC` https://eprint.iacr.org/2023/969.pdf ) + // We need to carefully check whether it lead to other vulnerability. + let arity = self.step_circuit.arity(); let num_augmented_circuits = if self.params.is_primary_circuit { // primary circuit only fold single running instance with secondary output strict r1cs instance @@ -418,55 +467,33 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC let zero = alloc_zero(cs.namespace(|| "zero"))?; let is_base_case = alloc_num_equals(cs.namespace(|| "Check if base case"), &i.clone(), &zero)?; - // Synthesize the circuit for the base case and get the new running instances - let Unew_base = self.synthesize_base_case( - cs.namespace(|| "base case"), - u.clone(), - &last_augmented_circuit_index, - num_augmented_circuits, - )?; - // Synthesize the circuit for the non-base case and get the new running // instances along with a boolean indicating if all checks have passed - let (Unew_non_base_folded, check_non_base_pass) = self.synthesize_non_base_case( - cs.namespace(|| "synthesize non base case"), - params.clone(), - i.clone(), - z_0.clone(), - z_i.clone(), - &U, + // must use return `last_augmented_circuit_index_checked` since it got range checked + let (last_augmented_circuit_index_checked, U_next_non_base, check_non_base_pass) = self + .synthesize_non_base_case( + cs.namespace(|| "synthesize non base case"), + params.clone(), + i.clone(), + z_0.clone(), + z_i.clone(), + &U, + u.clone(), + T, + arity, + &last_augmented_circuit_index, + program_counter.clone(), + num_augmented_circuits, + )?; + + // Synthesize the circuit for the base case and get the new running instances + let U_next_base = self.synthesize_base_case( + cs.namespace(|| "base case"), u.clone(), - T, - arity, - &last_augmented_circuit_index, - program_counter.clone(), + &last_augmented_circuit_index_checked, num_augmented_circuits, )?; - // update AllocatedRelaxedR1CSInstance on index match augmented circuit index - let Unew_non_base: Vec> = U - .iter() - .enumerate() - .map(|(i, U)| { - let mut cs = cs.namespace(|| format!("U_i+1 non_base conditional selection {:?}", i)); - let i_alloc = alloc_const( - cs.namespace(|| "i allocated"), - scalar_as_base::(G::Scalar::from(i as u64)), - )?; - let equal_bit = Boolean::from(alloc_num_equals( - cs.namespace(|| "check equal bit"), - &i_alloc, - &last_augmented_circuit_index, - )?); - conditionally_select_alloc_relaxed_r1cs( - cs.namespace(|| "select on index namespace"), - &Unew_non_base_folded, - U, - &equal_bit, - ) - }) - .collect::>, _>>()?; - // Either check_non_base_pass=true or we are in the base case let should_be_false = AllocatedBit::nor( cs.namespace(|| "check_non_base_pass nor base_case"), @@ -480,19 +507,13 @@ impl<'a, G: Group, SC: StepCircuit> SuperNovaAugmentedCircuit<'a, G, SC |lc| lc, ); - // Compute the U_new - let U_next = Unew_non_base - .iter() - .enumerate() - .zip(Unew_base.iter()) - .map(|((i, Unew_non_base), Unew_base)| { - Unew_base.conditionally_select( - cs.namespace(|| format!("compute U_new {:?}", i)), - Unew_non_base, - &Boolean::from(is_base_case.clone()), - ) - }) - .collect::>, _>>()?; + // Compute the U_next + let U_next = conditionally_select_vec_allocated_relaxed_r1cs_instance( + cs.namespace(|| "U_next"), + &U_next_base[..], + &U_next_non_base[..], + &Boolean::from(is_base_case.clone()), + )?; // Compute i + 1 let i_next = AllocatedNum::alloc(cs.namespace(|| "i + 1"), || { diff --git a/src/supernova/utils.rs b/src/supernova/utils.rs index a5bad84d..26bf583b 100644 --- a/src/supernova/utils.rs +++ b/src/supernova/utils.rs @@ -3,7 +3,7 @@ use bellpepper_core::{boolean::Boolean, num::AllocatedNum, ConstraintSystem, Syn use crate::{ gadgets::{ r1cs::{conditionally_select_alloc_relaxed_r1cs, AllocatedRelaxedR1CSInstance}, - utils::{alloc_const, alloc_num_equals, scalar_as_base}, + utils::{alloc_const, alloc_num_equals, conditionally_select}, }, traits::Group, }; @@ -16,36 +16,51 @@ pub fn get_from_vec_alloc_relaxed_r1cs], target_index: &AllocatedNum, -) -> Result, SynthesisError> { +) -> Result<(AllocatedNum, AllocatedRelaxedR1CSInstance), SynthesisError> { let mut a = a.iter().enumerate(); - let first = a - .next() - .ok_or_else(|| SynthesisError::IncompatibleLengthVector("empty vec length".to_string()))? - .1 - .clone(); - let selected = - a.try_fold::, _, _>(first, |matched, (i, candidate)| { - let i_const = alloc_const( - cs.namespace(|| format!("i_const {:?} allocated", i)), - scalar_as_base::(G::Scalar::from(i as u64)), - )?; - let equal_bit = Boolean::from(alloc_num_equals( - cs.namespace(|| format!("check {:?} equal bit", i_const.get_value().unwrap())), - &i_const, - target_index, - )?); - let next_matched = conditionally_select_alloc_relaxed_r1cs( - cs.namespace(|| { - format!( - "select on index namespace {:?}", - i_const.get_value().unwrap() - ) - }), - candidate, - &matched, - &equal_bit, - )?; - Ok::, SynthesisError>(next_matched) - })?; + let first = ( + alloc_const(cs.namespace(|| "i_const 0 allocated"), G::Base::from(0u64))?, + a.next() + .ok_or_else(|| SynthesisError::IncompatibleLengthVector("empty vec length".to_string()))? + .1 + .clone(), + ); + let selected = a.try_fold(first, |matched, (i, candidate)| { + let i_const = alloc_const( + cs.namespace(|| format!("i_const {:?} allocated", i)), + G::Base::from(i as u64), + )?; + let equal_bit = Boolean::from(alloc_num_equals( + cs.namespace(|| format!("check {:?} equal bit", i_const.get_value().unwrap())), + &i_const, + target_index, + )?); + let next_matched_index = conditionally_select( + cs.namespace(|| { + format!( + "select on index namespace {:?}", + i_const.get_value().unwrap() + ) + }), + &i_const, + &matched.0, + &equal_bit, + )?; + let next_matched_allocated = conditionally_select_alloc_relaxed_r1cs( + cs.namespace(|| { + format!( + "select on index namespace {:?}", + i_const.get_value().unwrap() + ) + }), + candidate, + &matched.1, + &equal_bit, + )?; + Ok::<(AllocatedNum, AllocatedRelaxedR1CSInstance), SynthesisError>(( + next_matched_index, + next_matched_allocated, + )) + })?; Ok(selected) }