Verifying the Microsoft Hyper-V hypervisor with VCC

Dirk Leinenbach, Thomas Santen
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 06 October 2019

International Symposium on Formal Methods
Springer
Pages 806-809
2009
Note(s): hypervisor, Operating Systems, information flow, VCC verifier

This short (3.5 page) paper gives a brief overview of Hyper-V verification. Hyper-V is a high performance commercial hypervisor not written with verification in mind. It is 100kloc of C plus 5kloc x86-64 assembly, uses lock free data structures, simulates 2-stage page translation. Verification makes heavy use of “two-state invariants” and “claims”. Useful as an overview but need to read other papers to get any detail.

  • Boogie: A modular reusable verifier for object-oriented programs [barnett:fmco:2005]