Fix Critical Security Vulnerability Caused by Circom Operator Misuse

[bruno-valante]

Dear crema-labs team,

I am a web3 developer who recently came across your project while searching for an open-source AES implementation in Circom. Your project impressively implements the functionality of AES algorithm and CTR mode with clean, concise code that is easy to use. We appreciate your generosity in contributing this work to the open-source community under the MIT license.

However, we have identified some misuses of Circom syntax that lead to significant security vulnerabilities. In Circom, the --> and ==> operations are distinctly different. The latter combines --> with ===. The --> operation indicates how an honest prover should compute intermediate and output signals from input signals, while === adds corresponding constraints to the underlying R1CS system, ensuring that only inputs satisfying these constraints can pass zero-knowledge proof verification.

Therefore, most Circom code uses ==> for assignments to ensure the logic is encoded into the underlying R1CS system. The rare uses of --> include the Num2Bits template in circomlib's bitify.circom, where binary expansion computation is more complex than result verification due to R1CS limitations. Since R1CS (rank-1 constraint system, the underlying constraint system of Circom) only supports addition and multiplication in large prime fields, computing binary expansion is more difficult than verifying the expansion result. Binary expansion computation requires bitwise operations, which are not supported by the R1CS, while verifying the expansion result can be done using only multiplication and addition. Therefore, this template uses --> to compute the binary expansion, and checks the expansion result through the last line lc1 === in.

In your code, --> is used in some places without output verification, such as in SBox calculations. This allows malicious provers to arbitrarily specify SBox output results without detection by the zero-knowledge proof system. This is also why, when running yarn compile:test, it encounter numerous warnings such as

warning[CA01]: In template "SBox128()": Local signal out does not appear in any constraint.

This occurs because your code only specifies the behavior for an honest prover, without adding constraints to restrict a malicious prover from providing incorrect inputs.

We have reviewed all uses of --> in your code and made the following fixes:

1. Convert the round parameter to a template parameter, ensuring it's a compile-time constant rather than a signal (which malicious provers cannot modify).

2. Reimplement SBox and TBox using finite field operations instead of lookup tables, which are costly in R1CS. We've implemented basic GF(2^8) operations in finite_field.circom. For the finite field multiplication inversion operation (required for SBox calculation), we first find the inverse element through a lookup table, then perform finite field multiplication (which is much cheaper than finite field division).

3. Add overflow checks for IV+Nonce addition in GenerateCounterBlocks, supporting full 16-byte carry (instead of just the least significant 4 bytes).

4. Add input validation to EncryptCTR function, ensuring all signals are uint8 integers, preventing malicious provers from inputting out-of-range values.

We've applied and tested these modifications in our project. We're offering these changes to enhance your code's security and reliability.

These fixes increase non-linear constraints from 17,088 to 54,608 in cipher_4.circom compilation. This increase is due to the inclusion of computational checks for the heaviest operations, which were previously omitted.

We look forward to your feedback and would be happy to discuss these changes further.

Best regards,
Bruno

[Nesopie]

Hi Bruno,

Thank you for your review and the changes you shared! We appreciate your effort in improving the security of our code. We’ll reviewed your suggestions and are keen on merging them into the project soon