SeL4: Formal verification of an operating-system kernel

Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; Simon Winwood

doi:10.1145/1743546.1743574

SeL4: Formal verification of an operating-system kernel

Gerwin Klein^*, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

216 Citations (Scopus)

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.

Original language	English
Pages (from-to)	107-115
Number of pages	9
Journal	Communications of the ACM
Volume	53
Issue number	6
DOIs	https://doi.org/10.1145/1743546.1743574
Publication status	Published - 1 Jun 2010

Access to Document

10.1145/1743546.1743574

Cite this

@article{4b1614b139df415aa01c0dca83b05ae9,

title = "SeL4: Formal verification of an operating-system kernel",

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.",

author = "Gerwin Klein and June Andronick and Kevin Elphinstone and Gernot Heiser and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood",

year = "2010",

month = jun,

day = "1",

doi = "10.1145/1743546.1743574",

language = "English",

volume = "53",

pages = "107--115",

journal = "Communications of the ACM",

issn = "0001-0782",

publisher = "Association for Computing Machinery (ACM)",

number = "6",

}

TY - JOUR

T1 - SeL4

T2 - Formal verification of an operating-system kernel

AU - Klein, Gerwin

AU - Andronick, June

AU - Elphinstone, Kevin

AU - Heiser, Gernot

AU - Cock, David

AU - Derrin, Philip

AU - Elkaduwe, Dhammika

AU - Engelhardt, Kai

AU - Kolanski, Rafal

AU - Norrish, Michael

AU - Sewell, Thomas

AU - Tuch, Harvey

AU - Winwood, Simon

PY - 2010/6/1

Y1 - 2010/6/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=77953210383&partnerID=8YFLogxK

U2 - 10.1145/1743546.1743574

DO - 10.1145/1743546.1743574

M3 - Article

SN - 0001-0782

VL - 53

SP - 107

EP - 115

JO - Communications of the ACM

JF - Communications of the ACM

IS - 6

ER -

SeL4: Formal verification of an operating-system kernel

Abstract

Access to Document

Other files and links

Fingerprint

Cite this