Paper Info
Title
From a proven correct microkernel to trustworthy large systems
Abstract
The seL4 microkernel was the world's first general-purpose operating system kernel with a formal, machine-checked proof of correctness. The next big step in the challenge of building truly trustworthy systems is to provide a framework for developing secure systems on top of seL4. This paper first gives an overview of seL4's correctness proof, together with its main implications and assumptions, and then describes our approach to provide formal security guarantees for large, complex systems.
Year
DOI
Venue
2010
10.1007/978-3-642-18070-5_1
FoVeOOS
Keywords
Field
DocType
trustworthy system,secure system,formal security guarantee,sel4 microkernel,complex system,main implication,large system,proven correct microkernel,general-purpose operating system kernel,machine-checked proof,correctness proof,next big step,operating system
Complex system,Programming language,Trustworthiness,Computer science,Correctness,Hoare logic,Microkernel,Enterprise information security architecture,Computer security model,Distributed computing,Formal verification
Conference
Volume
ISSN
ISBN
6528
0302-9743
3-642-18069-8
Citations 
PageRank 
References 
1
0.36
8
Authors
1
Name
Order
Citations
PageRank
June Andronick190342.66