SeL4: Formal verification of an operating-system kernel
-
Altmetric Citations
Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Heiser, Gernot; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon
Description
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...[Show more]
Collections | ANU Research Publications |
---|---|
Date published: | 2010 |
Type: | Journal article |
URI: | http://hdl.handle.net/1885/52945 |
Source: | Communications of the Association for Computing Machinery |
DOI: | 10.1145/1743546.1743574 |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
01_Klein_SeL4:_Formal_verification_of_2010.pdf | 420.52 kB | Adobe PDF | Request a copy |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator