From 2007 to 2010, researchers from Microsoft and the Verisoft XT project verified code from Hyper-Ⅴ, a multi-core x-64 hypervisor, using VCC, a verifier for concurrent C code. However, there is a significant gap between code verification of a kernel (such as a hypervisor) and a proof of correctness of a real system running the code. When the project ended in 2010, crucial and tricky portions of the hypervisor product were formally verified, but one was far from having an overall theory of multi core hypervisor correctness even on paper. For example, the kernel code itself has to set up low-level facilities such as its call stack and virtual memory map, and must continue to use memory in a way that justifies the memory model assumed by the compiler and verifier, even though these assumptions are not directly guaranteed by the hardware. Over the last two years, much of the needed theory justifying the approach has been worked out. We survey progress on this theory and identify the work that is left to be done.
展开▼
