Modern computer systems consist of a multitude of abstraction layers (e.g., OS kernels, hypervisors, device drivers, network protocols), each of which defines an interface that hides the implementation details of a particular set of functionality. Client programs built on top of each layer can be understood solely based on the interface, independent of the layer implementation. Despite their obvious importance, abstraction layers have mostly been treated as a system concept; they have almost never been formally specified or verified. This makes it difficult to establish strong correctness properties, and to scale program verification across multiple layers.

Kernel preemption is an important feature among mainstream OS kernels. It allows that a kernel thread can be preempted by another kernel thread by performing context switch. A kernel thread can access shared data by disabling kernel preemption temporarily without turning off interruption. Kernel preemption and preemption control reduce kernel response time, but at the same time make kernels more difficult to develop or verify. It is difficult to define their clear semantics and reason about preemptive kernel code. In this paper, we propose a verification framework to verify preemptive kernel code with kernel preemption control. In the framework, we cannot only verify the implementation of preemption control, but also verify the preemptive kernel code which may turn-on/off kernel preemption. The basic idea of the framework is that we build an intermediate abstract layer, where kernel threads, preemption status and interrupt context are made into abstract resources such that we can easily specify the global invariant of the kernel and reason about code with the help of abstract knowledge.

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.