Paper Info
Title
Verified Protection Model of the seL4 Microkernel
Abstract
This paper presents a machine-checked high-level security analysis of seL4--an evolution of the L4 kernel series targeted to secure, embedded devices. We provide an abstract specification of the seL4 access control system together with a formal proof that shows how confined subsystems can be enforced. All proofs and specifications in this paper are developed in the interactive theorem prover Isabelle/HOL.
Year
DOI
Venue
2008
10.1007/978-3-540-87873-5_11
VSTTE
Keywords
Field
DocType
sel4 microkernel,formal proof,abstract specification,verified protection model,machine-checked high-level security analysis,l4 kernel series,sel4 access control system,interactive theorem prover,embedded device,access control,security analysis,theorem prover
HOL,Programming language,Computer science,Microkernel,Theoretical computer science,Security analysis,Mathematical proof,Access control,Transitive closure,Formal proof,Proof assistant
Conference
Volume
ISSN
Citations 
5295
0302-9743
17
PageRank 
References 
Authors
2.16
21
3
Name
Order
Citations
PageRank
Dhammika Elkaduwe168929.13
Gerwin Klein2145087.47
K. Elphinstone3119065.76