Name
Abstract | ||
|---|---|---|
We report on the formal, machine-checked verication of the seL4 microkernel from an abstract specication down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code. seL4 is a third-generation microkernel of L4 provenance, comprising 8,700 lines of C and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels. We prove that the implementation always strictly follows our high-level abstract specication of kernel behaviour. This encompasses traditional design and implementation safety properties such as that the kernel will never crash, and it will never perform an unsafe operation. It also implies much more: we can predict precisely how the kernel will behave in every possible situation. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1145/1743546.1743574 | Commun. ACM |
Keywords | Field | DocType |
operating-system kernel,formal verification,operating system | Kernel (linear algebra),Programming language,Computer science,Abstract interpretation,Correctness,Microkernel,Compiler,Assembly language,Kernel preemption,Operating system,Formal verification | Journal |
Volume | Issue | ISSN |
53 | 6 | 0001-0782 |
Citations | PageRank | References |
84 | 5.86 | 7 |
Authors | ||
13 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gerwin Klein | 1 | 1450 | 87.47 |
| June Andronick | 2 | 903 | 42.66 |
| K. Elphinstone | 3 | 1190 | 65.76 |
| Gernot Heiser | 4 | 2525 | 137.42 |
| David Cock | 5 | 827 | 37.44 |
| Philip Derrin | 6 | 726 | 31.12 |
| Dhammika Elkaduwe | 7 | 689 | 29.13 |
| Kai Engelhardt | 8 | 762 | 35.62 |
| Rafal Kolanski | 9 | 802 | 34.23 |
| Michael Norrish | 10 | 1091 | 61.77 |
| Thomas Sewell | 11 | 914 | 37.60 |
| Harvey Tuch | 12 | 791 | 35.74 |
| Simon Winwood | 13 | 713 | 30.07 |