BigInt: Missing Bit Length Check

BigInt: Missing Bit Length Check

Identified By: Andrew He and Veridise Team independently

The BigMod circuit, used for the modulo operation on big integers, was missing a bit length check on the output remainder. This constraint needs to be added to prevent an attacker from using an unexpectedly large remainder value. This can break a protocol in various ways, depending on how they use this circuit.

Background

The BigInt circuits are used to perform arithmetic on integers larger than the SNARK scalar field order. BigMod is the circuit responsible for performing the modulo operation on these large integers. BigMod takes inputs a and b, and outputs the quotient and remainder of a % b. The circuit uses a helper function, long_division, to calculate the quotient and remainder. However, functions can’t add constraints, so the BigMod circuit must add constraints to ensure that the quotient and remainder are correct.

Additionally, the BigInt circuits store big integers in two formats: proper representation and signed overflow representation. Proper representation does not allow for integers to be negative whereas the signed overflow representation does. Due to the representation style, the negative signed overflow numbers may have more bits than the proper representation style.

The Vulnerability

Two important constraints are ensuring that both the quotient and the remainder are the proper number of bits. There was a bit length check on the quotient, however there was no check for the remainder:

 // From circom-ecdsa/circuits/bigint.circom before the fix
 
 // Long division helper function. Outputs the quotient and remainder
 var longdiv[2][100] = long_div(n, k, k, a, b);
 for (var i = 0; i < k; i++) {
     div[i] <-- longdiv[0][i]; // Quotient
     mod[i] <-- longdiv[1][i]; // Remainder
 }
 div[k] <-- longdiv[0][k];
 
 // Range check for the quotient
 component range_checks[k + 1];
 for (var i = 0; i <= k; i++) {
     range_checks[i] = Num2Bits(n);
     range_checks[i].in <== div[i];
 }

Without a bit length constraint on the remainder, the output of this circuit was not guaranteed to be in proper representation. Only the quotient, div[], was constrained to n bits per register in the array. The remainder array, mod[], was not constrained to n bits. Therefore any consumers of this circuit are not guaranteed to have the remainder be accurate and as expected.

The Fix

In order to ensure that the remainder doesn’t contain too many bits and proceed to cause unexpected behavior from there, a bit length constraint must be added. The circuit was changed to incorporate this fix:

 // From circom-ecdsa/circuits/bigint.circom after the fix
 
 var longdiv[2][100] = long_div(n, k, k, a, b);
 for (var i = 0; i < k; i++) {
     div[i] <-- longdiv[0][i];
     mod[i] <-- longdiv[1][i];
 }
 div[k] <-- longdiv[0][k];
 
 component div_range_checks[k + 1];
 for (var i = 0; i <= k; i++) {
     div_range_checks[i] = Num2Bits(n);
     div_range_checks[i].in <== div[i];
 }
 
 // The new bit length check on the remainder
 component mod_range_checks[k];
 for (var i = 0; i < k; i++) {
     mod_range_checks[i] = Num2Bits(n);
     mod_range_checks[i].in <== mod[i];
 }