Concrete operation M2
our state machines: kernel transitions, user transitions, user
events, idle transitions, and idle events. Kernel transitions are
those that are described by each of the specification layers
in increasing amount of detail. User transitions are specified
as nondeterministically changing arbitrary user-accessible
parts of the state space. User-events model kernel entry (trap
instructions, faults, interrupts). Idle transitions model the
behavior of the idle thread. Finally, idle events are interrupts
occurring during idle time; other interrupts that occur during kernel execution are modelled explicitly and separately in
each layer of Figure 2.
The model of the machine and the model of user programs remain the same across all refinement layers; only
the details of kernel behavior and kernel data structures
change. The fully nondeterministic model of the user means
that our proof includes all possible user behaviors, be they
benign, buggy, or malicious.
Let machine MA denote the system framework instantiated with the abstract specification of Section 4. 1, let
machine ME represent the framework instantiated with the
executable specification of Section 4. 2, and let machine MC
stand for the framework instantiated with the C program
read into the theorem prover. Then we prove the following
two, very simple-looking theorems:
Theorem 1. ME refines MA.
Theorem 2. MC refines ME.
Therefore, because refinement is transitive, we have
Theorem 3. MC refines MA.
4. 5. assumptions
Formal verification can never be absolute; it always must
make fundamental assumptions. The assumptions we
make are correctness of the C compiler, the assembly code, the
hardware, and kernel initialization. We explain each of them
in more detail below.
The initialization code takes up about 1. 2 kloc of the ker-
nel. The theorems in Section 4. 4 only state correspondence
between entry and exit points in each specification layer for
a running kernel.
5. eXPeRience anD Lessons LeaRneD
5. 1. Verification effort
The project was conducted in three phases. First an initial kernel with limited functionality (no interrupts,
single address space, and generic linear page table) was
designed and implemented in Haskell, while the verification team mostly worked on the verification framework
and generic proof libraries. In a second phase, the verification team developed the abstract spec and performed the