ZKHack IV - Puzzl 1 writeup

gistfile1.txt

## 1. Introduction
> Bob was deeply inspired by the Zcash design for private transactions and had some pretty cool ideas on how to adapt it for his requirements. He was also inspired by the Mina design for the lightest blockchain and wanted to combine the two. In order to achieve that, Bob used the MNT7653 cycle of curves to enable efficient infinite recursion, and used elliptic curve public keys to authorize spends. He released a first version of the system to the world and Alice soon announced she was able to double spend by creating two different nullifiers for the same key...

## 2. Understanding the circuit
```
impl ConstraintSynthesizer<ConstraintF> for SpendCircuit {
    fn generate_constraints(
        self,
        cs: ConstraintSystemRef<ConstraintF>,
    ) -> Result<(), SynthesisError> {
        // Allocate Merkle Tree Root
        let root = <LeafHG as CRHSchemeGadget<LeafH, _>>::OutputVar::new_input(
            ark_relations::ns!(cs, "new_digest"),
            || Ok(self.root),
        )?;

        // Allocate Parameters for CRH
        let leaf_crh_params_var =
            <LeafHG as CRHSchemeGadget<LeafH, _>>::ParametersVar::new_constant(
                ark_relations::ns!(cs, "leaf_crh_parameter"),
                &self.leaf_params,
            )?;
        let two_to_one_crh_params_var =
            <CompressHG as TwoToOneCRHSchemeGadget<CompressH, _>>::ParametersVar::new_constant(
                ark_relations::ns!(cs, "two_to_one_crh_parameter"),
                &self.two_to_one_params,
            )?;

        let secret = FpVar::new_witness(ark_relations::ns!(cs, "secret"), || Ok(self.secret))?;
        let secret_bits = secret.to_bits_le()?;

        Boolean::enforce_smaller_or_equal_than_le(&secret_bits, MNT6BigFr::MODULUS)?;

        let nullifier = <LeafHG as CRHSchemeGadget<LeafH, _>>::OutputVar::new_input(
            ark_relations::ns!(cs, "nullifier"),
            || Ok(self.nullifier),
        )?;

        let nullifier_in_circuit =
            <LeafHG as CRHSchemeGadget<LeafH, _>>::evaluate(&leaf_crh_params_var, &[secret])?;
        nullifier_in_circuit.enforce_equal(&nullifier)?;

        let base = G1Var::new_constant(ark_relations::ns!(cs, "base"), G1Affine::generator())?;
        let pk = base.scalar_mul_le(secret_bits.iter())?.to_affine()?;
        // Allocate Leaf
        let leaf_g: Vec<_> = vec![pk.x];

        // Allocate Merkle Tree Path
        let cw: PathVar<MntMerkleTreeParams, ConstraintF, MntMerkleTreeParamsVar> =
            PathVar::new_witness(ark_relations::ns!(cs, "new_witness"), || Ok(&self.proof))?;

        cw.verify_membership(
            &leaf_crh_params_var,
            &two_to_one_crh_params_var,
            &root,
            &leaf_g,
        )?
        .enforce_equal(&Boolean::constant(true))?;

        Ok(())
    }
}
```
The circuit's flow is as follows
1. The circuit starts by allocating a Merkle Tree root.
2. Then, parameters for a Collision-Resistant Hash (CRH) function are allocated. leaf_crh_params_var for leaf nodes and two_to_one_crh_params_var for intermediate node hashing.
3. A secret value is introduced as a witness in the circuit. This secret is crucial for the generation of a nullifier and a public key. 
4. A nullifier is allocated and calculated using the CRH function with the secret.
5. A public key is generated from the secret. This involves scalar multiplication of a base point with the secret's bits.
6. The X-coordinate of the resulting elliptic curve point is used to form a leaf node.
7. A Merkle Tree path is allocated for the newly created leaf node.
8. The circuit then performs a membership verification to confirm that the leaf node, created from the public key, is part of the Merkle Tree with the specified root.

```mermaid
graph TD
    A[Start] -->|Allocate Merkle Tree Root| B[Merkle Tree Root]
    B -->|Allocate CRH Parameters| C[Leaf CRH Parameters]
    B -->|Allocate CRH Parameters| D[Two-to-One CRH Parameters]
    C -->|Allocate Secret| E[Secret]
    D -->|Allocate Nullifier| F[Nullifier]
    E -->|Convert Secret to Bits| G[Secret Bits]
    G -->|Check Secret Size| H[Secret Size Check]
    H -->|Compute Nullifier in Circuit| I[Nullifier in Circuit]
    I -->|Verify Nullifier Consistency| F
    G -->|Generate Public Key| J[Public Key]
    J -->|Create Leaf Node| K[Leaf Node]
    K -->|Allocate Merkle Tree Path| L[Merkle Tree Path]
    L -->|Verify Merkle Tree Membership| M[Membership Verification]
    M -->|End| N[Verification Successful]
```

### 3. Requirements to Pass Verification in circuit
- Secret Size: The secret must be of an appropriate size (smaller than the MNT6BigFr::MODULUS).
- Nullifier Consistency: The computed nullifier must match the input nullifier.
- Merkle Tree Membership: The leaf created must correctly correspond to a valid path in the Merkle Tree with the given root.

### 4. Verification of valid inputs
First, a random number is generated for Groth16 ZK proof
```
let rng = &mut ark_std::rand::rngs::StdRng::seed_from_u64(0u64);
```

Next, tree's leaves and path data, Proving Key and Verifying key are loaded with from_file function. Its worth noting that all the data using the MNT4_753 curve.
```
let leaves: Vec<Vec<MNT4BigFr>> = from_file("./leaves.bin");
    let leaked_secret: MNT4BigFr = from_file("./leaked_secret.bin");
    let (pk, vk): (
        <Groth16<MNT4_753> as SNARK<MNT4BigFr>>::ProvingKey,
        <Groth16<MNT4_753> as SNARK<MNT4BigFr>>::VerifyingKey,
    ) = from_file("./proof_keys.bin");
```

The CRH params for leaves and intermediate nodes are using poseidon parameters and the node number we are proving is 2. The nullifier is generated by hashing the secret value. 
```
let leaf_crh_params = poseidon_parameters::poseidon_parameters();
    let i = 2;
    let two_to_one_crh_params = leaf_crh_params.clone();

    let nullifier = <LeafH as CRHScheme>::evaluate(&leaf_crh_params, vec![leaked_secret]).unwrap();
```

root node and proof of second node are calculated and validated. 
```
    let tree = MntMerkleTree::new(
        &leaf_crh_params,
        &two_to_one_crh_params,
        leaves.iter().map(|x| x.as_slice()),
    )
    .unwrap();
    let root = tree.root();
    let leaf = &leaves[i];

    let tree_proof = tree.generate_proof(i).unwrap();
    assert!(tree_proof
        .verify(
            &leaf_crh_params,
            &two_to_one_crh_params,
            &root,
            leaf.as_slice()
        )
        .unwrap());
```

The `leaf_params`, `two_to_one_params`, `two_to_one_crh_params`, `root`, `proof`, `nullifier`, `secret` inputs are set and verify the input with Groth16 verifier.
```
let c = SpendCircuit {
        leaf_params: leaf_crh_params.clone(),
        two_to_one_params: two_to_one_crh_params.clone(),
        root: root.clone(),
        proof: tree_proof.clone(),
        nullifier: nullifier.clone(),
        secret: leaked_secret.clone(),
    };

    let proof = Groth16::<MNT4_753>::prove(&pk, c.clone(), rng).unwrap();

    assert!(Groth16::<MNT4_753>::verify(&vk, &vec![root, nullifier], &proof).unwrap());
```

## 5. Solution Requirement 
We need to find the `nullifier` and `secret` such that the same node and proof can be verified again with valid `leaf_params`, `two_to_one_params`, `root`, `proof` which means trigger double spendig.
```
    assert_ne!(nullifier, nullifier_hack);

    let c2 = SpendCircuit {
        leaf_params: leaf_crh_params.clone(),
        two_to_one_params: two_to_one_crh_params.clone(),
        root: root.clone(),
        proof: tree_proof.clone(),
        nullifier: nullifier_hack.clone(),
        secret: secret_hack.clone(),
    };

    let proof = Groth16::<MNT4_753>::prove(&pk, c2.clone(), rng).unwrap();
```


## 6. Background Knowledges before solve.
### Symmetry About the X-axis of Elliptic Curves
The most commonly used form in elliptic curve cryptography (ECC) is the Weierstrass equation. 
$$
y^2 = x^3 + ax + b
$$
The symmetry about the x-axis can be observed from the equation of the curve itself. If you replace y with -y, the equation becomes 
$$
(-y)^2 = x^3 + ax + b
$$
which simplifies back. This means that for every value of $x$, there are two values of $y$.

### Negative Scalar Multiplication
Negative scalar multiplication involves a negative scalar $-k$ (where $k$ is a positive integer). If you have a point $P$ on the curve, $-kP$ is equivalent to adding the inverse of $P$ to itself $k$ times. In elliptic curves, the inverse of a point $P(x,y)$ is typically $P(x,-y)$.

### Base and Scalar field
Elliptic curves are defined over finite fields. There are two primary types of fields in the context of elliptic curves:
- Base Field: The field over which the elliptic curve is defined. Points on the curve are elements of this field. the coordinates of each point on the curve are elements of $F_p$
- Scalar Field: This field is associated with the order of the curve, which is the number of points on the curve. The scalars (multipliers) in scalar multiplication operations are elements of this field.

### MNT4 and MNT6 curve
The MNT4's base field is equal to MNT6's scalar field and the MNT4's scalar field is equal to base field of MNT6. [ref](https://docs.rs/ark-mnt6-753/latest/ark_mnt6_753/)


## 7. Triggering Strategy
We can use symmetry of elliptic curve to generate `hacked_secret` because the leaf that is going to be validated is selected by $x$ value of affine, we can generate pk that is inverse of valid $P$.
```
let leaf_g: Vec<_> = vec![pk.x];
```

We need the `hacked_secret` value less than MNT6's modulus value. As the MNT4's Base field is equal to MNT6's scalar field, we can bypass this check by setting `hacked_secret` into MNT6 and then convert into MNT4 input. As the value is a multiplier of scalar multiplication, it will used as MNT6 field because the circuit is set to MNT4 configuration.
```
Boolean::enforce_smaller_or_equal_than_le(&secret_bits, MNT6BigFr::MODULUS)?;
```

## Solution 
First, import the `Field` trait as we need field operation function.
```
use ark_ff::Field;
```

Next, load secret. This time we loaded the data as MNT6BigFr because we need to negate the value for negative scalar multiplication.
```
let mut secret_hack_temp: MNT6BigFr = from_file("./leaked_secret.bin");
```

Negate the loaded secret and convert into MNT4BigFr.
```
let secret_hack: MNT4BigFr =
        MNT4BigFr::from_bigint(secret_hack_temp.neg_in_place().into_bigint()).unwrap();
```

FYI, negating a value from field is subtraction from modulus. [ref](https://github.com/arkworks-rs/algebra/blob/master/ff/src/fields/models/fp/montgomery_backend.rs#L134)

```
    fn neg_in_place(a: &mut Fp<MontBackend<Self, N>, N>) {
        if !a.is_zero() {
            let mut tmp: BigInt<N> = Self::MODULUS;
            tmp.sub_with_borrow(&a.0);
            a.0 = tmp;
        }
    }
```

Now generate `nullified_hack` using the `secret_hack` with same parameter (Poseidon)
```
let nullifier_hack =
        <LeafH as CRHScheme>::evaluate(&leaf_crh_params, vec![secret_hack]).unwrap();
```

### Fixing the Circuit
By checking the sign of y value on the circuit, the double spending issue can be resolved. Following code checks whether the sign bit is set or not and make a constraint.
```
        use ark_ff::BigInteger;
        let a = Boolean::new_witness(cs.clone(), || Ok(false))?;
        let b = Boolean::new_witness(cs.clone(), || {
            Ok(pk.y.value().unwrap().into_bigint().to_bits_le()[0])
        })?;
        a.enforce_equal(&b)?;
```