Paper-Conference

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.

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