Fully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
summary
Shows that a fully abstract compiler only robustly preserves a precisely characterized set of hyperproperties which can be trivial or meaningless in some cases, gives an explicit example of a fully abstract compiler that fails to preserve non‑interference, and then fixes it by adding a back‑translation requirement on the compiler’s syntax and behavior maps. Proposes a MOS‑based criterion that ensures both robust compilation and full abstraction, provides categorical definitions and proofs, and reports an ongoing Agda mechanization.
AI-written summary · about
chapters (9)
- 0:00Intro
- 0:22SECURE COMPILERS
- 0:53FULLY ABSTRACT COMPILATION
- 2:40ROBUST COMPILATION
- 4:15GUARANTEES ON COMPILED PROGRAMS
- 5:43CAN WE HAVE BOTH?
- 7:02A CATEGORICAL APPROACH
- 9:12OUR CRITERION
- 10:09CONCLUSIONS
related talks
25mComposing Secure Compilers
22mThe Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How t
08mShort Talk: Generalising secure compilation criteria
25mA Semantic Approach to Robust Property Preservation
22mComputational-Bounded Robust Compilation and Universally Composable Security
25mUniversal Composability is Secure Compilation
23mUniversal Composability is Robust Compilation
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends