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

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

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.