Applying Formal Verification to Microkernel IPC at Meta
summary
Project uses Iris in Coq to verify the microkernel IPC algorithms (not the full C), proving correctness of two queues verified implemented as non‑blocking, two‑phase ring buffers. Proof work finishes in a few person‑months and uncovers four simplifications: removal of two memory barriers, one atomic load, and one boolean check, plus device‑driver fixes for uninitialized memory. Verification targets a sequential model, increases confidence, and yields concrete performance and correctness fixes rather than vague examples.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:02The XROS Operating System
- 2:06Motivation
- 2:55Strategy
- 3:49Algorithm vs Code
- 4:37Results
- 5:37Separation Logic
- 6:26Hoare Logic - Concurrent Programming
- 6:46Invariants
- 7:27Specifying Concurrent Data Structures
- 8:20The XROS Generic Queue
- 9:31The Code
- 10:53The Endless Ribbon
- 11:27The Ribbon State
- 12:08Queue Invariant
- 14:02Conclusion
- 19:39Proof Sketch - Logical States
related talks
19mOpen-Source Commercial-Grade RISC-V IOMMU with Verification
11mSpecifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
01h 05mKeynote: Can we reason about the security of concurrent systems code?
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
21mSecuring Verified IO Programs Against Unverified Code in F*
12mAutomated Synthesis of Verified Firewalls
26mThe Supervisionary proof-checking kernel, or: a work-in-progress toward proof-g