Universally Composable Security for Program Partitioning
summary
An implemented compiler called Viaduct compiler takes a single-threaded program with tuple information-flow labels (confidentiality, integrity) and automatically partitions it to concrete hosts or idealized cryptographic boxes, generating calls to real backends like MPC via ABY, libsnark zero-knowledge proofs and commitment libraries. The claim is a two-step UC-style proof: partitioning (source → hybrid) then cryptographic instantiation (hybrid → real) using label-transition simulations; this proof strategy yields UC implies robust hyperproperty preservation, so verified security composes with existing crypto proofs.
AI-written summary · about
chapters (14)
- 0:00Start
- 0:55Viaduct: Let the Compiler Worry About Cryptography
- 2:01Data Labels
- 6:40Cryptographic Instantiation
- 7:04Implementation
- 7:26What is Correctness?
- 7:58Proof Requirements
- 8:39Universal Composability (UC) Simulation
- 9:40Real World Attacker
- 11:25Two-step Proof
- 12:53Step 1: Correctness of Partitioning
- 14:47Step 2: Instantiating Functionalities
- 18:02Conclusion
- 19:06Proof Outline
related talks
23mUniversal Composability is Robust Compilation
25mUniversal Composability is Secure Compilation
22mComputational-Bounded Robust Compilation and Universally Composable Security
25mComposing Secure Compilers
44mModular Approach to Cloud Security
33mInteraction Preserving Compilers for Secure Computation
51mDistributed Zero-Knowledge Proofs and Applications to Secure Computation
15mMy Journey in Secure Compilation