A Semantic Approach to Robust Property Preservation
summary
Proposes a semantic reduction of robust property preservation: replace hard syntactic backtranslation with a backtranslation between semantic domains, so compiler correctness is the only syntax-heavy proof and the main security argument runs entirely in the semantic domain. Uses the DimSum multi-language semantics, a Rock theorem prover formalization and Iris separation logic site conditions to define a target universal contract and a source-level simulator; universal contract, simulator and program logic are mechanized and several example programs verify, while semantic backtranslation and full compiler correctness remain in progress.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:04Motivation for secure compilation
- 2:52Problems with existing approaches
- 7:49Semantic approach to challenges
- 9:39Proof outline
- 11:27Formalization in Rock
- 15:43Compiler verification Rack vs Cap
- 17:50Summary
- 18:53Q&A
related talks
26mEndangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…)
08mShort Talk: Generalising secure compilation criteria
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
40mFormal semantics for multi-language programs
29mSemantic Transformation Framework for Rewriting Rules
25mComposing Secure Compilers
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
20mRelaxed systems semantics and how we (hope to) reason above it