Skip to main content
SpringerLink
Log in

A Formally Verified OS Kernel. Now What?

  • Conference paper
Book cover Interactive Theorem Proving (ITP 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6172))

Included in the following conference series:

Abstract

Last year, the L4.verified project produced a formal, machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. In my presentation I will summarise the proof together with its main implications and assumptions, I will describe in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security, and I will explore further future research directions that open up with a formally verified OS kernel.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Boettcher, C., DeLong, R., Rushby, J., Sifre, W.: The MILS component integration approach to secure information sharing. In: 27th IEEE/AIAA Digital Avionics Systems Conference (DASC), St. Paul MN (October 2008)

    Google Scholar 

  2. Boyton, A.: A verified shared capability model. In: Klein, G., Huuck, R., Schlich, B. (eds.) 4th WS Syst. Softw. Verification SSV’09, Aachen, Germany, October 2009. ENTCS, vol. 254, pp. 25–44. Elsevier, Amsterdam (2009)

    Google Scholar 

  3. Elkaduwe, D., Klein, G., Elphinstone, K.: Verified protection model of the seL4 microkernel. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 99–114. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the armv7 instruction set architecture. In: Kaufmann, M., Paulson, L. (eds.) ITP’10. LNCS, vol. 6172, pp. 244–259. Springer, Heidelberg (2010)

    Google Scholar 

  5. Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: 22nd SOSP, Big Sky, MT, USA. October 2009, pp. 207–220. ACM, New York (2009)

    Chapter  Google Scholar 

  6. Leroy, X.: Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) 33rd POPL, pp. 42–54. ACM, New York (2006)

    Google Scholar 

  7. Myreen, M.O., Slind, K., Gordon, M.J.C.: Extensible proof-producing compilation. In: de Moor, O., Schwartzbach, M.I. (eds.) CC 2009. LNCS, vol. 5501, pp. 2–16. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  9. Saltzer, J.H., Schroeder, M.D.: The protection of information in computer systems. Proc. IEEE 63, 1278–1308 (1975)

    Article  Google Scholar 

  10. Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. PhD thesis, Technische Universität München (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NICTA, Australia, School of Computer Science and Engineering, UNSW, Sydney, Australia

    Gerwin Klein

Authors
  1. Gerwin Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Sciences, University of Texas, Austin, Talyor Hall 2.124, 78712-1188, Austin, TX, USA

    Matt Kaufmann

  2. Computer Laboratory, University of Cambridge, CB3 0FD, Cambridge,, UK

    Lawrence C. Paulson

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klein, G. (2010). A Formally Verified OS Kernel. Now What?. In: Kaufmann, M., Paulson, L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14052-5_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14051-8

  • Online ISBN: 978-3-642-14052-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation