VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating(…)
summary
Formalises a substantial fragment of Arm FF‑A as a toy ISA with hypercalls and develops VMSL separation logic to reason about VM-to-VM shared pages and handoff protocols, proving robust safety so unknown VMs cannot gain ownership of unrelated pages. Mechanisation uses Coq on Iris, verifies examples like a ping‑pong yield protocol and a page‑share where a reader observes 42, and proves two compatible logical relations for primary and secondary VMs. Artifacts and proofs are available.
AI-written summary · about
chapters (12)
- 0:00VMSL introduction
- 1:27Hypervisor isolation challenges
- 2:31Memory management
- 3:59Separation logic for VMs
- 5:04FFA semantics and VMSL design
- 6:27VM modular reasoning with FFA
- 8:57Memory sharing correctness
- 10:23Robust safety for unknown VMs
- 11:25Unary type logic relations
- 12:49Logical relations compatibility
- 13:10Conclusion and results
- 13:33Q&A
related talks
01h 05mKeynote: Can we reason about the security of concurrent systems code?
14mSecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
17mVeriSMo: A Verified Security Module for Confidential VMs
21mIris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe(…)
11mSpecifying and Verifying the NOVA Microhypervisor in Concurrent Separation Logic
20mFSLH: Flexible Mechanized Speculative Load Hardening
28mProving Memory Access Violations in Isabelle/HOL
47mLinux Virtualization Based Security