Verification of a Generative Separation Kernel

Abstract

A Separation Kernel is a small specialized microkernel that provides a sand-boxed execution environment for a given set of processes (also called \subjects"). The subjects may communicate only via declared memory channels, and are otherwise isolated from each other. A generative separation kernel is one in which a specialized separation kernel is generated for each system con figuration. Separation kernels are typically used in safety-critical and security-critical systems in the avionics and military domains, and it is of utmost importance to have a high level of assurance regarding the correct working of the separation kernel. In this thesis we present a formal veri fication of the functional correctness of the Muen separation kernel which is representative of the class of modern separation kernels that leverage hardware virtualization support and are generative in nature. The nature of generativeness is template-based, in that the kernel is essentially based on a fixed template of code and various constant data-structures are filled-in by the kernel generator. Although there is a great deal of work in verifi cation of OS kernels in the past two decades, applying those techniques to a separation kernel like Muen becomes challenging because of its generative nature. The use of hardware virtualization support poses another challenge. We propose a veri fication framework called conditional parametric re finement to reason about the functional correctness of template-based generative systems. Conditional parametric re finement extends classical re finement to parametric programs which are programs with uninitialized variables. This is a two-step technique for parametric programs. We first perform a general verifi cation step (independent of the input spec) to verify that the parametric program re fines a parametric abstract specifi cation, assuming certain natural conditions on the parameter values (for example injectivity of the page tables) that are to be fi lled in. This first step essentially tells us that for any input speci fication P, if the parameters generated by the system generator satisfy the assumed conditions, then the generated system is correct vis-a-vis the abstract specifi cation. In the second step, which is input-speci fic, we check that for a given input speci fication, the assumptions actually hold for the generated parameter values. This gives us an effective veri fication technique for verifying generative systems.

We applied this technique to verify the Muen Separation Kernal. We chose to model the virtualization layer (in this case Intel's VT-x layer) along with the rest of the hardware components like registers and memory, programmatically in software. We carried out the first step of conditional parametric refi nement for Muen, using the Spark Ada veri fication tool. The effort involved about 20K lines of source code and annotation. We have also implemented a tool that automatically and effciently performs the Step 2 check for a given separation kernel con figuration. The tool is effective in proving the assumptions, leading to machine-checked proofs of correctness for 16 different input con figurations, as well as in detecting issues like undeclared sharing of memory components in some seeded faulty con figurations