Verified Protection Model of the seL4 Microkernel

Select |




Print


Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin

Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin


2007-10-19


Report


Sydney


NRL-1474


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 its decidability. Using the decidability property we show 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


seL4, access control, proof, Isabelle/HOL


nicta:1474


Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin. Verified Protection Model of the seL4 Microkernel. 2007-10-19. nicta:1474.



Loading citation data...

Citation counts
(Requires subscription to view)