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

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.