SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn
summary
Proposes a concrete back-translation that emits data-flow traces (register moves, loads, stores) so stashing pointers no longer requires traversing the shared-memory graph, and mechanizes the construction and correctness proof in Coq. Introduces a turn-taking simulation relation and a mechanized recomposition lemma that reuses whole-program compiler-correctness. Works for a structured-source vs unstructured-target pair with shared memory; the implementation proof succeeds and replaces prior ad-hoc pointer-stashing work.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:22General Setup
- 0:53Partial Program Example
- 3:50BackTranslation
- 8:16Example
- 11:00Problem
- 12:28DataFlow Events
- 13:13BackTranslation Example
- 15:33Summary
- 15:57Technical Details
- 16:20Why do we want to reuse wholeprogram correctness limits
- 17:01Questions
- 18:02Online Questions
- 21:10Wrapup
related talks
28mMemory simulations, security and optimization in a verified compiler
25mSecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
31mBlame-Preserving Secure Compilation
15mMy Journey in Secure Compilation
08mShort Talk: Generalising secure compilation criteria
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
20mFully Composable and Adequate Verified Compilation with Direct Refinements betwe...
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...