VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating Above FF-A

Explore a groundbreaking presentation from PLDI 2023 that introduces VMSL, a novel separation logic for mechanized robust safety of virtual machines communicating above FF-A. Delve into the challenges of isolating key security components from vulnerable operating systems using thin hypervisors. Examine the delicate balance between expressivity, performance, and security in hypercall ABI design. Learn how the researchers formalized a substantial fragment of Arm's FF-A as a machine with a simplified ISA and developed VMSL to reason modularly about communicating virtual machines. Discover how this logic proves robust safety, ensuring compromised VMs cannot break safety properties of other VMs running known code. Gain insights into the Coq formalization using the Iris framework and explore the implications for hypervisor design and security.