Audit of Reclaim Protocol's ChaCha20 Circuit
September 23rd, 2023

Description. The Add32Bits gadget constrains the addition of two (assumed to be 32-bit) values to wrap around. In other words, if the addition of two 32-bit values overflows, the gadget removes the carry bit (the 33rd most-significant bit).

To do that, the logic witnesses a carry bit, which is used to remove the carry from the result if set to 1:

tmp <-- (a + b) >= (0xFFFFFFFF + 1) ? 1 : 0;
tmp * (tmp - 1) === 0;
out <== (a + b) - (tmp * (0xFFFFFFFF + 1));

The problem is that the carry bit tmp is not constrained to be correctly computed. That is, there are two scenarios in which this function can be maliciously used:

1. If $a+b$ are overflowing (the result is 33 bits), then you can set tmp=0 and the output will be 33 bits
2. If $a+b$ is not overflowing (the result is 32 bits), then you can set tmp=1 and the output will underflow (it should be around the bit size of the circuit field)

Both are problems if the output is not constrained to be 32 bits on the caller side, which seems to be the case.

Recommendations. In addition to fixing the issue, document the function to warn callers that they must be ensure that the two inputs are well-constrained to be 32-bit values.

Client response. The client fixed the issue by encoding the operation on the bits of the operands. This ensured that the result of adding the two 32-bit values had a unique decomposition of 32 bits and a carry bit.

Specifically, they add the two packed values together (as field elements):

$r = \sum_{i=0}^{31} a_i 2^i + \sum_{i=0}^{31} b_i 2^i$

and then unpack them in a 32-bit result $(r_0, \cdots, r_{31})$ plus a carry $c$:

$r = \sum_{i=0}^{31} r_i 2^i + 2^{32} c$

where $a_i, b_i$ are the inputs considered to be valid values, and the rest of the variables ($r_i$ and $c$) are constrained to be 0 or 1.

Description. The RotateLeft32Bits gadget is used to perform left rotations of (assumed to be 32-bit) values. The rotation is parameterized by an argument given to the Circom template.

The following snippet shows where the issue lies in:

signal part1 <-- (in << L) & 0xFFFFFFFF;
signal part2 <-- in >> (32 - L);
(part1 / 2**L) + (part2 * 2**(32-L)) === in;

As one can see, both part1 and part2 are witness values that are constrained only by the last line.

The problem is that the constraint is not enough, and both part1 and part2 can be chosen arbitrarily. For example, by following these steps:

• fix $\text{part2}$ arbitrarily
• set $\text{part1} = (\text{in} - \text{part2} \cdot 2^{32 - L}) \cdot 2^L$

Using sage, one can easily find such values:

# default circom circuit field
p = 21888242871839275222246405745257275088548364400416034343698204186575808495617
F = GF(p)

# settings
in_ = F(5) # input is 5
L = 3 # rotation of 3

# fix part2 to 2, for example
part2 = F(2)

# compute part1 as shown above
part1 = (in_ - part2 * 2^(32-L)) * 2^L
part1
21888242871839275222246405745257275088548364400416034343698204186567218561030

# the constraint passes
(part1 / 2^L) + (part2 * 2^(32-L)) == in_
True

Recommendations. Constrain part1 (resp. part2) to be $32-L$ (resp. $L$) bit-sized values.

In addition, add documentation to ensure that the caller is aware that the inputs have to be well-constrained 32-bit values. Consider changing the name of the function to emphasis that it is not validating the inputs. (Usually the keywords unchecked or unsafe appended at the end of the template name are good indicators.)

Client response. The client fixed the issue by manually re-ordering bits based on a shift (L):

for (var i = 0; i < BITS; i++) {
    out[i] <== in[(i + L) % BITS];
}

As one can see using zkSecurity's circomscribe tool (introduced here), the circuit correctly routes the bits:

Description. The XorWords gadget constraints the XOR of two arrays of M-bit values (for some fixed array size and value M).

In order to implement the XOR in-circuit, the logic implements the XORs bit by bit. It was found that the bit constraints for the witness values were commented at the time of the audit:

abits[l] <-- ain >= j ? 1 : 0;
bbits[l] <-- bin >= j ? 1 : 0;
// ensure abits[l] and bbits[l] are either 0 or 1
// below should be uncommented in prod?
// abits[l] * (abits[l] - 1) === 0;
// bbits[l] * (bbits[l] - 1) === 0;
xors[l] <== abits[l] + bbits[l] - 2 * abits[l] * bbits[l];

In addition, the bit decomposition of both operands a and b must be constrained to be correct. While the gadget's logic attempt to do just that, it was found that the check was flawed.

Iteration of each bitstring goes through the following logic, cleaned up to showcase only the checks applied to the variable a[i]:

ain = a[i];

// TRUNCATED...

for(j = 2 ** (M-1);j >= 1;j /= 2) {
    abits[l] <-- ain >= j ? 1 : 0;

    // TRUNCATED...

    ain -= abits[l] * j; // ain -= bit[j] * 2^j

    // TRUNCATED...
}

ain * a[i] === 0;

As you can see, the last check constraints that ain * a[i] == 0. This is true if either ain = 0 or a[i] == 0.

What we really want to check is that ain = 0, but the check doesn't apply if the value of a[i] is 0.

In the case where the value of a[i] is 0, then a malicious prover can use an arbitrary bit decomposition for a[i].

Recommendations. Use circomlib's Num2Bits function to convert both operands to bitstrings.

Client response. The client fixed the issue by enforcing an XOR constraint ($\text{res} = a + b - 2 a b$) on each bits individually. As one can see using zkSecurity's circomscribe tool (introduced here), the constraint is correctly enforced by the circuit (which includes correctly constraining the quadratic term):

Description. The ChaCha20 interface exposed by the library takes a key, nonce, a starting counter, and a plaintext (or ciphertext as the encryption and decryption algorithm is the same).

As there's usually a common way to initialize the nonce part of the algorithm, it might be safer to not have the user provide it. As per RFC 7539:

A 32-bit initial counter. This can be set to any number, but will usually be zero or one. It makes sense to use one if we use the zero block for something else, such as generating a one-time authenticator key as part of an AEAD algorithm.

In addition, the interface seems to be easy to misuse as it does not constrain any of the inputs provided (which are assumed to be 32-bit inputs).

At the very least, the documentation should warn the user that they must take care of constraining the inputs to be 32-bit values. Changing the template name to ChaCha20Unsafe or ChaCha20Unchecked is a good way to warn users that they must be careful when using this interface.

In addition, it might make sense to provide an alternative interface that enforces these checks on all the inputs.