Universal Composability is Secure Compilation
summary
Claims a correspondence between universal composability and a robust compilation criterion: UC ↔ RHC equivalence. Argues that for every target attacker a source context reproduces the same traces (robust hyperproperty preservation), and proposes formalizing protocols and ideal functionalities in the interactive lambda calculus (the Saucy/IRC style) to mechanize UC proofs. Covers full compilation pipelines including linkers and multi-stage compilers and plans a trace-preserving back-translation to show source-level simulators exist.
AI-written summary · about
chapters (15)
- 0:00Universal Composability is Secure Compilation
- 1:31Universal Composability: UC
- 3:08UC Base Notions: ITMs
- 5:39UC (Semi-formally)
- 8:38UC Beneifts: Compositionality
- 10:08Secure Compilation: SC
- 11:57Robust Criteria for SC
- 12:34Robust Hyperproperty Preservation: RHC
- 13:42A Closer Look
- 14:36Analogy
- 16:01Benefits
- 17:27UC Roadmap
- 18:05SC Roadmap
- 19:41But Fully Abstract Compilation...
- 21:48Questions?
related talks
23mUniversal Composability is Robust Compilation
22mComputational-Bounded Robust Compilation and Universally Composable Security
27mUniversally Composable Security for Program Partitioning
25mComposing Secure Compilers
08mShort Talk: Generalising secure compilation criteria
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
15mMy Journey in Secure Compilation