Viaduct

We develop an algebraic framework for information flow control labels that expresses asymmetric delegation: partial delegation of confidentiality or integrity. Safety is ensured via nonmalleable information flow, which we implement as a static checker together with a label inference procedure supporting bounded label polymorphism.

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 …

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