Description

The universal batch verifier chip's compute_pi_pairs function is used to calculate a sum $S=s_0+{\sum }_{j=1}^L{P}_j\cdot s_j$ using the following code, where ss corresponds to $[s_0,\dots ,s_L]$ and inputs to $[P_1,\dots ,P_L]$. The elliptic curve points $s_0,\dots ,s_L$ are part of the verification key for a Groth16 circuit, and the scalars $P_1,\dots ,P_L$ are the public inputs.

let rhs = ec_chip.variable_base_msm::<G1Affine>(
    builder,
    &ss[1..], // We skip the first element
    inputs,
    F::NUM_BITS as usize,
);
let pi_term = ec_chip.sum::<G1Affine>(
    builder.main(0),
    once(rhs).chain(once(ss[0].clone())),
);

If all components of $[P_1,\dots ,P_L]$ are zero, then ec_chip.variable_base_msm will return zero (i.e., the point at infinity), represented by $(0,0)$. There are also other linear combinations of $s_1,\dots ,s_L$ that are zero, though this is unlikely to happen by accident for legitimate verification keys. If $s_1,\dots ,s_L$ were random points, then finding nonzero scalars that make the linear combination zero means solving a discrete log relation problem for the elliptic curve, which is assumed to be infeasible. Note that if it were feasible to find a nontrivial linear relation between the $s_1,\dots ,s_L$, then this would amount to malleability of Groth16 proofs with respect to the public inputs. Thus, the case to consider here is the one where all scalars are zero.

Whenever the linear combination rhs is zero, the first summand in the call to ec_chip.sum will be $(0,0)$. However, sum does not support this as a representation of the point at infinity, so the result pi_term will not be ss[0] as it should. For more details, see Finding ref↗.

Similarly, proving will fail should rhs and ss[0] be additive inverses of each other (equivalently, if the correct result for pi_term would be zero). This is again unlikely to happen by accident for legitimate verification keys. For more details, see Finding ref↗.

Impact

Attempting to prove verification of a batch of Groth16 proofs using the universal batch verifier chip will fail if one of the proofs in the batch has all public inputs being zero. Proof generation will also fail in some other cases that are unlikely to occur for legitimate verification keys but can be caused by specifically choosing the verification key. The concern in this latter case is not completeness but soundness, and relevant impacts are discussed in Finding ref↗.

Recommendations

We recommend to change the above snippet of code to one that correctly computes the sum $S=s_0+{\sum }_{j=1}^L{P}_j\cdot s_j$ in all cases in which $P_j$ are points on the curve. This could be done by using variable_base_msm for the entire sum, by replacing ss[1..] in the call by ss and inputs by the concatenation of F::one() with inputs.

Remediation

This issue has been acknowledged by Nebra, and a fix was implemented in commit e19c58f8↗.