privacy-scaling-explorations / halo2wrong

Apache License 2.0
116 stars 87 forks source link

Aux point used for incomplete EC formulas #53

Open davidnevadoc opened 1 year ago

davidnevadoc commented 1 year ago

Some EC operations such as multiplication and batch multiplication make use an extra aux point in order to utilize incomplete (and more convenient) addition and doubling formulas. This approach is detailed here.

At the moment this aux point is generated at random and passed to the circuit. The purpose of this issue is to discuss whether this point could be fixed and hardcoded into the circuit or not, and what are the security implications and requirements regarding the choice of this point.

han0110 commented 1 year ago

After confirmed with @kilic, we should be able to bake a constant into aux, we only need to make sure [aux, 2*aux, 4*aux, 8*aux, ...] are all different for multiexp algorithm (so perhaps choose a random point that's not identity).

CPerezz commented 1 year ago

@davidnevadoc will elaborate on that and come up with a HackMD writeup to start the discussion over this.

CPerezz commented 1 year ago

This approach was taken from Aztec so we could contribute back with our solution.

davidnevadoc commented 1 year ago

I wrote a small note about this topic, see note. The summary is that the aux point cannot be fixed or, more generally, known by the prover before the witness generation, otherwise he can break soundness.

CPerezz commented 1 year ago

Las item to be able to close this would be to export an alias for a Fixed Random Point.

swasilyev commented 1 year ago

There's an observation by @burdges or @AlistairStewart that if the curve is not prime order (has a cofactor), you can start summation from an element from outside the subgroup. Then you will never meet an exceptional case when adding elements from the group.

burdges commented 1 year ago

It depends what constraints you've placed upon the inputs of course. You should avoid adversaries cancelling out your deformation, whether doing an independent point in the subgroup or using a point outside the subgroup. It'll always work if you produce an independent point by fiat-shamir but this maybe overkill for your setting. If adversarial supplied points all land inside the subgroup anyways then a point outside maybe simplest, but adversarial points being inside the subgroup incurs costs.

davidnevadoc commented 1 year ago

In short, everything seems to be properly constrained. By using incomplete formulas we need to make sure that, when adding 2 point P, Q, we disallow the following cases:

  1. P != Q
  2. P != - Q
  3. P != identity and Q != identity

In the context of the scalar multiplication algorithm, cases 1 and 2 are covered by checking P.x != Q.x for every addition, and case 3 is covered by not allowing the identity to pass the assert_is_on_curve() check, and consequently assuming no AssignedPoint is the identity.

However, AssignedPoints that are created directly with new instead of assign_point do not undergo this check. I have found no errors in the current code but I think this could be a source of bugs at some point in the future.

kitounliu commented 1 year ago

The current implementation does not appear to be secure, as there is no guarantee that the prover will choose aux_generator randomly or in any other appropriate way. Therefore, two assertions are required in ladder(..): x2 != x1 && x3 != x1, regardless of whether aux_generator is kept private, public, or constant. If aux_generator is kept private, then the computation for AuxFin in make_mul_aux(..) needs to be included within the circuits to show AuxFin is computed correctly. Alternatively, aux_generator and AuxFin can be made constant.

kitounliu commented 1 year ago

To fix the above issue with auxiliary generator, I implemented a windowed scalar mul where the auxiliary generator is only used in the last two steps. The algorithm description is here: https://github.com/kitounliu/halo2wrong/blob/windowed/ecc/README.md I also created a pull request: https://github.com/privacy-scaling-explorations/halo2wrong/pull/81

kilic commented 1 year ago

@kitounliu Thanks for the correction

to show AuxFin is computed correctly.

Yes it is basically a soundness error. We definitely need to prove that correction point is derived from the starting point.

Alternatively, aux_generator and AuxFin can be made constant.

This would introduce some dos issues if we don't want to handle infinity points and use incomplete formulas. There are some applications where points are derived from public inputs for example public keys in ecdsa