Zero-Knowledge, Maximum Security: Hardening ZKP Circuits with Formal Methods
Abstract: Zero-knowledge proofs are powerful cryptographic protocols for enhancing privacy and scalability in blockchains. However, ensuring the correctness and security of zero-knowledge proofs is a challenging task due to its complex nature. This talk aims to address this challenge by leveraging formal methods with a pipeline of increasing confidence, ranging from a domain-specific solver for detecting under-constrained circuits (PLDI'23), to formal verification for functional correctness using refinement types (Oakland'24). By applying formal methods with complementary strength, we have been working on rigorous techniques to detect vulnerabilities, verify correctness, and enhance the resilience of zero-knowledge proof systems against attacks.
Biodata: Yu Feng is an assistant professor in the Department of Computer Science at UCSB. Yu's research is focused on developing automated programming techniques that combine program synthesis and program analysis to enhance software usability, reliability, and security. His research group had developed many tools for hardening Web3 security including smart contracts, consensus protocols, wallets, and ZKP circuits. Yu has been recognized with prestigious academic awards for his contributions to the field, including best paper awards from top PL (PLDI’18, PLDI’22), software engineering (ASE’20), and HCI (CHI’21) conferences. He is also the recipient of the Google Faculty Award, the Ethereum Academic Award, and many others.