Securing Verified IO Programs Against Unverified Code in F*
summary
A verified secure compilation pipeline for F programs that perform IO, called SCIO, compiles verified code to a smaller F target and enforces assumptions at the boundary by inserting higher-order contracts and by linking an adversarial context to a reference monitor that records past IO and enforces an access control policy. The whole design is mechanized in F* and proves sound enforcement of a global trace safety property and Robust Relational Hyperproperty Preservation, and is demonstrated on a verified web server with reusable artifacts.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:22Secure compilation framework
- 2:08Unverified code problem
- 3:55Higher-order contracts
- 4:59Reference monitor
- 6:24Scio* for IO programs
- 7:26Key contributions
- 8:28Verifying IO programs in F*
- 11:42Type translation
- 14:13Secure compilation proof
- 15:38Verified web server case study
- 16:05Q&A
related talks
21mSecurely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typ...
25mSecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
19mVerifying non-terminating programs with IO in F*
15mMy Journey in Secure Compilation
12mAutomated Synthesis of Verified Firewalls
34mFormally verified hardening of C programs against hardware fault injection
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
38mBuilding Secure Systems in Haskell