Skip to main content

TS

Verified protection model of the seL4 microkernel

Authors

Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone

NICTA

UNSW

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 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.

BibTeX Entry

  @inproceedings{Elkaduwe_KE_08,
    publisher        = {Springer},
    isbn             = {3540878726},
    author           = {Elkaduwe, Dhammika and Klein, Gerwin and Elphinstone, Kevin},
    month            = oct,
    editor           = {{Natarajan Shankar and Jim Woodcock}},
    year             = {2008},
    title            = {Verified Protection Model of the {seL4} Microkernel},
    booktitle        = {Verified Software: Theories, Tools and Experiments},
    pages            = {99--115},
    address          = {Toronto, Canada }
  }

Download

Served by Apache on Linux on seL4.