Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
Fri 25 Jun 2021 13:50 - 13:55 at PLDI-B - Talks 6B: Applied Logics and Semantics
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 Jun

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:00
Talks 6B: Applied Logics and SemanticsPLDI at PLDI-B +12h
13:30
5m
Talk
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
5m
Talk
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
5m
Talk
CompCertO: Compiling Certified Open C Components
PLDI
Jérémie Koenig Yale University, Zhong Shao Yale University
DOI
13:45
5m
Talk
On Probabilistic Termination of Functional Programs with Continuous Distributions
PLDI
Raven Beutner University of Oxford, C.-H. Luke Ong University of Oxford
DOI
13:50
5m
Talk
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
5m
Talk
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 Jun

Displayed time zone: Eastern Time (US & Canada) change

01:30 - 02:00
Talks 6B: Applied Logics and SemanticsPLDI at PLDI-B
01:30
5m
Talk
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
5m
Talk
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
5m
Talk
CompCertO: Compiling Certified Open C Components
PLDI
Jérémie Koenig Yale University, Zhong Shao Yale University
DOI
01:45
5m
Talk
On Probabilistic Termination of Functional Programs with Continuous Distributions
PLDI
Raven Beutner University of Oxford, C.-H. Luke Ong University of Oxford
DOI
01:50
5m
Talk
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
5m
Talk
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