Specifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
summary
Verification of the NOVA microhypervisor uses BRiCk C++ program logic built on Iris and Skylabs proof automation to prove concurrency properties of about 15,000 lines of unchanged C++ code; architecture-independent, highly concurrent components are the focus. The project formalizes NOVA APIs (e.g. fair semaphores) as Iris-based atomic updates, verifies many functions end-to-end (many components marked green), and runs automated symbolic evaluation via Skylabs automation while leaving low-level assembly outside the current TCB.
AI-written summary · about
chapters (6)
- 0:00Verifying NOVA microhypervisor
- 1:03Microkernel hypervisor overview
- 2:30Separation logic verification
- 4:18Spike-driven verification
- 6:04Verification results and open source
- 9:36Q&A
related talks
24mTowards Modular Specification and Verification of Concurrent Hypervisor-based I...
01h 05mKeynote: Can we reason about the security of concurrent systems code?
23mApplying Formal Verification to Microkernel IPC at Meta
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
18mVMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…)
17mVeriSMo: A Verified Security Module for Confidential VMs
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
28mProving Memory Access Violations in Isabelle/HOL