# 2024-01-16 zk hack IV geometry puzzle 1 notes links: - [GitHub - ZK-Hack/puzzle-gamma-ray](https://github.com/ZK-Hack/puzzle-gamma-ray) - [my github repo](https://github.com/thor314/puzzle-gamma-ray/tree/main) - [mnt paper](https://eprint.iacr.org/2020/351.pdf) *A log of my thoughts while solving ZK Hack IV puzzle 1*. *initial pass notes and unpacking ConstraintSynthesizer are quite messy, but remain here for posterity. Skip to header [[#in review]] for the "knowledge clean-up" phase of the log* ## Initial pass notes Based on Zcash private transaction design and Mina chain compression. Alice is able to double spend. Guess: something in the recursion system over MNT7653exposes the key used for spending, or allows her otherwise to forge a new spending key. We will generate a faulty nullifier and secret, that satisfy *the same tree proof* for the merkle tree leaf at index 2. ### reading the code They define a Merkle Tree with some properties. Odds are, there isn't a bug in the merkle tree or hash implementation, but ya never know. vaguely hinted as suspicious secret and nullifier: ```rust type ConstraintF = MNT4BigFr; struct SpendCircuit { pub leaf_params: <LeafH as CRHScheme>::Parameters, pub two_to_one_params: <LeafH as CRHScheme>::Parameters, pub root: <CompressH as TwoToOneCRHScheme>::Output, pub proof: Path<MntMerkleTreeParams>, pub secret: ConstraintF, pub nullifier: ConstraintF, } ``` - construct the merkle tree from the attached serialized data - data stored uncompressed unchecked, and should match MNT768 - *is the leaked secret in the set of leaves*? - not directly - we're using groth16 proving over MNT4_753 - groth16 vk pk constructed from proof_keys.bin - we specify our own custom params for poseidon - we shouldn't have to, and that's weird, how were those params chosen - if they're poorly chosen, we may be able to find a hash collision, and therefore double-spend - nullifier constructed from our custom params and the leaked_secret - tree constructed - this looks possibly sketch: ```rust let tree = MntMerkleTree::new( &leaf_crh_params, &leaf_crh_params, // repeat? leaves.iter().map(|x| x.as_slice()), ) ``` - we generate a merkle-inclusion-proof for leaf 2--and check that it verifies - we construct a SpendCircuit, to spend the leaf (zcash specific) - I'm pretty foggy on how all that nullifier stuff works, would be worth a refresh - The circuit is specified over trait `ConstraintSynthesizer`, i.e. we can pass it to groth - we prove the spend circuit with groth16 - we check that the groth proof verifes - now it's our turn, to generate a verifying groth16 proof that we have a fake nullifier and secret for. ### Poseidon check that the parameters are correct, though too few rounds, or incorrect params seem unlikely to be the source of the vuln; still, they specified a configuration of Poseidon, so not impossible a vuln lives here From https://zips.z.cash/protocol/protocol.pdf#poseidonhash, also see daira's [pasta-hadeshash](https://github.com/daira/pasta-hadeshash/tree/master/code) - n_rounds = 8 - partial_rounds = 56 - **diff; partial_rounds = 29** - alpha = 5 - **diff; alpha = 17** - poseidon in sponge configuration - constant input length mode - mds matrix and round constants specified in daira's `calc_round_numbers.py` a couple differences, minor sus, check more later, look at daira's param gen script and check poseidon docs for more; also see [arkworks src](https://github.com/arkworks-rs/crypto-primitives/tree/main/src/sponge) ### skim review We found that we need to generate a faulty null/secret pair for leaf at index 2 in the merkle tree pair. These are not used to generate the merkle inclusion proof, so it seems unlikely that there is a bug in the hash function implementation. It seems more likely that then, that our bug lies in our Constraint system. We should try to understand how the nullifer and secret are spent, which should give hints about how to forge new ones. We also don't much remember how nullifiers are used, so hit a recap if the constraint review fails to turn much up. ## unpacking ConstraintSynthesizer everything here looks pretty boilerplate. That leaves to look at MNT and Poseidon, and investigating what precisely is proved. recall that the nullifier is the hash defined over the `private_spending_key`, the shielded address, and the notes (UTXO model) that the user would spend. If we can construct a fake nullifier, then we must be able to find a hash pre-image. There must be something the issue with using MNT for the curve, i.e. maybe too small field or something. Or else, maybe there is some convenient structure in MNT / Poseidon that we can exploit (the pairing). Let's find exactly how the nullifier is created and used. ### nullifier creation ```rust let ie$ullifier = <LeafH as CRHScheme>::evaluate(&leaf_crh_params, vec![leaked_secret]).unwrap(); // where type LeafH = poseidon::CRH<ConstraintF>; // implements the hash type ConstraintF = MNT4BigFr; // where in ark crypto primitives: /// Interface to CRH. Note that in this release, while all implementations of `CRH` have fixed length, /// variable length CRH may also implement this trait in future. pub trait CRHScheme { type Input: ?Sized; type Output: Clone + Eq + Debug + Hash + Default type Parameters: Clone; fn setup<R: Rng>(r: &mut R) -> Result<Self::Parameters, Error>; fn evaluate<T: Borrow<Self::Input>>( parameters: &Self::Parameters, input: T, ) -> Result<Self::Output, Error>; } // and: fn evaluate( parameters: &Self::ParametersVar, input: &Self::InputVar, ) -> Result<Self::OutputVar, SynthesisError> { let cs = input.cs(); if cs.is_none() { let mut constant_input = Vec::new(); for var in input.iter() { constant_input.push(var.value()?); } Ok(FpVar::Constant( CRH::<F>::evaluate(&parameters.parameters, constant_input).unwrap(), )) } else { let mut sponge = PoseidonSpongeVar::new(cs, &parameters.parameters); sponge.absorb(&input)?; let res = sponge.squeeze_field_elements(1)?; Ok(res[0].clone()) } } // restated from top: let nullifier_in_circuit = <LeafHG as CRHSchemeGadget<LeafH, _>>::evaluate(&leaf_crh_params_var, &[secret])?; ``` if no input cs: - push the values of input into a vector - pass evaluation to CRH with params and constant input else: - init sponge with the cs and params - absorb the input - squeeze the hash output and return the output do we have a cs? base: mnt6 G1var ### nullifier usage The nullifier is consumed by the `SpendCircuit`. We have: ```rust fn prove<C: ConstraintSynthesizer<E::ScalarField>, R: RngCore>( pk: &Self::ProvingKey, circuit: C, rng: &mut R, ) -> Result<Self::Proof, Self::Error> { Self::create_random_proof_with_reduction(circuit, pk, rng) } /// Create a Groth16 proof that is zero-knowledge using the provided /// R1CS-to-QAP reduction. /// This method samples randomness for zero knowledges via `rng`. #[inline] pub fn create_random_proof_with_reduction<C>( circuit: C, pk: &ProvingKey<E>, rng: &mut impl Rng, ) -> R1CSResult<Proof<E>> where C: ConstraintSynthesizer<E::ScalarField>, { // the zk parts, zero if no zk; let r = E::ScalarField::rand(rng); let s = E::ScalarField::rand(rng); Self::create_proof_with_reduction(circuit, pk, r, s) } /// Create a Groth16 proof using randomness `r` and `s` and the provided /// R1CS-to-QAP reduction. #[inline] pub fn create_proof_with_reduction<C>( circuit: C, pk: &ProvingKey<E>, r: E::ScalarField, s: E::ScalarField, ) -> R1CSResult<Proof<E>> where E: Pairing, C: ConstraintSynthesizer<E::ScalarField>, QAP: R1CSToQAP, { let cs = ConstraintSystem::new_ref(); // Set the optimization goal cs.set_optimization_goal(OptimizationGoal::Constraints); // Synthesize the circuit. circuit.generate_constraints(cs.clone())?; debug_assert!(cs.is_satisfied().unwrap()); cs.finalize(); let h = QAP::witness_map::<E::ScalarField, D<E::ScalarField>>(cs.clone())?; let prover = cs.borrow().unwrap(); let proof = Self::create_proof_with_assignment( pk, r, s, &h, &prover.instance_assignment[1..], &prover.witness_assignment, )?; Ok(proof) } ``` ## in review We know a few things: - curves: we're using the MNT4/6 cycle of curves for our nullifier, which support a pairing function. Zcash uses the BLS12-381 (pairing-supporting) curves for the nullifier argument. No actually, they use Jub-jub for this, which is pairing-unfriendly. - ~~both are pairing friendly~~. - MNT embedding degree 4 and 6, ~~while the BLS curves have embedding degree 12. Larger embedding degree means less efficient pairing computation, and a harder DLP~~. - ~~BLS has a smaller field size~~. - nullifier argument: - $N:= H(sk,r)$ where N is the nullifier, H the poseidon hash, r a random nonce, and sk the secret key - It does not look like there is a random nonce included included in the hash eval; we see `LEAFH::evaluate(&leaf_crh_params, [leaked_secret])`, where leaf params are just the poseidon config, and leaked secret is the secret key. - the zcash-style proof should show: - knowledge of (sk, r) such that the nullifier hash is correct - knowledge of (v,a,r) such that H(v,a,r)=C - that the coin exists - v the note's value, a the address, C a commitment to the coin's existence - that nullifier N has not already been published - Poseidon is an algebraic hash function used in zk circuits. Its parameter selection here looks a little different from the parameters that Zcash selected, though a vuln in Poseidon parameter selection would be surprising to me, given the hints. Two differences noted in param selection, from the zcash spec: - partial_rounds = 56 - **diff; partial_rounds = 29** - alpha = 5 - **diff; alpha = 17** - didn't check the vector of raw values, or the MDS matrix - Groth16 - the only element of the Groth16 proving system that factors in here is the specification of the SpendCircuit, so it seems unlikely that we'll find any Groth16-related bugs. The circuit checks: - outputvar from root - paramsvar's for leaf_params and two_to_one_params (which are the same) - fpvar witness for secret - outputvar from nullifier - g1var constant for g1 generator - pathvar witness for proof - to construct leaf_g: - assign g1var constant for G1 generator (base) - construct public key from secret key - leaf_g is the public key - assert that: - secret < MNT6's modulus - nullifier hash is correctly calculated - leaf_g lies in the merkle tree at index 2 - recall leaf_g = g1_generator * secret - Shape of the problem, we have: - a merkle tree, with the target leaked secret at index 2, configured to hash with poseidon over the MNT4BigFr Field - a nullifier constructed from the hash of the leaked secret - we want to construct a cheater-secret such that: - secret < MNT6's modulus - nullifier hash is correctly calculated: - `N == LeafHG::evaluate(&params, &[my_secret])?;` - leaf_g lies in the merkle tree at index 2 - recall `leaf_g = (g1_generator * my_secret).x` - in other words, we have: want construct a secret that obtains a hash collision: - `h(params, cheat_secret) == h(params, secret)` ``` root / \ h(h0,h1) h(h2,h3) | | | | h0 h1 h2 h3 (this row: leaves.bin) | | | | l0 l1 l2 l3 ^(leaked_secret.bin) ``` Issue: how are we going to construct a hash collision? [hint 1](https://twitter.com/__zkhack__/status/1747574583538925572) updated: see zcash spec lemma 5.4.7 for bob's reasoning on why to only use the x coordinate when storing public keys. **Lemma 5.4.7**. Let $P=(u,v) \in \mathbb J^{(r)}.$ Then $(u,-v) \not \in \mathbb J^{(r)}$. - initial thought: the hint suggests that the x coordinate for the point on the chosen curve may not be unique, i.e. that for $P=(x,y)$, there may exist $y'$ such that $Q=(x,y')$. Then we would have: - a new nullifier: $N=H(s)$ and $N'=H(s')$ - but with leaf: $l=(s'G).x=(sG).x$, such that the merkle proof verifies correctly. - by the hint, it seems likely that the point we want is $s'G=(x,-y)$. Given leaked secret $s$ such that $k=(sG).x$, we want to obtain $s'$ such that: $$k'=(s'G).x=(x,-y).x = x = (x,y).x = (sG).x =k$$ Is it possible that $(-s)G=(x,-y)$? Seems unlikely. Checks: nope. Let's read the proof very carefully. It's not immediately obvious how we will peel off $s'$, i.e. solve the discrete log problem. Jubjub, the zcash curve which the lemma describes, does not have a pairing. Can we exploit the pairing? $$e(s'*G_1, G_2)=e(G_1, s'*G_2)= s'*e(G_1,G_2)=s'G_T$$ Maybe if solving the discrete log problem in $G_T$ or $G_2$ is easy, but still, that feels unlikely to be it. But Jubjub isn't pairing friendly; mnt4/6 is, so that feels like a big hint that we just haven't figured out how to use yet. Might be worth throwing an hour at the whiteboard. Still, we've made some progress. The state of the problem is now: - we want to obtain $s'$ such that $s'G=(x,-y).x$ where $(x,y).x=sG$. Solving for $s'$ directly would involve solving the discrete log problem. - we're pretty sure that there's an exploit on the pairing somehow to help us solve for $s'$. **Lemma 5.4.7**. Let $P=(u,v) \in \mathbb J^{(r)}.$ Then $(u,-v) \not \in \mathbb J^{(r)}$ (subgroup of Jubjub of order r). Proof: - if P is the point at infinity (u,v)=(0,1), but -P=(0,-1) which does not lie on the curve. - all other points P have odd order. - further, $v\ne 0$. if v=0, then $au^2=1$ then $[2]P=(0,-1)$ then $[2]([2]P)=(0,1)=O$, which would have even order. - *unsure what the $au^2=1$ argument is saying. $a$ is part of the curve equation, $y^2=x^3 +ax + b$*. Check: $0=u^3+au+b$--nope. Maybe there's another curve representation they're working over, something twisted-ed related. Oh, u,v denotes twisted edwards notation. - if $v\ne 0$ then $v\ne -v$. - Let $Q=(u,-v)$ be a point on the curve. We will show $Q=-P$ is a contradiction. - Then $[2]Q=-[2]P=[2](-P)$, but $Q.v=-P.v$ is contradiction since $-v \ne v$ - *what? Should expand on that* - Therefore either $Q=-P$ or else doubling is not injective on the curve, which contradicts the curve's odd order. Hint 2 released: > Note that the MNT curves are represented in Weierstrass from in the circuit, and use the fact that both (x,y) and (x,-y) are valid points for spending Which confirms my suspicion that we want $s'=(x,-y)$. Let's find it. - $P=sG=(x,y)$ - $-P=O-P=O-sG=s'G=(x,-y)$ We observe that for the order $n$ of generator $G$, we have $nG=O$, therefore: $$\begin{align} s'G &= O-sG = nG-sG\\ &=(n-s)G\\ \therefore s'&=(n-s) \end{align}$$ However, note that $s$ lives in the `mnt4::Fr` field, but the order $n$ of generator $G$ will live in `mnt4::Fp`, so we'll have to do a type conversion.