2023/04/15 by Junrui Liu, Liu, Junrui, Ian Kretz +17 · 1 citation
Computer Science · #Cryptography and Data Security #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Physical Unclonable Functions (PUFs) and Hardware Security #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2304.07648
openalex publication_date 2023/04/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Zero-knowledge (ZK) proof systems have emerged as a promising solution for building security-sensitive applications. However, bugs in ZK applications are extremely difficult to detect and can allow a malicious party to silently exploit the system without leaving any observable trace. This paper presents Coda, a novel statically-typed language for building zero-knowledge applications. Critically, Coda makes it possible to formally specify and statically check properties of a ZK application through a rich refinement type system. One of the key challenges in formally verifying ZK applications is that they require reasoning about polynomial equations over large prime fields that go beyond the capabilities of automated theorem provers. Coda mitigates this challenge by generating a set of Coq lemmas that can be proven in an interactive manner with the help of a tactic library. We have used Coda to re-implement 79 arithmetic circuits from widely-used Circom libraries and applications. Our evaluation shows that Coda makes it possible to specify important and formally verify correctness properties of these circuits. Our evaluation also revealed 6 previously-unknown vulnerabilities in the original Circom projects.