MTZK: Testing and Exploring Bugs in Zero-Knowledge (ZK) Compilers

Zero-knowledge (ZK) proofs have been increasingly popular in privacy-preserving applications and blockchain systems.To facilitate handy and efficient ZK proof generation for normal users, the industry has designed domain-specific languages (DSLs) and ZK compilers.Given a program in ZK DSL, a ZK compiler compiles it into a circuit, which is then passed to the prover and verifier for ZK checking.However, the correctness of ZK compilers is not well studied, and recent works have shown that de facto ZK compilers are buggy, which can allow malicious users to generate invalid proofs that are accepted by the verifier, causing security breaches and financial losses in cryptocurrency.In this paper, we propose MTZK, a metamorphic testing framework to test ZK compilers and uncover incorrect compilations.Our approach leverages deliberately designed metamorphic relations (MRs) to mutate ZK compiler inputs.This way, ZK compilers can be automatically tested for compilation correctness using inputs and mutated variants without requiring manual intervention.We propose a set of design considerations and optimizations to deliver an efficient and effective testing framework.In the evaluation of four industrial ZK compilers, we successfully uncovered 21 bugs, out of which the developers have promptly patched 15.We also show possible exploitations of the uncovered bugs to demonstrate their severe security implications.