Collaborative Research: FMitF: Track I: Automating and Synthesizing Parallel Zero-Knowledge Protocols

零知识证明（ZKP）协议允许一方向其他人证明陈述的正确性，而无需透露原因。虽然ZKP协议在密码学中是一个相对古老且易于理解的概念，但由于其在区块链隐私、私有审计、可验证计算和匿名网络中的许多应用，它最近再次成为人们关注的焦点。虽然ZKP协议提供了令人兴奋的功能，但它们也带来了巨大的计算资源开销。为了使ZKP协议达到与机器学习算法相同的实际意义水平，需要一个自动化框架，即使是非密码学家也可以开发由可并行协议支持的优化应用程序。从密码学的角度来看，该项目更广泛的意义和重要性正在推进最先进的ZKP协议的可部署性。该项目的新颖之处在于ZKP协议的正式系统化，以获得新的并行和高度优化的ZKP算法。此外，研究人员正在开发一门课程，包括正式计算方法和密码学的基础及其在实际环境中的应用。通过充分利用分布式计算和特定于zkp的优化所提供的可伸缩性和成本节约，该框架使非专业程序员能够在该领域编写高效且直观的程序。特别是，该项目使没有密码学背景的程序员能够编写ZKP应用程序，自动获得算法的优化版本，并将它们部署在多台机器上，以改进端到端运行时间。该框架的特点是(i)一种编程语言，开发人员可以用顺序思维来编写应用程序；（ii）一个编译和优化工具集，可以首先优化程序，然后自动将生成的应用程序分割成更小的应用程序；（iii）一组支持组件，可以帮助程序员验证和合成框架语言中的代码。从形式化方法的角度研究并行化ZKP协议的问题，其中出现了许多新的研究问题，涉及新的优化问题，需要仔细的语言设计和严格的安全性证明。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Zero-knowledge proof (ZKP) protocols allow one party to prove to others the correctness of a statement without revealing why. Although a relatively old and well-understood concept in cryptography, ZKP protocols recently came into the spotlight again given their many applications in blockchain privacy, private auditing, verifiable computation, and anonymous networks. While ZKP protocols offer exciting capabilities, they also come with a huge overhead in computational resources. For ZKP protocols to reach the same level of practical significance as machine learning algorithms, an automated framework is needed that can allow even non-cryptographers to develop optimized applications backed by parallelizable protocols. The project's broader significance and importance are advancing deployability of state-of-the-art ZKP protocols from a cryptography perspective. The project's novelties are the formal systematization of ZKP protocols to obtain novel parallel and highly optimized ZKP algorithms. Furthermore, the investigators are developing a course that encompasses the foundations of formal computing methods and cryptography and their applications in practical settings.The framework enables non-expert programmers to write efficient and intuitive programs in that domain, by taking full advantage of the scalability and cost savings offered by distributed computing and ZKP-specific optimizations. In particular, the project enables programmers with little background in cryptography to write ZKP applications, automatically obtain optimized versions of the algorithms, and deploy them on multiple machines for improved end-to-end running time. The framework features (i) a programming language where developers can write applications with a sequential mindset, (ii) a compilation and optimization toolset that can first optimize the program and then automatically partition the resulting application into smaller ones, and (iii) a set of supporting components that can help programmers verify and synthesize code in the framework's language. The problem of parallelizing ZKP protocols is studied from a formal methods lens, where many new research questions emerge regarding new optimization problems requiring careful language design and rigorous proofs of security.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.