Developing secure distributed systems adds new challenges not seen in ordinary programming paradigms due to the presence of multiple mutually distrusting domains. Program partitioning is a promising option for navigating this added complexity: instead of writing the distributed program directly, the programmer writes a single program intended to run on a hypothetical, trusted host. This program is then automatically compiled to a distributed version employing cryptographic mechanisms to ensure security.

Viaduct is a recent implementation of program partitioning featuring an expressive security typed language and an extensible, wide range of cryptographic mechanisms, including reactive multiparty computations and noninteractive zero-knowledge proofs. Unfortunately, Viaduct does not currently come with a formal proof of security.

To give formal guarantees to Viaduct, we propose using a variant of Universal Composability (UC) as a security condition. Using UC allows us to formally connect our model of program partitioning with the security of underlying cryptographic mechanisms. UC security implies robust hyperproperty preservation, a strong criterion for compiler correctness.