Description

This finding concerns the method evaluate_non_native_field_multiplication of the class UltraCircuitBuilder_. We refer to section ref↗ for background on how this function is intended to work.

The issue is that calculations done by evaluate_non_native_field_multiplication can overflow modulo the native circuit prime modulus $r$. (Note that the function uses an array also called r for the remainder; to distinguish the remainder from the prime, we will only refer to the limbs of the remainder r[0], r[1], r[2], and r[3] but never use r for the array itself.) The core computation of the function is summarized by the following snippet containing the out-of-circuit calculation of the witnesses, which are then constrained elsewhere in the function:

FF lo_0 = a[0] * b[0] - r[0] + (a[1] * b[0] + a[0] * b[1]) * LIMB_SHIFT;
FF lo_1 = (lo_0 + q[0] * input.neg_modulus[0] +
           (q[1] * input.neg_modulus[0] + q[0] * input.neg_modulus[1] - r[1]) * LIMB_SHIFT) *
          LIMB_RSHIFT_2;

FF hi_0 = a[2] * b[0] + a[0] * b[2] + (a[0] * b[3] + a[3] * b[0] - r[3]) * LIMB_SHIFT;
FF hi_1 = hi_0 + a[1] * b[1] - r[2] + (a[1] * b[2] + a[2] * b[1]) * LIMB_SHIFT;
FF hi_2 = (hi_1 + lo_1 + q[2] * input.neg_modulus[0] +
           (q[3] * input.neg_modulus[0] + q[2] * input.neg_modulus[1]) * LIMB_SHIFT);
FF hi_3 = (hi_2 + (q[0] * input.neg_modulus[3] + q[1] * input.neg_modulus[2]) * LIMB_SHIFT +
           (q[0] * input.neg_modulus[2] + q[1] * input.neg_modulus[1])) *
          LIMB_RSHIFT_2;

These calculations can overflow modulo $r$. If an overflow happens, evaluate_non_native_field_multiplication can be used to prove incorrect multiplications, so it is crucial that callers ensure that all limbs of the arguments are sufficiently constrained to ensure no overflow can happen.

The method evaluate_non_native_field_multiplication under discussion is in particular called by bigfield::unsafe_evaluate_multiple_multiply_add, which is in turn used by bigfield::operator*. We will now describe how a call to bigfield::operator* can ultimately result in an overflow in evaluate_non_native_field_multiplication in such a way that an incorrect product can be proven. There are likely also other paths to use this bug; this is just one concrete example.

Let a, b, and c be such that (a<<68) * b = r + c, with c<r and a,b < 2^117. This is possible because 2 * 117 + 68 = 302 is significantly bigger than the bit width of $r$, which is 254. Now suppose we instantiate two bigfield elements A and B with binary limbs (in little endian) (0, a, 0, 0) and (b, 0, 0, 0). Applying operator* to calculate A*B, no reductions would be needed as the limbs of both elements are less than 117 bits and the unsigned integer represented is also small enough, since we are only using the two least significant limbs. The two elements would thus be passed to unsafe_evaluate_multiple_multiply_add unchanged.

In the HasPlookup<Builder> case, we would ultimately end up in evaluate_non_native_field_multiplication, with factors still unchanged A and B. The calculation of lo_0 would then overflow:

FF lo_0 = a[0] * b[0] - r[0] + (a[1] * b[0] + a[0] * b[1]) * LIMB_SHIFT;

This expression calculating lo_0 simplifies to a*b*(1<<68) - r[0], which is by our assumption equal to r+c - r[0]. As the calculation is done modulo $r$, we obtain an overflow and will have lo_0=c - r[0]. We will then have that all further computations, ending up with lo_1 and hi_3, will be zero, if we set the remainder to be proven to (c, 0, 0, 0) and the quotient to (0, 0, 0, 0).

Thus, the checks in evaluate_non_native_field_multiplication and bigfield::unsafe_evaluate_multiple_multiply_add will amount to the incorrect acceptance of (a<<68) * b to be equal to c modulo 2^t, which is, however, false. The check of the identity for the prime limbs will also pass, as (a<<68) * b actually is equal to c modulo $r$.

Thus, a malicious prover can ultimately prove that $(a<<68)\cdot b=c$ modulo the emulated prime modulus $p$, even though this is wrong.

Impact

It is possible to prove incorrect product identities modulo $2^t$, which can be leveraged from the bigfield component in order to (in particular) prove incorrect products of bigfield elements.

Recommendations

Ensure that no overflows modulo $r$ can happen in evaluate_non_native_field_multiplication. As this function is not passed maximums for its arguments, this likely needs to be done in two steps.

First, document bounds for the arguments to evaluate_non_native_field_multiplication that callers must enforce, and ensure that those bounds are strict enough that no overflows modulo $r$ can happen.

Second, make sure callers such as unsafe_evaluate_multiply_add (perhaps by documenting requirements for its callers) actually enforce those bounds. How to do that might depend from case to case. Carrying out a reduction check is not enough, as the example above demonstrates (operator* does have a reduction check, but as the limbs are all small enough, the elements pass it without reduction). So it might be necessary to check whether the maximums satisfy the bounds, and if not, then reduce both elements and check again.

The situation is complicated by the fact that unsafe_evaluate_multiply_add (which calls evaluate_non_native_field_multiplication) is used by self_reduce, and for that usage, unsafe_evaluate_multiply_add must be able to deal with values for input_left that have limbs that are even bigger than 117 bits wide. Reducing to deal with this is not an option, as this is exactly the call intended to perform the reduction. While input_left might have very large limbs on calls by self_reduce, the second factor input_to_mul will just be one, however. So, it may be feasible to make two sets of assumptions for arguments to unsafe_evaluate_multiply_add, and satisfying either of those two sets of assumptions will ensure the conditions necessary for evaluate_non_native_field_multiplication.

Remediation