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