Abstract
Last year, the 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. In my presentation I will summarise the proof together with its main implications and assumptions, I will describe in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security, and I will explore further future research directions that open up with a formally verified OS kernel. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Klein, G. (2010). A formally verified OS kernel. Now what? In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6172 LNCS, pp. 1–7). https://doi.org/10.1007/978-3-642-14052-5_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
