One of our favorite things to do at Veridise is to perform security audits of zero-knowledge proofs (ZKPs). In this article, we will explore what zero-knowledge proofs are, how you can construct them using a domain-specific language like Circom, and how to use the artifacts generated by the Circom compiler.
What are Zero-Knowledge Proofs?
At a high-level, zero-knowledge proofs allow one party (namely, ”the prover”) to prove to another party (”the verifier”) the correctness of a statement ϕ without revealing any other information other than the fact that ϕ is valid. Recently, ZKPs have gained widespread adoption as a way of addressing privacy issues in smart contracts and for facilitating scalable layer-2 blockchain solutions known as “ZK-Rollups”.
ZKPs can come in several different forms, depending on the size of the proof, whether they are interactive or not, and the necessity of a trusted set-up. In the rest of this article, we will mainly focus on zkSNARKs (Zero Knowledge Succinct Non-interactive ARgument of Knowledge), which have become quite popular in the context of blockchain applications. As their name indicates, zkSNARKs are a family of non-interactive ZKPs that allow succinct proofs, and therefore, constant verification time. Because of the popularity of zkSNARKs, domain-specific languages like Circom and Halo2 have emerged as a way of facilitating the construction of ZKPs.
Constructing ZKPs with Circom
How does one construct a zero-knowledge proof in a domain-specific language like Circom? To illustrate this, suppose that we have some computation F for which we want to construct a zero-knowledge proof — that is, given some input x, we want to prove (in a zero-knowledge way!) that F(x) is equal to y. To do so, one expresses two things as part of their Circom program:
- the computation F, referred to as a “witness generation program” in Circom lingo, and
- a constraint system C, which is essentially a set of polynomial equations over a finite field.
As an example, consider the Circom program (often referred to as ”arithmetic circuit”) shown below.
This circuit takes two inputs, a and b, and produces two outputs, o1 and o2. The program makes use of three widely-used Circom operators:
- The operator
<--is used for performing assignment and only contributes to computation (witness generation); - The operator
===is used to generate a constraint to add to the constraint system C; - The operator
<==is used for both performing assignment and for constraint generation. In particular,x <== eis shorthand forx <-- eandx === e.
Thus, our example Circom program corresponds to the witness generator F and constraints C shown in the figure above. Note that while this example is written in Circom, the concepts are more general as they apply to other ZK languages such as Halo2.
From Constraints to ZKPs
So, let’s say we’ve written a Circom program like the example program above. How do we generate a zero-knowledge proof from it?
First, you use the Circom compiler to compile the constraints C to a Rank 1 Constraint System (R1CS), which is essentially a set of degree-2 polynomial equations over a finite field. Because the Circom compiler places restrictions on how the === and <== can be used, the resulting constraints are relatively straightforward to convert to R1CS. Next, once we have an R1CS constraint, we can use a zkSNARK generator such as (snarkjs) to generate a prover P and verifier V. This process is illustrated below.
How to Use these Artifacts
OK, great! Now, we have a prover and verifier, but where does the witness generator come into play and how do we use these artifacts in a zero-knowledge system?
The figure above shows how two parties, say Alice and Bob, can use the artifacts produced by the Circom compiler to (respectively) prove and verify that F(x) is equal to y in a zero-knowledge way. First, Alice uses the witness generator to compute the values of all signals, including intermediate ones. These values are then passed to the prover P which produces a zero-knowledge proof that F(x) = y. On the other end, Bob uses the verifier V to check that the proof is correct.
Conclusion
Domain specific languages like Circom try to make it easy to build ZKP applications by producing a witness generator and an R1CS constraint system. The latter can be fed into a zkSNARK generator to produce a prover and verifier. These three artifacts (witness generator, prover, and verifier) can then be used to build a zero knowledge application.
However, don’t let the word “verification” trick you into thinking that nothing can go wrong in this process! Indeed, if your Circom program has a bug, then the verifier could easily “verify” bogus proofs, undermining the whole process. In the next blog post, we will talk about some common problems in ZKP development and how you can avoid them!
About Veridise
Veridise is a blockchain security company that provides audits and software analysis tools for all layers of the blockchain ecosystem, including smart contracts, web3 applications, zero-knowledge circuits, and blockchain implementations. Co-founded by a team of formal verification and software security researchers, Veridise provides state-of-the-art tooling for hardening blockchain security. Our clients can work with us in a variety of ways, including hiring us for security audits, using our automated security analysis tools (for testing, static analysis, formal verification), or a combination of these.
If you’re interested in learning more information, please consider following us on social media or visiting our website:
Website | Twitter | Facebook | LinkedIn | Github | Request Audit
