Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption
Sat 26 Jun 2021 01:50 - 01:55 at PLDI-B - Talks 6B: Applied Logics and Semantics
Homomorphic encryption (HE) is a privacy-preserving technique that enables computation directly on encrypted data. Despite its promise, HE has seen limited use due to performance overheads and compilation challenges. Recent work has made significant advances to address the performance overheads but automatic compilation of efficient HE kernels remains relatively unexplored.
This paper presents Porcupine, an optimizing compiler that generates vectorized HE code using program synthesis. HE poses three major compilation challenges: it only supports a limited set of SIMD-like operators, it uses long-vector operands, and decryption can fail if ciphertext noise growth is not managed properly. Porcupine captures the underlying HE operator behavior so that it can automatically reason about the complex trade-offs imposed by these challenges to generate optimized, verified HE kernels. To improve synthesis time, we propose a series of optimizations including a sketch design tailored to HE to narrow the program search space. We evaluate Porcupine using a set of kernels and show speedups of up to 52% (25% geometric mean) compared to heuristic-driven hand-optimized kernels. Analysis of Porcupine's synthesized code reveals that optimal solutions are not always intuitive, underscoring the utility of automated reasoning in this domain.
Fri 25 JunDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:00 | |||
13:30 5mTalk | Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic PLDI Simon Spies MPI-SWS, Lennard Gäher Saarland University, Daniel Gratzer Aarhus University, Joseph Tassarotti Boston College, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Lars Birkedal Aarhus University DOI | ||
13:35 5mTalk | Example-Guided Synthesis of Relational Queries PLDI Aalok Thakkar University of Pennsylvania, Aaditya Naik University of Pennsylvania, Nathaniel Sands University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California DOI | ||
13:40 5mTalk | CompCertO: Compiling Certified Open C Components PLDI DOI | ||
13:45 5mTalk | On Probabilistic Termination of Functional Programs with Continuous Distributions PLDI DOI | ||
13:50 5mTalk | Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption PLDI Meghan Cowan Facebook Reality Labs Research, Deeksha Dangwal Facebook Reality Labs Research, Armin Alaghi Facebook Reality Labs Research, Caroline Trippel Stanford University, Vincent T. Lee Facebook Reality Labs Research, Brandon Reagen New York University DOI | ||
13:55 5mTalk | Polynomial Reachability Witnesses via Stellensätze PLDI Ali Asadi Sharif University of Technology, Krishnendu Chatterjee IST Austria, Hongfei Fu Shanghai Jiao Tong University, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Mohammad Mahdavi Sharif University of Technology DOI |
Sat 26 JunDisplayed time zone: Eastern Time (US & Canada) change
01:30 - 02:00 | |||
01:30 5mTalk | Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic PLDI Simon Spies MPI-SWS, Lennard Gäher Saarland University, Daniel Gratzer Aarhus University, Joseph Tassarotti Boston College, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Lars Birkedal Aarhus University DOI | ||
01:35 5mTalk | Example-Guided Synthesis of Relational Queries PLDI Aalok Thakkar University of Pennsylvania, Aaditya Naik University of Pennsylvania, Nathaniel Sands University of Southern California, Rajeev Alur University of Pennsylvania, Mayur Naik University of Pennsylvania, Mukund Raghothaman University of Southern California DOI | ||
01:40 5mTalk | CompCertO: Compiling Certified Open C Components PLDI DOI | ||
01:45 5mTalk | On Probabilistic Termination of Functional Programs with Continuous Distributions PLDI DOI | ||
01:50 5mTalk | Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption PLDI Meghan Cowan Facebook Reality Labs Research, Deeksha Dangwal Facebook Reality Labs Research, Armin Alaghi Facebook Reality Labs Research, Caroline Trippel Stanford University, Vincent T. Lee Facebook Reality Labs Research, Brandon Reagen New York University DOI | ||
01:55 5mTalk | Polynomial Reachability Witnesses via Stellensätze PLDI Ali Asadi Sharif University of Technology, Krishnendu Chatterjee IST Austria, Hongfei Fu Shanghai Jiao Tong University, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Mohammad Mahdavi Sharif University of Technology DOI |