Porcupine: A Synthesizing Compiler for Vectorized Homomorphic Encryption

TL;DR

Porcupine is an optimizing compiler that uses program synthesis to automatically generate efficient, verified homomorphic encryption kernels, overcoming compilation challenges and achieving significant speedups over hand-optimized code.

Contribution

It introduces Porcupine, a novel compiler framework that automates HE kernel generation through program synthesis, addressing key HE-specific challenges.

Findings

Achieves up to 51% speedup over hand-optimized kernels

Synthesized solutions often differ from intuitive approaches

Proves the effectiveness of automated reasoning in HE kernel optimization

Abstract

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, and HE DSL named Quill to automatically generate 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. Quill captures the underlying HE operator behavior that enables Porcupine to reason about the complex trade-offs imposed by the challenges and generate optimized, verified HE kernels. To improve synthesis time, we propose a series of optimizations including a sketch design tailored to HE and instruction restriction to narrow the program search space. We evaluate Procupine using a set of kernels and show speedups of up to 51% (11% 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.