Formal Verification of Interrupt Injection in a Hypervisor

Operating systems usually rely on external interrupts as notifications of various events, such as the completion of a DMA transfer and the coming of a time point. The loss of external interrupts may affect the correct execution of operating systems. In the virtualization environment, some interrupts accepted by the virtual CPU are injected by the hypervisor. The hypervisor is responsible to implement a reliable interrupt injection mechanism so as to avoid losing external interrupts in the virtual machine. In this paper, we apply the formal method to verify the interrupt injection implementation in a research hypervisor. First, we formally define a machine model with a more realistic x86 interrupt model than others used in the existing work. Our interrupt model defines the semantics of the interrupt shadow which has never been modeled before. It also defines the semantics of the interrupt injection mechanism provided by the x86 CPU virtualization extensions, such as Intel VMX and AMD SVM. Second, we formally define the safety property and reliability property of the interrupt injection mechanism on this interrupt model. Finally, we take the interrupt injection code in a research hypervisor as an example and verify that it satisfies above two properties.