Automated Soundness and Completeness Vetting of Polygon zkEVM

Zero-knowledge rollups have emerged as popular layer 2 scaling solutions for blockchains. Polygon zkEVM, a leading deployment of zk rollups, leverages non-deterministic execution to derive free inputs from an unconstrained command evaluator when implementing the zkEVM. This mechanism significantly simplifies the design of zkEVM and enhances the performance of proof generation. However, it introduces the challenge of requiring developers to define constraints for free inputs, a task that demands strong mathematical expertise and is prone to errors. As a component of the layer-2 infrastructure, the zkEVM's vulnerabilities could lead to powerful attacks. However, despite their importance, the security of free inputs in zkEVM remains unexplored. In this paper, we present the first systematic exploration of free inputs in Polygon zkEVM. Our study reveals critical soundness and completeness issues with them. In particular, we uncover a new attack surface, termed the dual execution path attack, which targets unsound implementations of free inputs and can lead to chain splits. Moreover, we design the first tool, FreeVer, which facilitates the verification of the soundness and completeness of free inputs with formal semantics. Additionally, it automatically generates formal specifications for correct constraints by constructing prover state graphs that model both the behaviors of malicious and honest provers. It then uses the states from the honest prover as specifications to assist in the verification of states from the malicious one. FreeVer also adopts optimization strategies to reduce the complexity of constraints for effective verification. Our evaluation results show that FreeVer can correctly identify all previously disclosed free input related vulnerabilities and detect 7 new vulnerabilities in Polygon zkEVM. All detected bugs are submitted through the bug bounty program and are confirmed as high impact vulnerabilities.