Skip to main content
SpringerLink
Log in

From a Verified Kernel towards Verified Systems

  • Conference paper
Programming Languages and Systems (APLAS 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6461))

Included in the following conference series:

Abstract

The L4.verified project has produced a formal, machine- checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper briefly summarises the proof, its main implications and assumptions, reports on the experience in conducting such a large-scale verification, and finally lays out a vision how this formally verified kernel may be used for gaining formal, code-level assurance about safety and security properties of systems on the order of a million lines of code.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

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. Andronick, J., Greenaway, D., Elphinstone, K.: Towards proving security in the presence of large untrusted components. In: Klein, G., Huuck, R., Schlich, B. (eds.) Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada. USENIX (October 2010)

    Google Scholar 

  2. Bevier, W.R.: Kit: A study in operating system verification. IEEE Transactions on Software Engineering 15(11), 1382–1396 (1989)

    Article  Google Scholar 

  3. Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning 5(4), 411–428 (1989)

    Google Scholar 

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

  5. Boyton, A.: A verified shared capability model. In: Klein, G., Huuck, R., Schlich, B. (eds.) Proceedings of the 4th Workshop on Systems Software Verification, Aachen, Germany. Electronic Notes in Computer Science, vol. 254, pp. 25–44. Elsevier, Amsterdam (2009)

    Google Scholar 

  6. Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 167–182. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  7. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Elkaduwe, D., Klein, G., Elphinstone, K.: Verified protection model of the seL4 microkernel. Technical Report NRL-1474, NICTA (October 2007), http://ertos.nicta.com.au/publications/papers/Elkaduwe_GE_07.pdf

  9. Feiertag, R.J., Neumann, P.G.: The foundations of a provably secure operating system (PSOS). In: AFIPS Conference Proceedings, 1979 National Computer Conference, New York, NY, USA, pp. 329–334 (June 1979)

    Google Scholar 

  10. Hart, B.: SDR security threats in an open source world. In: Software Defined Radia Conference, Phoenix, AZ, USA, pp. 3.5–3 1–4 (November 2004)

    Google Scholar 

  11. Klein, G.: Correct OS kernel? proof? done! USENIX;login: 34(6), 28–34 (2009)

    Google Scholar 

  12. Klein, G., Andronick, J., Elphinstone, K., Heiser, G., 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. Communications of the ACM 53(6), 107–115 (2010)

    Article  Google Scholar 

  13. 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: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, pp. 207–220. ACM, New York (2009)

    Chapter  Google Scholar 

  14. Koscher, K., Czeskis, A., Roesner, F., Patel, S., Kohno, T., Checkoway, S., McCoy, D., Kantor, B., Anderson, D., Shacham, H., Savage, S.: Experimental security analysis of a modern automobile. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, USA, pp. 447–462 (May 2010)

    Google Scholar 

  15. Kuz, I., Klein, G., Lewis, C., Walker, A.: capDL: A language for describing capability-based systems. In: Proceedings of the 1st Asia-Pacific Workshop on Systems, New Delhi, India (to appear, August 2010)

    Google Scholar 

  16. Meng, J., Paulson, L.C., Klein, G.: A termination checker for Isabelle Hoare logic. In: Beckert, B. (ed.) Proceedings of the 4th International Verification Workshop, Bremen, Germany. CEUR Workshop Proceedings, vol. 259, pp. 104–118 (July 2007)

    Google Scholar 

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

    MATH  Google Scholar 

  18. Richards, R.J.: Modeling and security analysis of a commercial real-time operating system kernel. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 301–322. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, pp. 97–108 (January 2007)

    Google Scholar 

  20. Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. Communications of the ACM 23(2), 118–131 (1980)

    Article  MATH  Google Scholar 

  21. Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., Norrish, M.: Mind the gap: A verification framework for low-level C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol. 5674, pp. 500–515. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  22. Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, Toronto, Ontario, Canada, pp. 99–110. ACM, New York (June 2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NICTA, Australia

    Gerwin Klein

  2. 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. Dept. of Computer Science and Engineering, Waseda University, 3-4-1, Okubo, Shinjuku-ku, 169-8555, Tokyo, Japan

    Kazunori Ueda

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klein, G. (2010). From a Verified Kernel towards Verified Systems. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17164-2_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17163-5

  • Online ISBN: 978-3-642-17164-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation