The Challenges of Developing Zero-Knowledge Proofs
In this post, we’ll look at the challenges developers encounter when developing Zero-Knowledge Proofs: performance and programmability.
Zero-Knowledge Proofs
Firstly, let’s briefly repeat what Zero-Knowledge Proofs are. A Zero-Knowledge Proof (ZKP) is a cryptographic technique that allows:
- a prover to convince to a verifier that it executed a computation correctly (computational integrity),
- while keeping some inputs confidential (confidentiality).
For a more detailed description of ZKPs, we refer to this blog post by Vitalik Buterin explaining the maths behind zk-SNARKs, this more high-level article explaining what ZKPs are, and this YouTube video explaining ZKPs at different levels of abstraction.
In the rest of this post, we will be using the ZoKrates programming language to create ZKPs. This example program proves knowledge of the factors of a (large) number:
def main(private field a, private field b) -> field {
assert(a > 1 && b > 1);
return a * b;
}
This program takes in two inputs a and b, which are numbers in a finite field (up to ~255-bit). The keyword private indicates that these inputs are kept confidential. The program first checks that both a and b are greater than 1 and then returns their product.
After this program is executed, a proof is generated that contains the result of the computation, but not the (private) inputs. This proof can be verified to check that the computation was executed correctly, without revealing the inputs.
When executing the program with the inputs
123456789and987654321, the proof ends up looking like this:{ "scheme": "g16", "curve": "bn128", "proof": { "a": [ "0x2438520bf50f1ef4f0cbd71ad04069c72e4683b88f5f2becb98bbf7c0c101582", "0x1940ec3fb0df60726e6bc95e196171e826b00453a106a6085d61d4327ea445cb" ], "b": [ [ "0x2403a661a61aa80b86fe5515547e99e9d8139d5f892c9a29b03f0e2eda82677b", "0x0cc2321418da1284478f2a9397d279eddecfb631965981c934d065f6c058e2f1" ], [ "0x2865222599023b1bb0776c8c5eb23b780d0cf2659d4ccb4e511e2df22b9612f2", "0x195051b7b0cb3aa2577aa3b99376bd44b8424125db2350015331288cdd2be045" ] ], "c": [ "0x05759e3efb49a3dc8c11cf7fdb4cbd152dd64b1d233f8a9da03a03afac532a4d", "0x286af8c6919b3053acef0fad338b38bc91e92071d6fe3757cc083d79639e7cf6" ] }, "inputs": [ "0x00000000000000000000000000000000000000000000000001b13114fbff5385" ] }Here, the
inputscontains the public inputs and outputs, in this case only the product of the two secret factors (121932631112635269 in hex). Together with the other numbers and a verification key, this forms a proof that can be verified by anyone. The proof is tied to this particular program.
Similarly, the following ZoKrates program proves that the prover knows the pre-image of a SHA256 hash, without revealing the input (relying on the sha256 function of ZoKrates’ standard library):
def main(private u8[256] input) -> u32[8] {
return sha256(input);
}
In other words, a proof generated by this program shows that the prover knows an input that hashes to a particular hash. This can be used to show that a prover knows a password, without revealing the password.
Hashes are also used to create a commitment to secret data: multiple programs can prove that they are using the same input data, while keeping this data secret, by each calculating and returning the hash. If two programs output the same hash, we know they must have used the same input to the hash, but we cannot deduce this (secret) input because the hash is a one-way function.
Performance
The program that calculates the SHA256 hash of a 256-byte input is quite slow. (The program corresponds to a circuit of 145560 constraints.) On a MacBook Pro with a 2.3 GHz 8-Core Intel Core i9 from 2019:
- compiling the program takes 19 seconds (this only needs to happen once per program),
- performing the set-up takes 8 seconds (this generates keys that are used by prover and verifier, and only needs to happen once per prover–verifier pair),
- computing the witness takes 6 seconds (this actually executes the program, and keeps track of the intermediate values),
- generating the proof takes 7 seconds,
- while verification takes 16 milliseconds.
Moreover, the performance characteristics of ZKPs are non-obvious. As these programs are compiled to arithmetic circuits that work on a finite field, their performance is quite different from ‘normal’ programs. For example:
- For an
if, both branches are executed. This also means no short-circuiting of&&and||. - Loops must have a static bound and are unrolled.
- The performance of different operations can be quite different:
- Operations are in a finite field, so addition is fast but division is slow. Moreover, overflow checks may be needed.
- Operations that work on the types
u8, …,u32,u64may need to be emulated using operations on their individual bits.
Programmability
When programming ZKPs, it’s very easy to make mistakes, which can have severe consequences.
For example, when writing a program to prove knowledge of the factors of a number n, a first attempt might be:
def main(private field a, private field b) -> field {
return a * b;
}
However, this program allows the prover to generate a trivial proof by picking a = 1 and b = n, hence allowing the prover to generate a valid proof without knowing the factors of n. This breaks the computational integrity we expected as verifier.
As another example, the program above that proves knowledge of the pre-image of a SHA256 hash actually contains a mistake (depending on the use case): as the input is not salted, the verifier may be able to guess the input by brute-forcing all possible inputs. This breaks the confidentiality that we expected as prover. A better implementation would have been:
def main(private u8[256] input, private u8[256] salt) -> u32[8] {
return sha256([...input, ...salt]);
}
Such bugs have been observed in practice [1], [2], appearing in popular projects like the Bulletproofs paper, zcash, and Circom’s standard library. These bugs are hard to find and hard to fix, as they require a deep understanding of the program and the cryptographic properties of the ZKP. Note also that many existing bug detection and static analysis tools focus on finding the first kind of problem (bugs that produce incorrect outputs), and not accidental leaks of confidential information.
Finally, the ZoKrates language (as well as other languages for ZKPs) is quite limited. For instance, there is no support for floating-point numbers or strings. The standard library is also very limited, with support for (1) hashing, (2) operations on elliptic curves, (3) EdDSA signature verification, and (4) some functions for type conversion; but not much else.
Conclusion & Future work
In this post, we described the main challenges of developing ZKPs: their slow and non-obvious performance, and how easy it is to introduce bugs that break confidentiality or computational integrity.
In a next post, we will introduce our current solutions for these problems, as well as our vision on how to improve this more generally in the future.
References
- ZK Bug Tracker
- Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Işıl Dillig, and Yu Feng. 2023. Certifying Zero-Knowledge Circuits with Refinement Types.
- Shankara Pailoor, Yanju Chen, Franklyn Wang, Clara Rodríguez, Jacob Van Geffen, Jason Morton, Michael Chu, Brian Gu, Yu Feng, and Işıl Dillig. 2023. Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs. In Proceedings of Programming Language Design and Implementation (PLDI).
- Hongbo Wen, Jon Stephens, Yanju Chen, Kostas Ferles, Shankara Pailoor, Kyle Charbonnet, Işıl Dillig, and Yu Feng. 2023. Practical Security Analysis of Zero-Knowledge Proof Circuits. In USENIX Security ’24.
- Stefanos Chaliasos, Jens Ernstberger, David Theodore, David Wong, Mohammad Jahanara, and Benjamin Livshits. 2024. SoK: What don’t we know? Understanding Security Vulnerabilities in SNARKs.