We prove the end-to-end correctness of a compiler that synthesizes cryptographic protocols from high-level programs. The proof is based on the Universal Composability framework.

I describe Viaduct, a compiler that transforms high-level programs into secure, efficient distributed realizations that use cryptography. I develop a modular security proof for Viaduct that abstracts away from the details of cryptographic mechanisms.

We introduce AIRduct, a new array-based intermediate representation designed to support generating efficient code for interactive programs employing multiple cryptographic mechanisms. AIRduct is intended as an IR for the Viaduct compiler, which can synthesize secure, distributed programs with an extensible suite of cryptography. Therefore, AIRduct supports an extensible variety of cryptographic mechanisms, including MPC and ZKP.

We present Viaduct, a compiler that transforms high-level programs into efficient distributed realizations that use cryptography to preserve security.

We extend the deep logical connection between linear sequent calculus and session-typed concurrency with intersection and union types to express multiple behavioral properties of processes.