Skip to content

Instantly share code, notes, and snippets.

@niooss-ledger

niooss-ledger/zkhack2021_puzzle6_writeup.md

Created December 1, 2021 10:33
Show Gist options
  • Save niooss-ledger/1e63fe7a4c70e31398a33bacccc7f69e to your computer and use it in GitHub Desktop.
Save niooss-ledger/1e63fe7a4c70e31398a33bacccc7f69e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
zkhack2021_puzzle6_writeup.md

Write-up for zkHack puzzle #6: Soundness of Music

Subject

It is a well-known fact that 1+1=2. Recent work by Alice von Trapp (et al) suggests that under special conditions in the Swiss Alps, 1+1+1+1=1. Alice has been unable to prove this statement over the BLS12-381 scalar field. The primary difficulty appears to be the fact that 1 is not equal to 4. Alice's proving system can write a proof for every statement (x,y) where x and y are BLS12-381 scalars, and x+x+x+x=y. The proving system easily outputs a proof for the statement (1,4) showing 1+1+1+1=4, but seems unable to produce a proof for the statement (1,1) showing 1+1+1+1=1.

A proof for the statement (1,1) is badly needed for the elliptic curve finale song to be added to Appendix A. Can you save the show and output a proof where verify(&[Fr::one(), Fr::one()], &setup, &proof) = true?

The proof system

The project https://github.com/kobigurk/zkhack-soundness-of-music implements a proof system which uses polynomial commitments, like some previous puzzles. This system relies on four components:

The project also provides some code which show how to use the functions to compute a proof in src/lib.rs:

// Successfully prove that 1+1+1+1=4
let two = Fr::one() + Fr::one();
let four = two + two;
let public_inputs = [Fr::one(), four];
let private_inputs = [two];
let proof = prover::prove(&public_inputs, &private_inputs, &circuit, &setup);
assert!(verifier::verify(&public_inputs, &setup, &proof));

How does this proof work? This example uses a public input with two items [1, 4], and a private input with a single item [2]. To craft a proof that 1+1+1+1 = 4, the system splits this equation in two: 1+1 = 2 and 2+2 = 4.

In practice, the circuit works on three inputs [x, y, z]: x and y are public while z is a private input (meaning: the verifier can ignore its value while verifying the proof). How is it possible to craft a circuit which ensures that x+x = z and z+z = y? By rewriting these equations as:

2*(1*x + 0*y + 0*z) = 0*x + 0*y + 1*z
2*(0*x + 0*y + 1*z) = 0*x + 1*y + 0*z

In the world of zk-SNARKs, it is common to merge such equations using polynomials which take specific values when being evaluated on roots of the unity. Here the system introduces polynomials input_i[X] and output_i[X] such that:

2*(input_0[X]*x + input_1[X]*y + input_2[X]*z) = output_0[X]*x + output_1[X]*y + output_2[X]*z
ω is a square root of unity of order 2
input_0(ω^0) = 1 and input_0(ω^1) = 0
input_1(ω^0) = 0 and input_1(ω^1) = 0
input_2(ω^0) = 0 and input_2(ω^1) = 1
output_0(ω^0) = 0 and output_0(ω^1) = 0
output_1(ω^0) = 0 and output_1(ω^1) = 1
output_2(ω^0) = 1 and output_2(ω^1) = 0

The structure Circuit contains these polynomials, as well as the polynomial Z[X] = X^2 - 1. This polynomial is named the vanishing polynomial of the domain [ω^0, ω^1] because its value is zero on the chosen roots of the unity.

The system then uses a Setup structure which contains pre-computed points on the BLS12-381 curves. It was generated from the Circuit polynomials, the generators g1 and g2 of BLS12-381 curves, and six random number (τ, ρ, α_in, α_out, β, γ):

setup.tau = [g1, τ.g1, (τ^2).g1]
setup.inputs = [(ρ*input_0(τ)).g1, (ρ*input_1(τ)).g1, (ρ*input_2(τ)).g1]
setup.inputs_prime = [(α_in*ρ*input_0(τ)).g1, (α_in*ρ*input_1(τ)).g1, (α_in*ρ*input_2(τ)).g1]
setup.outputs = [(ρ*output_0(τ)).g1, (ρ*output_1(τ)).g1, (ρ*output_2(τ)).g1]
setup.outputs_prime = [(α_out*ρ*output_0(τ)).g1, (α_out*ρ*output_1(τ)).g1, (α_out*ρ*output_2(τ)).g1]
setup.K = [(β*ρ*(input_0(τ) + output_0(τ))).g1, (β*ρ*(input_1(τ) + output_1(τ))).g1, (β*ρ*(input_2(τ) + output_2(τ))).g1]
setup.alpha_inputs = α_in.g2
setup.alpha_outputs = α_out.g2
setup.gamma = γ.g2
setup.beta_gamma = (β*γ).g2
setup.rho_Z = (ρ*Z(τ)).g2

To create a Proof object from public inputs [x, y] and a private input [z], the prover computes:

  • P[X] = 2*(input_0[X]*x + input_1[X]*y + input_2[X]*z) - (output_0[X]*x + output_1[X]*y + output_2[X]*z). This is a polynomial which evaluates to zero on the roots of unity ω^i. This property makes P[X] a multiple of the vanishing polynomial Z[X].
  • H[X] = P[X] / Z[X]. This is the polynomial such that P[X] = H[X] * Z[X].
  • π_H = H(τ).g1. This point can be computed without knowing τ thanks to the precomputation in setup.tau.
  • π_input = z . setup.inputs[2]
  • π'_input = z . setup.inputs_prime[2]
  • π_output = x . setup.outputs[0] + y . setup.outputs[1] + z . setup.outputs[2]
  • π'_output = z . setup.outputs_prime[0] + y . setup.outputs_prime[1] + z . setup.outputs_prime[2]
  • π_K = x * setup.K[0] + y * setup.K[1] + z * setup.K[2]

The proof then consists in (π_input, π'_input, π_output, π'_output, π_K, π_H).

To verify such a proof, the verifier computes a point pk = x . setup.inputs[0] + y . setup.inputs[1] (in the literature this is often called PI, as this point maps the public input associated with the proof) and uses the BLS12-381 pairing function e to check the following equations:

e(π'_input, g2) = e(π_input, setup.alpha_inputs)
e(π'_output, g2) = e(π_output, setup.alpha_outputs)
e(π_K, setup.gamma) = e(pk + π_input + π_output, setup.beta_gamma)
e(2.(pk + π_input) - π_output, g2) = e(π_H, setup.rho_Z)

Now that the system is fully described, how can be craft a proof for 1+1+1+1=1?

Proving that 4 = 1

The proof system has a vulnerability: π'_input is not used in the last equation and it is possible to modify π'_input and π_input to craft a valid proof for another public input! This is the same vulnerability as the one which was described in https://eprint.iacr.org/2019/119 for another zk-SNARK system.

More precisely, let's consider an attacker who wants to build a new proof for the input [x', y']. This attacker first computes the new pk:

pk' = x' . setup.inputs[0] + y' . setup.inputs[1]

Then, to verify the last equation, the attack can craft a η_input point which updates π_input such that:

pk' + η_input = pk + π_input

By expanding the definitions of pk and pk', this leads to computing:

η_input = π_input + (x - x') . setup.inputs[0] + (y - y') . setup.inputs[1]

Then the first equation e(π'_input, g2) = e(π_input, setup.alpha_inputs) becomes incorrect when π_input is replaced with η_input. Nevertheless by computing η'_input from setup.inputs_prime the attacker is able to craft a valid proof:

η'_input = π'_input + (x - x') . setup.inputs_prime[0] + (y - y') . setup.input_primes[1]

After these computations, (η_input, η'_input, π_output, π'_output, π_K, π_H) is a valid proof for [x', y'].

In the puzzle, we already have a legitimate proof for 1+1+1+1=4 which uses x = 1 and y = 4. To prove that 1+1+1+1=1, all we need to do is to compute a rogue proof with x' = 1 and y' = 1. In Rust, the following code computes this proof (using the previous proof object):

let my_proof = prover::Proof {
    pi_input: proof.pi_input + setup.inputs[1].mul(Fr::from(4 - 1)).into_affine(),
    pi_input_prime: proof.pi_input_prime + setup.inputs_prime[1].mul(Fr::from(4 - 1)).into_affine(),
    pi_output: proof.pi_output,
    pi_output_prime: proof.pi_output_prime,
    pi_K: proof.pi_K,
    pi_H: proof.pi_H,
};
let public_inputs = [Fr::one(), Fr::one()];
assert!(verifier::verify(&public_inputs, &setup, &my_proof));

This attack is mainly possible because setup.inputs_prime[0] and setup.inputs_prime[1] are known (so the attacker is able to compute η'_input), even though these points are never used. Removing them would make this proof system more secure... wouldn't it? In fact, the system is much more broken and here removing these points from the setup data would not be enough.

Implementation bug 1: the domain is too small and input_1[X] = 0

This puzzle seems to be a straightforward illustration of the vulnerability from https://eprint.iacr.org/2019/119. Nevertheless an implementation issue makes the puzzle much easier: the domain used by the circuit is too small.

Indeed, when defining the circuit, one of the polynomials was defined as:

input_1(ω^0) = 0 and input_1(ω^1) = 0

In Rust, this polynomial is computed in function make_circuit:

pub fn make_circuit<E: PairingEngine>() -> Circuit<E> {
    let domain = GeneralEvaluationDomain::<E::Fr>::new(2).unwrap();
    /* ... */
    let input_polynomial =
        Evaluations::<E::Fr>::from_vec_and_domain(vec![E::Fr::zero(), E::Fr::zero()], domain)
            .interpolate();

Among polynomials of degree at most 1, the only one which evaluates to zero in 2 distincts point is 0. Therefore input_1[X] = 0, input_1(τ) = 0, setup.inputs[1] = O and setup.inputs_prime[1] = O (O being here the point at infinity on an elliptic curve). In Rust this can be verified:

assert_eq!(setup.inputs[1], G1Affine::zero());
assert_eq!(setup.inputs_prime[1], G1Affine::zero());

This also means that when verifying a proof, pk = x . setup.inputs[0] + y . O = x . setup.inputs[0]. So the public input y is ignored!!! This makes the attack much simpler, as this means that a valid proof for [x, y] is automatically valid for any other y.

How can this be fixed? A first idea would be to increase the size of the domain, for example by using 4th-roots of the unity. However doing so does not help much, as the circuit polynomials has to still evaluate to zero in the new roots, for P[X] to be a multiple of the vanishing polynomial Z[X].

Taking a step back, the main reason why input_1[X] = 0 is because the second public input y is never used as input in the circuit equations. And this is what happens when verifying the proof, as π_output contains a commitment for some value of y, which is not verified against the provided public input.

Therefore a stronger way to fix this issue consists in introducing 3 more equations in the circuit, which becomes:

2*(1*x + 0*y + 0*z) = 0*x + 0*y + 1*z
2*(0*x + 0*y + 1*z) = 0*x + 1*y + 0*z

2*(1*x + 0*y + 0*z) = 2*x + 0*y + 0*z
2*(0*x + 1*y + 0*z) = 0*x + 2*y + 0*z
2*(0*x + 0*y + 1*z) = 0*x + 0*y + 2*z

With ω' being a 5th root of the unity, this makes for example building a new input_1[X] such that input_1[ω'^0] = 0, input_1[ω'^1] = 0, input_1[ω'^2] = 0, input_1[ω'^3] = 1 and input_1[ω'^4] = 0. So input_1[X] is no longer zero.

Implementation bug 2: P[X] computation is wrong

The puzzle does not compute P[X] correctly. The code documents that P[X] = 2*(input_0[X]*x + input_1[X]*y + input_2[X]*z) - (output_0[X]*x + output_1[X]*y + output_2[X]*z) (in function prove) and this makes sense. But the implementation uses circuit.inputs instead of circuit.outputs on line 41:

P = &P + &P;
for (input, output_polynomial) in izip!(
    public_inputs.iter().chain(private_inputs.iter()),
    circuit.inputs.iter(),  // <= bug here: should be circuit.outputs.iter()
) {
    P = P + output_polynomial.mul(-*input);
}

So in fact the computed polynomial is:

P[X] = 2*(input_0[X]*x + input_1[X]*y + input_2[X]*z) - (input_0[X]*x + input_1[X]*y + input_2[X]*z)
     = input_0[X]*x + input_1[X]*y + input_2[X]*z

Therefore P(ω^0) = input_0(ω^0)*x + input_1(ω^0)*y + input_2(ω^0)*z = 1*x + 0*y + 0*z = x and P(ω^1) = z. As the input values are unlikely to be zero, this means that P[X] is not a multiple of Z[X].

However the proof system appears to be working well. How can this be?

In fact, as all input and output polynomials of the circuit are of degree at most 1, the degree of the computed P[X] is at most 1. With Z[X] = X^2 - 1, P[X] has a degree which is lower than Z[X]'s one, so P[X] / Z[X] = 0.

In the intended implementation, P[X] is a polynomial of degree at most 1 such that P(ω^0) = 0 and P(ω^1) = 0, so P[X] = 0 and H[X] = P[X] / Z[X] = 0. This is why the implementation works: H[X] is correct despite P[X] being incorrect. This happens because there is no hiding in this system. In other ones, H[X] could have been a non-zero polynomial which would hide the values of the private inputs.

To conclude, the verifier accepts the proof because π_H contains the right point: π_H = H(τ).g1 = 0.g1 = O.

Implementation bug 3: setup.rho_Z computation is wrong

The implementation of the setup contains comments which do not match the code. Indeed he documentation of struct Setup contains:

pub struct Setup<E: PairingEngine> {
// ...
    pub K: Vec<E::G1Affine>, // beta * (rho * input_polynomial_i(tau) + rho^2 * output_polynomial_i(tau))
// ...
    pub rho_Z: E::G2Affine,  // rho*Z(tau)
}

However setup.K is computed without squaring ρ and setup.rho_Z is computed with ρ^2 instead or ρ (on line 85).

rho_Z: fr_to_g2::<E>(rho * rho * circuit.Z.evaluate(&tau)),

The first contradiction is probably a misspelling in the comment, as using ρ^2 in setup.K would require other points to enable the verifier to verify the proof. Nevertheless this introduces an unexpected linear relationship between the values in setup.K:

setup.K[0] + setup.K[1] = setup.K[2]

This relationship was found by computing the circuit polynomials:

ω = -1  (this is the only square root of the unity of order 2)
circuit.inputs[0] = (X + 1) / 2  ; circuit.outputs[0] = 0
circuit.inputs[1] = 0            ; circuit.outputs[1] = (-X + 1) / 2
circuit.inputs[2] = (-X + 1) / 2 ; circuit.outputs[2] = (X + 1) / 2

setup.K[0] = (β*ρ*(input_0(τ) + output_0(τ))).g1 = (β*ρ*(τ + 1)/2).g1
setup.K[1] = (β*ρ*(input_1(τ) + output_1(τ))).g1 = (β*ρ*(-τ + 1)/2).g1
setup.K[2] = (β*ρ*(input_2(τ) + output_2(τ))).g1 = (β*ρ*(-τ + 1 + τ + 1)/2).g1 = (β*ρ).g1

setup.K[0] + setup.K[1] = (β*ρ).g1 = setup.K[2]

This linear relationship could be the source of more fragility in the proof system, but right now it is not the most important issue.

The second contradiction (of setup.rho_Z using ρ^2) is more problematic, as this breaks the proof verification, theoretically, as this can no longer hold:

e(2.(pk + π_input) - π_output, g2) = e(π_H, setup.rho_Z)

In practice, π_H = O (as there is no hiding in this proof system), so e(π_H, setup.rho_Z) is the point of infinity in the target group of the pairing, and the value of setup.rho_Z does not matter: the verifier in fact could check that 2.(pk + π_input) - π_output = O.

Conclusion

The system studied in this puzzle is very broken, as a proof for 1+1+1+1=4 can be directly used to prove that 1+1+1+1=y for any other y. The implementation also has several other bugs which can be easily fixed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment