Theory of Multi Core Hypervisor Verification

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