s
s;

State relation
State relation
s
s;

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