SaTC: CORE: Small: Compilation and Backend-Independent Optimization for Multi-Party Computation

在大数据分析和机器学习的时代，构建安全的(隐私保护)系统是一个非常重要的问题。算法聚合数据并构建预测模型，当它们聚合来自许多不同各方的数据时，预测模型变得更加准确。如此大规模的聚合引发了安全和隐私方面的担忧。安全多方计算(MPC)是一种允许双方或多方在不泄露其数据信息的情况下对其私有数据执行计算的方法。在理论密码学领域，MPC在编程技术方面取得了长足的进步。它已经在密封拍卖、标杆公司业绩、隐私保护机器学习、生物特征匹配等场景中得到实践部署。不幸的是，编程技术仍处于初级阶段，构建系统需要理论密码学和编译器方面的大量专业知识。这个项目的目标是将编程技术提高到这样一个水平，即来自不同域的程序员可以编写安全高效的算法，而不需要掌握广泛的密码原语知识。这个项目关注于一种新的MPC中间表示(IR)，并提出了后端无关优化的思想，这与经典编译器中的机器无关优化非常相似。它构建了一个编译器框架，该框架采用类似Python的程序并生成低级加密代码。该项目的第一个主旨是在内部关系上进行程序内优化。它建立了新的SIMD矢量化、分而治之、调度、协议混合和其他优化，将经典分析扩展到MPC的独特设置和约束，以及开发新的MPC特定成本模型和优化(例如，协议混合)。关键的前提是，IR的线性结构高度服从程序分析、准确的成本建模和程序综合，因此这些技术可以产生积极的和可证明是最优的转换。第二个推力为证明IR上变换的正确性奠定了理论基础。第三个推力将程序内推理扩展到程序间环境。除了在技术上的贡献外，该项目还将促进本科生和研究生的教育。它将在安全计算、编译器和系统构建方面培训新一代计算机科学家。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Building secure (privacy-preserving) systems is a problem of great importance in the day and age of big data analytics and machine learning. Algorithms aggregate data and build predictive models that become more accurate as they aggregate data from many different parties. Such large-scale aggregation raises security and privacy concerns. Secure Multi-Party Computation (MPC) is an approach that allows two or more parties to perform a computation on their private data without revealing information about their data. Long in the realm of theoretical cryptography, MPC has seen advances in programming technology. It has been deployed in practice in scenarios such as sealed auctions, benchmarking company performance, privacy-preserving machine learning, and biometric matching. Unfortunately, programming technology is still nascent and building systems requires significant expertise in theoretical cryptography, as well as compilers. The goal of this project is to bring programming technology to a level where programmers from different domains can write secure and efficient algorithms without commanding extensive knowledge of cryptographic primitives. This project focuses on a new intermediate representation (IR) for MPC and advances the idea of backend-independent optimization, in a close analogy to machine-independent optimization in the classical compiler. It builds a compiler framework that takes a Python-like program and produces low-level cryptographic code. The first thrust of the project develops intra-procedural optimizations over the IR. It builds novel SIMD-vectorization, divide-and-conquer, scheduling, protocol mixing and other optimizations, extending classical analyses to the unique setting and constraints of MPC, as well as developing new MPC-specific cost models and optimizations (e.g., protocol mixing). The key premise is that the linear structure of the IR is highly amenable to program analysis, accurate cost modeling, and program synthesis and therefore these techniques can give rise to aggressive and provably optimal transformations. The second thrust builds a theoretical foundation for proving correctness of transformations over the IR. The third thrust extends intra-procedural reasoning to the inter-procedural setting. In addition to its technical contribution, the project will contribute to the education of students at both the undergraduate and graduate levels. It will train a new generation of computer scientists in secure computation, compilers, and system building.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.