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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
Bevier, W.R.: Kit: A study in operating system verification. IEEE Transactions on Software Engineering 15(11), 1382–1396 (1989)
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)
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)
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)
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)
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)
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
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)
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)
Klein, G.: Correct OS kernel? proof? done! USENIX;login: 34(6), 28–34 (2009)
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)
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)
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)
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)
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)
Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
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)
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)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)