Abstract
Last year, the NICTA L4.verified project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper gives a brief overview of the proof together with its main implications and assumptions, and paints a vision on how this verified kernel can be used for gaining assurance of overall system security on the code level for systems of a million lines of code or more. © 2010 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Klein, G. (2010). The L4.verified project - Next steps. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6217 LNCS, pp. 86–96). https://doi.org/10.1007/978-3-642-15057-9_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
