SeL4: Formal verification of an operating-system kernel

Date

2010

Authors

Klein, Gerwin
Andronick, June
Elphinstone, Kevin
Heiser, Gernot
Cock, David
Derrin, Philip
Elkaduwe, Dhammika
Engelhardt, Kai
Kolanski, Rafal
Norrish, Michael

Journal Title

Journal ISSN

Volume Title

Publisher

Association for Computing Machinery Inc (ACM)

Abstract

We report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification 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 8700 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 specification of kernel behavior. 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.

Description

Keywords

Keywords: Abstract specifications; Assembly code; Formal verifications; Safety property; System kernel; Third generation; Specifications; Abstracting

Citation

Source

Communications of the Association for Computing Machinery

Type

Journal article

Book Title

Entity type

Access Statement

License Rights

DOI

10.1145/1743546.1743574

Restricted until

2037-12-31