2024-01-16 zk hack IV geometry puzzle 1 notes

links:

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:

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:

  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

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

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

  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:

    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 (s k, 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 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 J^{(r)} .

Then

(u, - v) \notin 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 = (s G) . 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 = (s G) . x

, we want to obtain

s^{'}

such that:

k^{'} = (s^{'} G) . x = (x, - y) . x = x = (x, y) . x = (s G) . 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}

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 = s G$ . 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 J^{(r)} .

Then

(u, - v) \notin 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 \neq 0$ . if v=0, then
  $a u^{2} = 1$ then
  $[2] P = (0, - 1)$ then
  $[2] ([2] P) = (0, 1) = O$ , which would have even order.
  - unsure what the
    $a u^{2} = 1$ argument is saying.
    $a$ is part of the curve equation,
    $y^{2} = x^{3} + a x + b$ . Check:
    $0 = u^{3} + a u + 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 \neq 0$ then
  $v \neq - 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 \neq 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 = s G = (x, y)$
$- P = O - P = O - s G = s^{'} G = (x, - y)$

We observe that for the order

n

of generator

G

, we have

n G = O

, therefore:

\begin{aligned} s^{'} G & = O - s G = n G - s G \\ = (n - s) G \\ ∴ s^{'} & = (n - s) \end{aligned}

However, note that

s

lives in the mnt4::Fr field, but the order

n