Certifying Zero-Knowledge Circuits with Refinement Types

Junrui Liu; Ian Kretz; Hanzhi Liu; Bryan Tan; Jonathan Wang; Yi Sun; Luke Pearson; Anders Miltner; Işıl Dillig; Yu Feng

Paper 2023/547

Certifying Zero-Knowledge Circuits with Refinement Types

Junrui Liu

, University of California, Santa Barbara

Ian Kretz, The University of Texas at Austin

Hanzhi Liu, University of California, Santa Barbara, Veridise Inc.

Bryan Tan, Veridise Inc.

Jonathan Wang, Axiom

Yi Sun, Axiom

Luke Pearson, Polychain Capital

Anders Miltner

, Simon Fraser University

Işıl Dillig

, The University of Texas at Austin, Veridise Inc.

Yu Feng

, University of California, Santa Barbara, Veridise Inc.

Abstract

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.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Preprint.
Keywords: zero knowledge verification
Contact author(s): junrui @ cs ucsb edu
kretz @ cs utexas edu
hanzhi @ ucsb edu
bryan @ veridise com
jonathanpwang @ protonmail com
yi sun @ post harvard edu
luke @ polychain capital
miltner @ cs sfu ca
isil @ cs utexas edu
yufeng @ cs ucsb edu
History: 2023-08-30: last of 2 revisions; 2023-04-18: received; See all versions
Short URL: https://ia.cr/2023/547
License: CC BY

BibTeX

@misc{cryptoeprint:2023/547,
      author = {Junrui Liu and Ian Kretz and Hanzhi Liu and Bryan Tan and Jonathan Wang and Yi Sun and Luke Pearson and Anders Miltner and Işıl Dillig and Yu Feng},
      title = {Certifying Zero-Knowledge Circuits with Refinement Types},
      howpublished = {Cryptology ePrint Archive, Paper 2023/547},
      year = {2023},
      note = {\url{https://eprint.iacr.org/2023/547}},
      url = {https://eprint.iacr.org/2023/547}
}