Towards Modular Specification and Verification of Concurrent Hypervisor-based I...
summary
NOVA is a microhypervisor of 17K lines and 15 hypercalls whose specification (~100 pages) is decomposed with Iris-based separation logic into WP_Nova_EC and per-hypercall WP specs. The team verifies C++ implementations for semaphore up/down and a user-space synchronization library, models ownership transfer for a master controller, and is finishing a verified vSwitch and UMX console multiplexer; robust safety is proven as a safety property only, and full revocation proofs remain open.
AI-written summary · about
chapters (10)
- 0:00Introduction Nova overview
- 1:25Nova kernel interface
- 3:10Verification goals
- 4:12Semaphores in Nova
- 6:40Weakest precondition user threads
- 8:48Bootstrapping with Carousel
- 10:57Robust safety against user space
- 12:45Hybrid clients verified/unverified
- 15:13System verifications libraries
- 16:16Q&A
related talks
11mSpecifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
28mLightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
17mVeriSMo: A Verified Security Module for Confidential VMs
23mApplying Formal Verification to Microkernel IPC at Meta
18mVMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…)
23mHyper-V's Virtual Secure Mode in KVM project update
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
44mModular Approach to Cloud Security