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

在大数据分析和机器学习时代，构建安全（隐私保护）系统是一个非常重要的问题。算法聚合数据并构建预测模型，这些模型在聚合来自许多不同方的数据时变得更加准确。这种大规模的聚合引发了安全和隐私方面的担忧。安全多方计算（MPC）是一种允许两方或多方在不泄露有关其数据的信息的情况下对其私有数据执行计算的方法。MPC在理论密码学领域有很长的时间，在编程技术方面取得了进展。它已在实际应用中部署在密封拍卖、基准公司绩效、隐私保护机器学习和生物识别匹配等场景中。不幸的是，编程技术仍然处于萌芽状态，构建系统需要理论密码学和编译器方面的大量专业知识。该项目的目标是将编程技术提高到一个水平，使来自不同领域的程序员可以编写安全有效的算法，而无需掌握大量的密码原语知识。这个项目的重点是一个新的中间表示（IR）MPC和先进的后端独立优化的想法，在一个密切的类比，在经典的编译器中的机器独立优化。它构建了一个编译器框架，该框架接受类似Python的程序并生成低级加密代码。该项目的第一个重点是开发IR上的过程内优化。它构建了新颖的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.