Modularizing CPU Semantics for Virtualization

Explore a 25-minute conference talk from ACM SIGPLAN's PriSC'24 that delves into the modularization of CPU semantics for virtualization. Learn how researchers Paolo G. Giarrusso, Abhishek Anand, Gregory Malecha, František Farka, and Hoang-Hai Dang propose a novel approach to simplify the verification of virtual machine monitors (VMMs) using hardware-assisted virtualization. Discover their method for modularizing hardware semantics to efficiently capture the differences between bare-metal and hardware-virtualized processor behavior. Gain insights into how this modularization technique can streamline the verification process for VMMs, addressing the challenges of case analysis in modern architectures and separating ISA architect responsibilities from VMM implementer tasks.

[PriSC'24] Modularizing CPU Semantics for Virtualization