🔢BigInt: Missing Bit Length Check

Book an audit with Zokyo

Summary

Related Vulnerabilities: 1. Under-constrained Circuits, 2. Nondeterministic Circuits, 3. Arithmetic Over/Under Flows, 4. Mismatching Bit Lengths

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];
}

Conculsion

1. BigInt Circuits: These are specialized circuits that handle arithmetic operations on very large integers. This is crucial in cryptography where large numbers are common.

2. BigMod Circuit: It's a sub-component of the BigInt circuits and is responsible for the modulo operation on large integers (i.e., finding the remainder when one number is divided by another). In this case, the circuit is taking two inputs 'a' and 'b', and computing the result of 'a % b' which yields a quotient and a remainder.

3. Proper Representation vs. Signed Overflow Representation:

   • Proper Representation: Positive integers only.

   • Signed Overflow Representation: Allows for both positive and negative integers. And notably, these negative numbers might take up more bits than the positive ones.

The Vulnerability:

1. The crux of the vulnerability is that while there are constraints ensuring that the quotient has a proper number of bits, there was no such constraint for the remainder. This means the remainder could have an unexpected number of bits.

2. In the provided code, there's a bit-length check on the quotient (div[]), but not on the remainder (mod[]). Without this constraint on the remainder, the output of the modulo operation might not be in the expected format or size.

3. Because of the missing constraint, the remainder could have been in the "signed overflow representation" when it should have been in the "proper representation." In practice, if other parts of the system expected the remainder to always be in proper representation, this could lead to a variety of issues, including incorrect calculations or other vulnerabilities.

Why is this a big deal?

If any consumers or other circuits use this BigMod circuit and expect the remainder to be in a specific format (e.g., proper representation) but it's not, then those circuits might malfunction or even introduce other security vulnerabilities. For cryptographic systems, even a tiny inaccuracy or unexpected behavior can cascade into big security flaws.

The Fix:

The solution is straightforward: apply the same bit-length constraint on the remainder (mod[]) as was applied to the quotient (div[]). The updated code reflects this, ensuring that both the quotient and remainder are of the expected length and representation.

In essence, ensuring the correct bit-length and representation is fundamental in cryptography. Not doing so can make the system unpredictable, which is a cardinal sin in security-sensitive applications.

"But I thought remainders are small so how can they ever be out of range?"

The concept of a "remainder" in arithmetic that we learned in school might seem like it's always small, especially when we think about numbers in base 10. For instance, when you divide by 10, the remainder can only be between 0 and 9. However, in the context of cryptographic operations and, more broadly, computer science, "remainder" can take on a different scale.

To understand why a remainder can be large or "overflow", consider these points:

1. Large Divisors: In computer arithmetic, especially in cryptographic contexts, the divisor can be a very large number. The remainder, by definition, is a number between 0 and (divisor-1). So, if your divisor is a number with hundreds of bits, the remainder can also be a number up to that many bits minus one.

2. Binary Representation: Computers work in binary. So, when we talk about overflows and bit lengths, we are thinking in terms of binary representation. A number that might seem small in decimal can have a long representation in binary.

3. BigInt Context: The passage you provided talks about BigInt circuits, which handle "big integers" – numbers that can have hundreds or even thousands of bits. When such big numbers are divided, the remainder, although it's smaller than the divisor, can still be a big number.

4. Consistency in Representations: The circuits you're dealing with use specific representations for numbers. If a number, even a remainder, doesn't fit within the expected bit length, it might get represented incorrectly or might cause unexpected behaviors in subsequent operations.

In the vulnerability you shared, the issue wasn't just that the remainder could be large. The primary concern was that there was no constraint to ensure the remainder fit within the expected bit length. In cryptographic circuits, every bit matters, and an unexpected bit can introduce vulnerabilities or make the circuit behave unpredictably.

References

1. Commit of the Fix
2. More info on bigint representation