🚓Circom-Pairing: Missing Output Check Constraint

Book an audit with Zokyo

Summary

Related Vulnerabilities: 1. Under-constrained Circuits, 2. Nondeterministic Circuits, 4. Mismatching Bit Lengths

Identified By: Veridise Team

The Circom-Pairing circuits, written in circom, are used for the Succinct Labs' bridge that is based on cryptographic protocols. However, the circuits were missing a constraint to ensure proper range checks.

Background

The Circom-Pairing circuit needs to use integers larger than the prime field (254 bits), so it uses the circom big-int library. Therefore, numbers are represented as k-length arrays of n-bit numbers to represent a much larger number. Even though Circom-Pairing uses very large numbers, there is still a max range of expected numbers to be used. To ensure that numbers are constrained to the expected max range, the following circuit is often used:

template BigLessThan(n, k){
  signal input a[k];
  signal input b[k];
  signal output out;
  ...
}

The output of this circuit will be 1 if a < b, and 0 otherwise.

The Vulnerability

The vulnerability arose in the CoreVerifyPubkeyG1 circuit:

template CoreVerifyPubkeyG1(n, k){
  ...
  var q[50] = get_BLS12_381_prime(n, k);

  component lt[10];
  // check all len k input arrays are correctly formatted bigints < q (BigLessThan calls Num2Bits)
  for(var i=0; i<10; i++){
    lt[i] = BigLessThan(n, k);
    for(var idx=0; idx<k; idx++)
      lt[i].b[idx] <== q[idx];
  }
  for(var idx=0; idx<k; idx++){
    lt[0].a[idx] <== pubkey[0][idx];
    lt[1].a[idx] <== pubkey[1][idx];
    ... // Initializing parameters for rest of the inputs
}

The BigLessThan circuit is used to constrain pubkey < q to ensure that the pubkey values are correctly formatted bigints. However, the rest of the circuit never actually checks the output of these BigLessThan circuits. So, even if a proof has pubkey >= q and BigLessThan outputs 0, the proof will successfully be verified. This could cause unexpected behavior as the cryptographic protocol depends on these numbers being within the expected range.

The Fix

The fix required a constraint on all of the outputs of the BigLessThan circuits to ensure that each one had an output of 1. The following snippet was added to fix this:

var r = 0;
for(var i=0; i<10; i++){
    r += lt[i].out;
}
r === 10;

Once this was added, each BigLessThan circuit was then constrained to equal 1. Now, the pubkey inputs can be trusted to be in the expected range.

Conclusion

1. Purpose of the CoreVerifyPubkeyG1 Circuit: Within this circuit, there's a function to ensure that the pubkey values (probably public keys in the cryptographic protocol) are indeed less than a particular value q (a given prime number, likely a significant threshold in the protocol). This is to ensure that public keys are within a specific valid range.

2. The Oversight: While the circuit does make a comparison between pubkey and q using the BigLessThan circuit, it doesn't do anything with the result. In simpler terms, the circuit checks if the public key is too big but then doesn't act upon that information. This means even if the public key is too large (an invalid input), the overall protocol would still accept it, which is a significant vulnerability.

References

1. Veridise Explainer Article

2. Commit of the Fix