Verified Protection Model of the seL4 Microkernel

  • Dhammika Elkaduwe
  • Gerwin Klein
  • Kevin Elphinstone
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


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.


Transitive Closure Access Control Model Physical Memory Protection Model Current System State 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bishop, M.: Conspiracy and information flow in the take-grant protection model. Journal of Computer Security 4(4), 331–360 (1996)Google Scholar
  2. 2.
    Bishop, M., Snyder, L.: The transfer of information and authority in a protection system. In: 7th SOSP, pp. 45–54. ACM Press, New York (1979)Google Scholar
  3. 3.
    Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Munoz, C., Ait, O. (eds.) TPHOLs 2008. LNCS 5170 (to appear, 2008)Google Scholar
  4. 4.
    Dennis, J.B., Van Horn, E.C.: Programming semantics for multiprogrammed computations. CACM 9, 143–155 (1966)zbMATHGoogle Scholar
  5. 5.
    Derrin, P., Elphinstone, K., Klein, G., Cock, D., Chakravarty, M.M.T.: Running the manual: An approach to high-assurance microkernel development. In: ACM SIGPLAN Haskell WS, Portland, OR, USA (September 2006)Google Scholar
  6. 6.
    Elkaduwe, D., Derrin, P., Elphinstone, K.: A memory allocation model for an embedded microkernel. In: Proc. 1st MicroKernels for Embedded Systems, Sydney, Australia, pp. 28–34. NICTA (January 2007)Google Scholar
  7. 7.
    Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a practical, verified kernel. In: 11th HotOS, San Diego, CA, USA (May 2007)Google Scholar
  8. 8.
    Elphinstone, K., Klein, G., Kolanski, R.: Formalising a high-performance microkernel. In: Leino, R. (ed.) Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 2006), Microsoft Research Technical Report MSR-TR-2006-117, pp. 1–7, Seattle, USA (August 2006)Google Scholar
  9. 9.
    Hardy, N.: KeyKOS architecture. Operat. Syst. Rev. 19(4), 8–25 (1985)CrossRefMathSciNetGoogle Scholar
  10. 10.
    Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. In: CACM, pp. 561–471 (1976)Google Scholar
  11. 11.
    Leslie, B., van Schaik, C., Heiser, G.: Wombat: A portable user-mode Linux for embedded systems. In: 6th Linux.Conf.Au, Canberra (April 2005)Google Scholar
  12. 12.
    Liedtke, J.: On μ-kernel construction. In: 15th SOSP, Copper Mountain, CO, USA, pp. 237–250 (December 1995)Google Scholar
  13. 13.
    Lipton, R.J., Snyder, L.: A linear time algorithm for deciding subject security. J. ACM 24(3), 455–464 (1977)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    National ICT Australia. seL4 Reference Manual (2006),
  15. 15.
    Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  16. 16.
    Nuutila, E.: Efficient transitive closure computation in large digraphs. PhD thesis, Helsinki University of Technology (June 1995)Google Scholar
  17. 17.
    Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report (December 1992),
  18. 18.
    Shapiro, J.S.: The practical application of a decidable access model. Technical Report SRL-2003-04, SRL, Baltimore, MD 21218 (November 2003)Google Scholar
  19. 19.
    Shapiro, J.S., Smith, J.M., Farber, D.J.: EROS: A fast capability system. In: 17th SOSP, Charleston, SC, USA, pp. 170–185 (December 1999)Google Scholar
  20. 20.
    Snyder, L.: Theft and conspiracy in the Take-Grant protection model. Journal of Computer and System Sciences 23(3), 333–347 (1981)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Dhammika Elkaduwe
    • 1
  • Gerwin Klein
    • 1
  • Kevin Elphinstone
    • 1
  1. 1.NICTA and University of New South WalesSydneyAustralia

Personalised recommendations