Finding bugs in large ZK circuits with CIVER

The COSTA research group has started a new collaboration with the ZisK development team to apply CIVER to verify the determinism of the recursion/aggregation circuits of ZisK.

CIVER has already been able to find vulnerabilities in several projects in production (see [1] for details).

The size of these ZisK circuits ranges from one million to over five million constraints, so verifying them and finding bugs is very challenging. Other tools have shown to be unable to handle circuits of this size at once.

Using CIVER we have detected two subtle bugs which compromise the soundness of ZisK. Thanks to using CIVER these bugs have been detected in the development process and will not reach the production phase. CIVER has been able to spot the problematic components and provide a buggy instance.

Verifying circuits with CIVER

CIVER [1] is a tool that can verify weak safety [2], also known as determinism, which means there is a single valid output for any given inputs. When this property is not satisfied it means that the circuit is underconstrained, as all non expected values that are valid for the outputs should be restricted. CIVER can verify weak safety of circuits defined using the DSL circom, but can also verify circuits given as a constraints system (in R1CS format, PLONK, ACIR, …). CIVER modularly analyses the circuit to increase scalability and to find the problematic part of the circuit.
When the circuit is provided in the circom language, it uses the structure of the circuit definition to modularly check all the components. CIVER can also check Pre/Postconditions defined on circom programs, as well as verify circom's tag specifications. CIVER has been integrated in the circom compiler and can handle full circom programs.
When CIVER is applied to non-circom circuits powerful clustering techniques are applied in order to break the circuit into smaller components that are then handled modularly.

Details about the bugs

The first bug was detected in a circom template called Num2Ternary(n) that transforms an input number to its ternary form (i.e. in base 3) using n values in {0..2} expressed in binary form.
The second bug was detected in a template called SignFp, which given an input number

The Num2Ternary bug

The circom code of this template is as follows:

template Num2Ternary(n) {
    signal input in;
    signal output {binary} out[n][2];
    var lc1=0;

    var e3=1;

    signal ternary_digits[n];
    for (var i = 0; i<n; i++) {
        ternary_digits[i] <-- (in \ e3) % 3;
        lc1 += ternary_digits[i] * e3;
        e3 *= 3;
        out[i] <== Num2Bits(2)(ternary_digits[i]);
    }

    lc1 === in;
}

Note that the output

The problem with this circuit is that although the intended behavior would be that the values of all numbers in

in === ternary[0] + 3 * ternary[1] + 9 * ternary[2] + 27 * ternary[3]
out[0] === Num2Bits(2)(ternary[0])
out[1] === Num2Bits(2)(ternary[1])
out[2] === Num2Bits(2)(ternary[2])
out[3] === Num2Bits(2)(ternary[3])

Then, since

• $ternary[0]=0,ternary[1]=1,out[1]=[0,1]$, and the rest all zeros,which is the expected one, and
• $ternary[0]=3,out[0]=[1,1]$, and the rest all zeros, which is not expected.

CIVER was able to produce a counter example showing this bug.

The issue can be found here.

The SignFp bug:

This is a more critical bug, since for every input the circuit is not deterministic.
The code of SignFp is the following:

// Given a ∈ Fp and sign ∈ {0,1}, checks sign == sign(a) := a % 2
template SignFp() {
    signal input a;
    signal output {binary} sign;

    sign <-- a % 2;
    sign * (1 - sign) === 0;
    signal q <-- a \ 2;
    a === 2 * q + sign;
}

Here the problem is that for instance, for

• If
  $a$ is even:
  • $q=a\mathrm{\setminus }2,sign=0$ (expected solution)
  • $q=-1\mathrm{\setminus }2+a\mathrm{\setminus }2,sign=1$ (alternative solution)
    (Recall that
    $\mathrm{\setminus }$ is the field division.)
• If
  $a$ is odd:
  • $q=(a-1)\mathrm{\setminus }2,sign=1$ (expected solution)
  • $q=1\mathrm{\setminus }2+(a-1)\mathrm{\setminus }2,sign=0$ (alternative solution)

The issue can be found here.

Full ZisK recursion/aggregation verification

The full verification of the recursion/aggregation circuits is not finished yet. When done, a complete public report will be delivered.

References

[1] Miguel Isabel, Clara Rodríguez-Núñez, Albert Rubio. Scalable verification of zero-knowledge protocols. 2024 IEEE Symposium on Security and Privacy (SP). DOI:10.1109/SP54263.2024.00133
[2] Marta Bellés-Muñoz, Miguel Isabel, Jose Luis Muñoz-Tapia, Albert Rubio, Jordi Baylina.
Circom: A Circuit Description Language for Building Zero-Knowledge Applications. IEEE Transactions on Dependable and Secure Computing, 2022. DOI:10.1109/TDSC.2022.3232813