SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
summary
SecRef is a secure-compilation framework for F that enforces verified programs’ assumptions about dynamically shared ML-style mutable references by inserting higher-order contracts and tracking shareability with a ghost label system built on F’s monotonic state. The authors mechanize proofs in F showing robust relational hyperproperty preservation (observational equivalence, non-inference, trace properties), extract a compiler that inserts runtime checks, and demonstrate the approach with a verified cooperative multithreading scheduler; artifacts are available.
AI-written summary · about
chapters (12)
- 0:00SecRef* and F* introduction
- 1:22Mixing verified and unverified code
- 2:26Stateful programs and shared references
- 3:53Enforcing assumptions with checks
- 5:38SecRef* contributions overview
- 6:00Unverified library example
- 8:32Tracking references with labels
- 12:26Unverified code assumptions
- 15:37Weak and intermediate types
- 17:47Why SecRef* is secure
- 19:34Case study and contributions
- 20:18Q&A on performance
related talks
21mSecuring Verified IO Programs Against Unverified Code in F*
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
26mSecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
15mMy Journey in Secure Compilation
20mFSLH: Flexible Mechanized Speculative Load Hardening
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
22mQuest Complete: The Holy Grail of Gradual Security