ZKHack IV Puzzle F1: Gamma Ray

ZKHackIVPuzzle1.md

The Scenario

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 MNT6-753 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...

Puzzle Definition

Bob was exploited by Alice when he attempted to compose a frankenstein protocol. Let's review his protocol and understand what went wrong.

The Building Blocks

Elliptic Curves

Elliptic Curves are a valuable building block in cryptography. When cast over a finite field useful primitives appear. A set of points that live on the curve form a group $\mathbb{G}$. The points are represented by elements in $\mathbb{F}_q$ the base field, but there exists another finite field associated with the curve called the scalar field $\mathbb{F}_r$ which can be used to for group arithmetic. An operation between an element in $\mathbb{F}_r$ (represented as $a$) and and element in $\mathbb{G}$ (represented as $g$) can be thought of as $g^a$. In some groups, given $g$, it is cryptographically hard to extract $a$.

Bob's protocol uses this property in his protocol. A secret key in his protocol is $a \in \mathbb{F}_r$ and its public key is $\prod g^{a_i}$ where $g$ is a publically known generator point and $a_1..a_i$ are the little endian bytes of the secret key. In the circuit, one proves that they know of a secret key by producing the public key in zero-knowledge (code).

let base = G1Var::new_constant(ark_relations::ns!(cs, "base"), G1Affine::generator())?;
let pk = base.scalar_mul_le(secret_bits.iter())?.to_affine()?;

Short Weierstrass Form

Short Weierstrass form is a way to represent elliptic curves. Here is an example of Weierstrass curve represented in 2 dimensions over all real numbers:

In affine coordinates $(x,y)$, the lines approach a single point of infinity at both ends.

The curves that Bob is using are represented in this form.

Twisted Edwards Form

Twisted Edwards form is a different way of representing elliptic curves that can lead to more efficient arithmetic. The point of infinity is usually represented by $(0,1)$. This comes with entirely different formulas for arithmetic and point representation than Weierstrass form.

Snarks

Snarks are a way to prove the correctness of a computation while optionally allowing the inputs to the computation to be hidden. The proof can be significantly smaller than the size of the inputs to the computation.

Snarks are made up of a polynomial IOP which translates a program into a polynomial representation of random values, and a polynomial commitment, which allows a protocol to evaluate a committed polynomials at those random values. Many polynomial commitements use elliptic curve cryptography.

In Bob's protocol, he proves a correct computation on a secret key without revealing that secret key. A proof is output and can be verified by an honest party (like a blockchain).

Snark Recursion

Recursion of snarks is where we take a proof ($\pi_1$) and implement the verification procedure inside of a circuit, then prove that we were able to successfully verify $\pi_1$ and produce a proof of verification $\pi_2$. This can be used to decrease the size of the proof and the verification time in exchange for extra proving work.

Cycles of Curves

Elliptic curve cycles are defined as curves in which the scalar field ($\mathbb{F}_r$) of curve $E_1$ is equal to the base field ($\mathbb{F}_q$) of curve $E_2$, and the scalar field ($\mathbb{F}_r$) of curve $E_2$ is equal to the base field ($\mathbb{F}_q$) of curve $E_1$.

This is applicable to snark recursion. Poplular polynomial commitment schemes such as Groth16, KZG, and Bulletproofs, require the commitment to group elements. This means that the polynomial IOP has to be done in $\mathbb{F}_r$ of the curve used to compute the commitments. The proof ($\pi_1$) is then distilled into a set of group elements that are defined by their coordinates in $F_q$.

When recursing snarks, the verifier of $\pi_1$ must be implemented in a circuit and committed to in a another proof ($\pi_2$) that certifies that $\pi_1$ was correctly verified. Since we have to commit to the verification process, we have to do it in a scalar field ($\mathbb{F}_r$), but the commitments we received are group elements with coordinates in $\mathbb{F}_q$. Luckily, we have the curve $E_2$, where $E_2\mathbb{F}_r = E_1\mathbb{F}_q$.

Bob's protocol attempts to use a cycle of curves called MNT4-753 and MNT6-753.

The Vulnerability

Bob's circuit forces one to prove knowledge of a secret key which corresponds to a public key. There is a database of public keys and the circuit makes sure that the public key corresponding the the secret key is in that database.

There is an issue though. Alice was seemingly able to prove membership of a single public key using 2 different private keys.

Based on clue #1, Bob's representation of the public key element was inspired by a passage in the Zcash protocol specification.

See lemma 5.4.7 in the Zcash spec for Bob's reasoning on why to only use the x coordinate when storing the public keys.

This is reflected in his circuit's code.

let leaf_g: Vec<_> = vec![pk.x];

The leema from the Zcash spec that he is referring to is as follows:

Let 𝑃 = (𝑢,v) $\in$ $J$($𝑟$). Then (𝑢,−v) $\not\in$ $J$($𝑟$).

$J$ is for JubJub, a twisted edwards curve built on top of the scalar field of BLS12-381.

Bob does not realize that JubJub uses a different form than MNT6-753 and therefore lemma 5.4.7 is not applicable to his application. Let's explore JubJub by negating a point:

use ark_ed_on_bls12_381::{Fr as JubJubFr, EdwardsAffine};

let scalar = JubJubFr::from(1_u64);
let negated_scalar = scalar.neg();
let g = EdwardsAffine::generator();

println!("{}", g * scalar);
println!("{}", g * negated_scalar);

(8076246640662884909881801758704306714034609987455869804520522091855516602923, 13262374693698910701929044844600465831413122818447359594527400194675274060458)

(44359628534463305569565938749481659123655942513071768018083136608083064581590, 13262374693698910701929044844600465831413122818447359594527400194675274060458)

In both points, $y$ is the same, but $x$ is different.

This is different than the result we would get from negating the point in Weierstrass form.

use ark_mnt6_753::{Fr as MNT6BigFr, G1Affine};


let scalar = MNT6BigFr::from(1_u64);
let negated_scalar = scalar.neg();
    
let g = G1Affine::generator();
    
println!("{}", g * scalar);
println!("{}", g * negated_scalar);

(3458420969484235708806261200128850544017070333833944116801482064540723268149235477762870414664917360605949659630933184751526227993647030875167687492714052872195770088225183259051403087906158701786758441889742618916006546636728, 27460508402331965149626600224382137254502975979168371111640924721589127725376473514838234361114855175488242007431439074223827742813911899817930728112297763448010814764117701403540298764970469500339646563344680868495474127850569)

(3458420969484235708806261200128850544017070333833944116801482064540723268149235477762870414664917360605949659630933184751526227993647030875167687492714052872195770088225183259051403087906158701786758441889742618916006546636728, 14437982565586988252717614566858499873667733940785577960142578199436225087194633258220659402675483745929828964457019403099345314677681955251765513742498632717710601561232363037930119372875928969272289155715227295725310348309432)

In both points, $x$ is the same, but $y$ is different.

$- (x, y) = (x, -y)$

This means that Bob's technique of only checking the $x$ coordinate of the public key did not ensure that a single secret key generated it. Even worse, there is a simple equation to find the other secret key that generates the $x$ coordinate.

The Exploit

In the codebase, the leaked secret key is represented as a scalar element in MNT4-753. When it is passed into the circuit, it is passed in as bytes in little endian encoding.

When we look in the circuit, Bob decode's those bytes into an element in the scalar field of MNT6-753. That scalar is then used to generate the public key in the circuit. This means that exploiting the protocol will not be as easy as negating the secret key.

Alice still found a way though:

let secret_hack = MNT4BigFr::from_le_bytes_mod_order(
    &MNT6BigFr::from_le_bytes_mod_order(
        &leaked_secret.into_bigint().to_bytes_le()
    )
    .neg()
    .into_bigint()
    .to_bytes_le()
);
let nullifier_hack = <LeafH as CRHScheme>::evaluate(
    &leaf_crh_params, vec![secret_hack]
).unwrap();
   

She first encoded the secret key as bytes and create an element in the scalar field of MNT6-753, exactly like the circuit does. She then negated that element and transformed it back into a scalar in MNT4-753. She used that to create a nullifier that did not resemble her original one and exploited the protocol.