"Your Secrets are Safe with Julia: A Compiler for Secure Computation" by Jason Dagit

### Overview In this talk presented at Strange Loop, Jason Dagit discusses an IARPA-funded proof-of-concept project conducted at Galois to address the usability challenges of secure computation, specifically homomorphic encryption (HE). While homomorphic encryption enables computation directly on encrypted data without decrypting it, it faces two primary hurdles: massive performance overhead (5 to 10 orders of magnitude slower than native CPU execution) and significant programming difficulty, as computations must ultimately be expressed as arithmetic circuits (integer polynomials). Dagit and his team focused on the usability problem by building a compilation toolchain allowing programmers to write standard Julia code and automatically compiling it into arithmetic circuits evaluated via an HE backend.

### Key Topics - **Homomorphic Encryption Basics**: The structure of HE evaluated over integer rings supporting associative, commutative addition and commutative multiplication, but lacking general division, dynamic control flow, and persistent memory. - **Symbolic Execution with Crucible**: Using Galois' open-source symbolic evaluation framework, Crucible (written in Haskell), to interpret and unroll high-level Julia programs into arithmetic circuits and polynomial expressions. - **Integration with Palisade**: Utilizing Palisade, a lattice cryptography library developed by Kurt Roloff and his team at the New Jersey Institute of Technology, to execute arithmetic circuits over encrypted data. - **Data Flattening and Metadata**: Managing dynamic structures such as matrices by enforcing concrete dimensions while allowing symbolic elements, flattening structures into integer arrays, and generating Julia metadata functions to reshape decrypted output.

### Technical Details The toolchain workflow begins with standard Julia code (such as an image-sharpening algorithm or linear regression). By using Julia’s reflection capabilities, the system lowers the abstract syntax tree (AST) into an S-expression representation without needing a custom parser. This AST is handed to Crucible, which symbolically evaluates the program with designated symbolic inputs and concrete dimensions (e.g., fully unrolling loops and eliminating side effects like dead error paths). Crucible outputs an arithmetic circuit along with Julia metadata functions designed to rebuild structured data types from flat integer lists. The data is encrypted using Palisade, evaluated homomorphically through Palisade's circuit interpreter, and the resulting ciphertext is returned to Julia for decryption and reshaping. Dagit also noted specific technical limitations and discoveries: division was restricted to power-of-two right shifts as the final operation on a ciphertext; large circuits required streaming out of Crucible to prevent Haskell heap exhaustion; and loops with symbolic bounds (like Euclid's GCD) cannot be easily bounded. Furthermore, the functional specifications derived via symbolic execution enabled equivalence verification between algorithms (such as naive determinant vs. Richard Bird's integer-only determinant) using SMT/SAT solvers.

### Takeaways The project demonstrated that symbolic execution is an effective bridge between high-level dynamic programming languages and the rigid, polynomial representations required by homomorphic encryption backends. While this proof of concept specifically targeted usability rather than the underlying cryptographic performance penalties, it highlighted how formal methods, symbolic evaluation, and solver-based equivalence checking can make privacy-preserving computation accessible to domain scientists.