Universally Composable Security for Program Partitioning
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.
Sat 21 JanDisplayed time zone: Eastern Time (US & Canada) change
16:00 - 17:30
|Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers|
Michael Smith UC San Diego, Abhishek Sharma UC San Diego, John Renner University of California at San Diego, USA, David Thien UC San Diego, Sorin Lerner University of California at San Diego, Fraser Brown CMU, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San DiegoFile Attached
|FaJITa: Verifying Optimizations on Just-In-Time Programs|
David Thien UC San Diego, Michael Smith UC San Diego, Evan Johnson University of California at San Diego; Arm, Sorin Lerner University of California at San Diego, Hovav Shacham University of Texas at Austin, Deian Stefan University of California at San Diego, Fraser Brown CMUPre-print File Attached
|Universally Composable Security for Program Partitioning|
Coşku Acay Cornell University, Joshua Gancher Carnegie Mellon University, Rolph Recto Cornell University, Andrew Myers Cornell UniversityFile Attached