Paper Info
Title
A formally verified OS kernel. now what?
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.
Year
DOI
Venue
2010
10.1007/978-3-642-14052-5_1
ITP
Keywords
Field
DocType
last year,os kernel,hol proof,machine-checked isabelle,sel4 os microkernel,abstract implementation,main implication,c code,overall system security,future research direction,system security
HOL,Kernel (linear algebra),Computer science,Algorithm,Microkernel,System call,Os kernel,Operating system kernel
Conference
Volume
ISSN
ISBN
6172
0302-9743
3-642-14051-3
Citations 
PageRank 
References 
2
0.39
7
Authors
1
Name
Order
Citations
PageRank
Gerwin Klein1145087.47