Verified Protection Model of the seL4 Microkernel

Select |




Print


Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin

Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin


2008-10-06


Conference Material


Verified Software: Theories, Tools, and Experiments (VSTTE 2008)


Toronto, Canada


99--115


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 in terms of a classical take-grant model together with a formal proof of how confined subsystems can be enforced. All proofs and specifications in this paper are machine-checked and developed in the interactive theorem prover Isabelle/HOL.


Springer


http://qpq.csl.sri.com/vsr/vstte-08


3540878726


nicta:209


Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin. Verified Protection Model of the seL4 Microkernel. In: Natarajan Shankar and Jim Woodcock Editor, editor/s. Verified Software: Theories, Tools, and Experiments (VSTTE 2008); Toronto, Canada. Springer; 2008-10-06. 99--115.



Loading citation data...

Citation counts
(Requires subscription to view)