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]
dc.contributor.author | Klein, Gerwin | |
---|---|---|
dc.contributor.author | Andronick, June | |
dc.contributor.author | Elphinstone, Kevin | |
dc.contributor.author | Heiser, Gernot | |
dc.contributor.author | Cock, David | |
dc.contributor.author | Derrin, Philip | |
dc.contributor.author | Elkaduwe, Dhammika | |
dc.contributor.author | Engelhardt, Kai | |
dc.contributor.author | Kolanski, Rafal | |
dc.contributor.author | Norrish, Michael | |
dc.contributor.author | Sewell, Thomas | |
dc.contributor.author | Tuch, Harvey | |
dc.contributor.author | Winwood, Simon | |
dc.date.accessioned | 2015-12-10T22:23:45Z | |
dc.identifier.issn | 0001-0782 | |
dc.identifier.uri | http://hdl.handle.net/1885/52945 | |
dc.description.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. | |
dc.publisher | Association for Computing Machinery Inc (ACM) | |
dc.source | Communications of the Association for Computing Machinery | |
dc.subject | Keywords: Abstract specifications; Assembly code; Formal verifications; Safety property; System kernel; Third generation; Specifications; Abstracting | |
dc.title | SeL4: Formal verification of an operating-system kernel | |
dc.type | Journal article | |
local.description.notes | Imported from ARIES | |
local.identifier.citationvolume | 53 | |
dc.date.issued | 2010 | |
local.identifier.absfor | 080199 - Artificial Intelligence and Image Processing not elsewhere classified | |
local.identifier.ariespublication | f2965xPUB260 | |
local.type.status | Published Version | |
local.contributor.affiliation | Klein, Gerwin, National ICT Australia | |
local.contributor.affiliation | Andronick, June, University of New South Wales | |
local.contributor.affiliation | Elphinstone, Kevin, University of New South Wales | |
local.contributor.affiliation | Heiser, Gernot, University of New South Wales | |
local.contributor.affiliation | Cock, David, University of New South Wales | |
local.contributor.affiliation | Derrin, Philip, University of New South Wales | |
local.contributor.affiliation | Elkaduwe, Dhammika, University of New South Wales | |
local.contributor.affiliation | Engelhardt, Kai, University of New South Wales | |
local.contributor.affiliation | Kolanski, Rafal, University of New South Wales | |
local.contributor.affiliation | Norrish, Michael, College of Engineering and Computer Science, ANU | |
local.contributor.affiliation | Sewell, Thomas, University of New South Wales | |
local.contributor.affiliation | Tuch, Harvey, National ICT Australia | |
local.contributor.affiliation | Winwood, Simon, University of New South Wales | |
local.description.embargo | 2037-12-31 | |
local.bibliographicCitation.issue | 6 | |
local.bibliographicCitation.startpage | 107 | |
local.bibliographicCitation.lastpage | 115 | |
local.identifier.doi | 10.1145/1743546.1743574 | |
local.identifier.absseo | 970108 - Expanding Knowledge in the Information and Computing Sciences | |
dc.date.updated | 2016-02-24T08:26:30Z | |
local.identifier.scopusID | 2-s2.0-77953210383 | |
local.identifier.thomsonID | 000278635800034 | |
Collections | ANU Research Publications |
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