Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet
Hypervisors are an essential part of our computing infrastructure, yet ensuring their correctness remains a significant challenge for the community. While several hypervisors have been formally verified using traditional methods, they have typically required a huge effort and significant input from verification experts. With the increasing diversity of hypervisors, driven by open hardware and custom ISAs, there is a growing need for more accessible approaches that can be used by non-experts.
Authors
- Nate Foster (ORCID: https://orcid.org/0000-0002-6557-684X)
- Thomas Bourgeat (ORCID: https://orcid.org/0000-0002-8468-8409)
- Charly Castes (ORCID: https://orcid.org/0009-0008-7021-158X)
- Edouard Bugnion (ORCID: https://orcid.org/0000-0001-7237-6929)
- François Costa
Institutions
- Cornell University (US)
- The Jane Goodall Institute (US)
- ETH Zurich (CH)
- Jane Street (United States)
- École Polytechnique Fédérale de Lausanne (CH)
Publication Details
- Published
- 2025-05-14
- DOI
- https://doi.org/10.1145/3713082.3730373
- Primary Topic
- Security and Verification in Computing
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- VMware
- École Polytechnique Fédérale de Lausanne
- Defense Advanced Research Projects Agency
- Office of Naval Research