Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
summary
Secure compilation chain for an F subset with IO converts static specs into runtime checks and adds a linking-time reference monitor that blocks forbidden system calls (example: prevents any open("ethical_password") from context code). Implemented and machine-checked in F via shallow embeddings and an indexed IO monad with getTrace; uses flag polymorphism to isolate implementations and enable a back-translation. Proves soundness and Robust Relational Hyperproperty Preservation by syntactic-equality style proofs; toolchain and proofs succeed.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:06Naive compilation problems
- 3:36Running example and interface weakening
- 5:21Dynamic result constraints
- 8:36Interface strengthening via imports/exports
- 10:23Reference monitor for IO enforcement
- 11:49Formalizing in F* and Fλ
- 13:14Modeling IO with trace properties
- 15:26Linking via instrumentation
- 16:54Soundness proof
- 18:00Hyper property preservation
- 19:47Syntactic equality in back translation
- 20:08Summary
related talks
21mSecuring Verified IO Programs Against Unverified Code in F*
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
25mSecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
01h 05mAll the Languages Together
19mVerifying non-terminating programs with IO in F*
17mOvercoming Restraint: Composing Verification of Foreign Functions with Cogent
38mBuilding Secure Systems in Haskell
01h 02mPolyglot Programming through Foreign Function Interfaces