Towards formally secure compilation of verified F* programs against unverified ML(…)
summary
Framework written and verified in F compiles terminating higher-order IO F programs to a deeply embedded ML-like language with an end-to-end mechanized proof; it replaces F’s unverified extraction and proves robust relational hyperproperty preservation (stronger than full abstraction) via a cross-language logical relation. Key technique is relational quotation: a typing relation that records typing derivations (used to project syntax) plus a small meta program (typeclass-based) to find derivations, so no formal meta-theory of F is required. Prototype handles callbacks and IO traces; nontermination and full OCaml extraction remain future work.
AI-written summary · about
chapters (7)
- 0:00Verified F* compilation intro
- 1:27What is F*
- 3:35Secure compilation challenges
- 6:52Relational quotation technique
- 11:31End-to-end proof guarantees
- 12:57Recap and future work
- 13:21Q&A
related talks
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
01h 05mAll the Languages Together
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
21mVerified Extraction from Coq to OCaml
50mA Type-Theoretic Framework for Certified Meta-programming
01h 06mVerifying a compiler through equational means
18mA Verified Compiler for a Functional Tensor Language
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...