Gernot Heiser
Kevin Elphinstone
Skip Abstract Section
Abstract
The L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions that are deployed on a large scale and in safety-critical systems. In this article we examine the lessons learnt in those 20 years about microkernel design and implementation. We revisit the L4 design articles and examine the evolution of design and implementation from the original L4 to the latest generation of L4 kernels. We specifically look at seL4, which has pushed the L4 model furthest and was the first OS kernel to undergo a complete formal verification of its implementation as well as a sound analysis of worst-case execution times. We demonstrate that while much has changed, the fundamental principles of minimality, generality, and high inter-process communication (IPC) performance remain the main drivers of design and implementation decisions.
- Mike Accetta, Robert Baron, William Bolosky, David Golub, Richard Rashid, Avadis Tevanian, and Michael Young. 1986. Mach: A new kernel foundation for UNIX development. In Proceedings of the 1986 Summer USENIX Technical Conference. US, 93--112.Google Scholar
- Michael T. Alexander. 1972. Organization and features of the Michigan terminal system. In AFIPS Conference Proceedings, 1972 Spring Joint Computer Conference. 585--591.Google Scholar
- Apple Inc. 2015. iOS security--iOS 9.0 or later. https://www.apple.com/business/docs/iOS Security Guide.pdf, September 2015.Google Scholar
- Andrew Baumann, Paul Barham, Pierre-Evariste Dagand, Tim Harris, Rebecca Isaacs, Simon Peter, Timothy Roscoe, Adrian Schüpbach, and Akhilesh Singhania. 2009. The multikernel: A new OS architecture for scalable multicore systems. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles.Google ScholarDigital Library
- Bernard Blackham and Gernot Heiser. 2012. Correct, fast, maintainable choose any three! In Proceedings of the Asia-Pacific Workshop on Systems (APSys). 7.Google Scholar
- Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury, and Gernot Heiser. 2011. Timing analysis of a protected operating system kernel. In Proceedings of the IEEE Real-Time Systems Symposium. 339--348.Google ScholarDigital Library
- Bernard Blackham, Yao Shi, and Gernot Heiser. 2012. Improving interrupt response time in a verifiable protected microkernel. In Proceedings of the EuroSys Conference. 323--336.Google ScholarDigital Library
- Per Brinch Hansen. 1970. The nucleus of a multiprogramming operating system. Commun. ACM 13 (1970), 238--250.Google ScholarDigital Library
- Alan C. Bromberger, A. Peri Frantz, William S. Frantz, Ann C. Hardy, Norman Hardy, Charles R. Landau, and Jonathan S. Shapiro. 1992. The KeyKOS nanokernel architecture. In Proceedings of the USENIX Workshop on Microkernels and Other Kernel Architectures. 95--112.Google Scholar
- J. Bradley Chen and Brian N. Bershad. 1993. The impact of operating system structure on memory system performance. In Proceedings of the 14th ACM Symposium on Operating Systems Principles. 120--133.Google Scholar
- Michael Condict, Don Bolinger, Dave Mitchell, and Eamonn McManus. 1994. Microkernel Modularity with Integrated Kernel Performance. Technical report. OSF Research Institute.Google Scholar
- Jack B. Dennis and Earl C. Van Horn. 1966. Programming semantics for multiprogrammed computations. Commun. ACM 9 (1966), 143--155.Google ScholarDigital Library
- Dhammika Elkaduwe, Philip Derrin, and Kevin Elphinstone. 2008. Kernel design for isolation and assurance of physical memory. In Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems.Google ScholarDigital Library
- Keir Fraser, Steven Hand, Rolf Neugebauer, Ian Pratt, Andrew Warfield, and Mark Williamson. 2004. Safe hardware access with the Xen virtual machine monitor. In Proceedings of the 1st Workshop on Operating System and Architectural Support for the On-Demand IT Infrastructure (OASIS).Google Scholar
- Eran Gabber, Christopher Small, John Bruno, José Brustoloni, and Avi Silberschatz. 1999. The Pebble component-based operating system. In Proceedings of the 1999 USENIX Annual Technical Conference. 267--282.Google Scholar
- Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang, and Gernot Heiser. 2005. Itanium—a system implementor’s tale. In Proceedings of the 2005 USENIX Annual Technical Conference. 264--278.Google Scholar
- Andreas Haeberlen. 2003. Managing Kernel Memory Resources from User Level. Diploma Thesis. Dept of Computer Science, University of Karlsruhe. http://os.ibds.kit.edu/english/97_639.php.Google Scholar
- Norman Hardy. 1985. KeyKOS architecture. ACM Operating Systems Review 19, 4 (Oct. 1985), 8--25.Google ScholarDigital Library
- Hermann Härtig, Robert Baumgartl, Martin Borriss, Claude-Joachim Hamann, Michael Hohmuth, Frank Mehnert, Lars Reuther, Sebastian Schönberg, and Jean Wolter. 1998. DROPS—OS support for distributed multimedia applications. In Proceedings of the 8th SIGOPS European Workshop.Google Scholar
- Hermann Härtig, Michael Hohmuth, Jochen Liedtke, Sebastian Schönberg, and Jean Wolter. 1997. The performance of μ-kernel-based systems. In Proceedings of the 16th ACM Symposium on Operating Systems Principles. 66--77.Google ScholarDigital Library
- Hermann Härtig and Michael Roitzsch. 2006. Ten years of research on L4-based real-time systems. In Proceedings of the 8th Real-Time Linux Workshop.Google Scholar
- Gernot Heiser. 2009. The Motorola Evoke QA4: A Case Study in Mobile Virtualization. White paper. Open Kernel Labs. Retrieved from https://www.researchgate.net/profile/Gernot_Heiser/publication/242743911_The_Motorola_Evoke_QA4_A_Case_Study_in_Mobile_Virtualization/links/00b7d53acc2c9d970d000000.pdf.Google Scholar
- Gernot Heiser, Etienne Le Sueur, Adrian Danis, Aleksander Budzynowski, Tudor-Ioan Salomie, and Gustavo Alonso. 2013. RapiLog: Reducing system complexity through verification. In Proceedings of the EuroSys Conference. 323--336.Google ScholarDigital Library
- Gernot Heiser and Ben Leslie. 2010. The OKL4 microvisor: Convergence point of microkernels and hypervisors. In Proceedings of the Asia-Pacific Workshop on Systems (APSys). 19--24.Google ScholarDigital Library
- Michael Hohmuth and Hermann Härtig. 2001. Pragmatic nonblocking synchronization for real-time systems. In Proceedings of the 2001 USENIX Annual Technical Conference.Google ScholarDigital Library
- Michael Hohmuth and Hendrik Tews. 2005. The VFiasco approach for a verified operating system. In Proceedings of the 2nd Workshop on Programming Languages and Operating Systems (PLOS).Google Scholar
- Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko, and Yoonho Park. 1999. Flexible access control using IPC redirection. In Proceedings of the 7th Workshop on Hot Topics in Operating Systems.Google ScholarCross Ref
- J. Leslie Keedy. 1979. On the Programming of Device Drivers for In-Process Systems. Monads Report 5. Dept. of Computer Science, Monash University, Clayton VIC, AU.Google Scholar
- Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32, 1 (Feb. 2014), 2:1--2:70.Google ScholarDigital Library
- Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: Formal verification of an OS kernel. In Proceedings of the ACM Symposium on Operating Systems Principles. 207--220.Google ScholarDigital Library
- Adam Lackorzynski and Alexander Warg. 2009. Taming subsystems: Capabilities as universal resource access control in L4. In Proceedings of the 2nd Workshop on Isolation and Integration in Embedded Systems. 25--30.Google ScholarDigital Library
- Adam Lackorzynski, Alexander Warg, Marcus Völp, and Hermann Härtig. 2012. Flattening hierarchical scheduling. In Proceedings of the International Conference on Embedded Software. 93--102.Google ScholarDigital Library
- Ben Leslie, Peter Chubb, Nicholas FitzRoy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone, and Gernot Heiser. 2005a. User-level device drivers: Achieved performance. J. Comput. Sci. Technol. 20, 5 (Sept. 2005), 654--664.Google ScholarCross Ref
- Ben Leslie, Carl van Schaik, and Gernot Heiser. 2005b. Wombat: A portable user-mode Linux for embedded systems. In 6th Linux.conf.au. Canberra.Google Scholar
- Roy Levin, Ellis S. Cohen, William M. Corwin, Fred J. Pollack, and William A. Wulf. 1975. Policy/mechanism separation in HYDRA. In Proceedings of the 5th ACM Symposium on Operating Systems Principles. 132--140.Google Scholar
- Jochen Liedtke. 1993a. Improving IPC by kernel design. In Proceedings of the 14th ACM Symposium on Operating Systems Principles. 175--188.Google ScholarDigital Library
- Jochen Liedtke. 1993b. A persistent system in real use: Experience of the first 13 years. In Proceedings of the 3rd IEEE International Workshop on Object Orientation in Operating Systems (IWOOOS). IEEE, 2--11.Google ScholarCross Ref
- Jochen Liedtke. 1995. On μ-kernel construction. In Proceedings of the 15th ACM Symposium on Operating Systems Principles. 237--250.Google Scholar
- Jochen Liedtke. 1996. Towards real microkernels. Commun. ACM 39, 9 (Sept. 1996), 70--77.Google ScholarDigital Library
- Jochen Liedtke, Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, and Gyula Szalay. 1991. Two years of experience with a μ-kernel based OS. ACM Operat. Syst. Rev. 25, 2 (April 1991), 51--62.Google ScholarDigital Library
- Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam, and Trent Jaeger. 1997a. Achieved IPC performance (still the foundation for extensibility). In Proceedings of the 6th Workshop on Hot Topics in Operating Systems. 28--31.Google ScholarCross Ref
- Jochen Liedtke, Nayeem Islam, and Trent Jaeger. 1997b. Preventing denial-of-service attacks on a μ-kernel for WebOSes. In Proceedings of the 6th Workshop on Hot Topics in Operating Systems. IEEE, 73--79.Google Scholar
- Steven B. Lipner. 1975. A comment on the confinement problem. In Proceedings of the 5th ACM Symposium on Operating Systems Principles. ACM, 192--196.Google ScholarDigital Library
- Richard J. Lipton and Lawrence Snyder. 1977. A linear time algorithm for deciding subject security. J. ACM 24, 3 (1977), 455--464.Google ScholarDigital Library
- Anna Lyons and Gernot Heiser. 2014. Mixed-criticality support in a high-assurance, general-purpose microkernel. In Proceedings of the Workshop on Mixed Criticality Systems. 9--14.Google Scholar
- Paul E. McKenney, Dipankar Sarma, Andrea Arcangelli, Andi Kleen, Orran Krieger, and Rusty Russell. 2002. Read copy update. In Proceedings of the Ottawa Linux Symposium.Google Scholar
- Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013. seL4: From general purpose to a proof of information flow enforcement. In Proceedings of the IEEE Symposium on Security and Privacy. 415--429.Google ScholarDigital Library
- Roger M. Needham and R. D. H. Walker. 1977. The Cambridge CAP computer and its protection system. In Proceedings of the 6th ACM Symposium on Operating Systems Principles. ACM, New York, NY, 1--10.Google ScholarDigital Library
- Michael Norrish. 1998. C Formalised in HOL. Ph.D. Dissertation. University of Cambridge Computer Laboratory.Google Scholar
- Abi Nourai. 2005. A Physically-Addressed L4 Kernel. BE Thesis. School of Computer Science and Engineering, Sydney, Australia. Available from publications page at http://ssrg.nicta.com.au/.Google Scholar
- John K. Ousterhout. 1990. Why aren’t operating systems getting faster as fast as hardware? In Proceedings of the 1990 Summer USENIX Technical Conference. 247--56.Google Scholar
- Sean Peters, Adrian Danis, Kevin Elphinstone, and Gernot Heiser. 2015. For a microkernel, a big lock is fine. In Proceedings of the Asia-Pacific Workshop on Systems (APSys).Google ScholarDigital Library
- Kaushik Kumar Ram, Jose Renato Santos, and Yoshio Turner. 2010. Redesigning Xen’s memory sharing mechanism for safe and efficient I/O virtualization. In Proceedings of the 2nd Workshop on I/O Virtualization.Google ScholarDigital Library
- Richard Rashid, Avadis Tevanian, Jr., Michael Young, David Golub, Robert Baron, David Black, William J. Bolosky, and Jonathan Chew. 1988. Machine-independent virtual memory management for paged uniprocessor and multiprocessor architectures. IEEE Trans. Comput. C-37 (1988), 896--908.Google Scholar
- Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, and Gerwin Klein. 2011. seL4 enforces integrity. In Proceedings of the International Conference on Interactive Theorem Proving. 325--340.Google ScholarCross Ref
- Jonathan S. Shapiro. 2003. Vulnerabilities in synchronous IPC designs. In Proceedings of the IEEE Symposium on Security and Privacy.Google ScholarCross Ref
- Jonathan S. Shapiro, Jonathan M. Smith, and David J. Farber. 1999. EROS: A fast capability system. In Proceedings of the 17th ACM Symposium on Operating Systems Principles. US, 170--185.Google Scholar
- Livio Soares and Michael Stumm. 2010. FlexSC: Flexible system call scheduling with exception-less system calls. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation.Google Scholar
- Udo Steinberg. 2013. Personal communication.Google Scholar
- Udo Steinberg and Bernhard Kauer. 2010. NOVA: A microhypervisor-based secure virtualization architecture. In Proceedings of the 5th EuroSys Conference. 209--222.Google ScholarDigital Library
- Udo Steinberg, Jean Wolter, and Hermann Härtig. 2005. Fast component interaction for real-time systems. In Euromicro Conference on Real-Time Systems. Palma de Mallorca, ES, 89--97.Google ScholarDigital Library
- Andrew S. Tanenbaum. 2016. Lessons learned from 30 years of MINIX. Commun. ACM 59, 3 (2016), 70--78.Google ScholarDigital Library
- Volkmar Uhlig. 2005. Scalability of Microkernel-Based Systems. Ph.D. Dissertation. University of Karlsruhe, Karlsruhe, Germany.Google Scholar
- Michael von Tessin. 2012. The clustered multikernel: An approach to formal verification of multiprocessor OS kernels. In 2nd Workshop on Systems for Future Multi-core Architectures. Bern, Switzerland, 1--6.Google Scholar
- Michael von Tessin. 2013. The Clustered Multikernel: An Approach to Formal Verification of Multiprocessor Operating-System Kernels. Ph.D. Thesis. School of Computer Science and Engineering, UNSW, Sydney, Australia.Google Scholar
- Matthew Warton. 2005. Single Kernel Stack L4. BE Thesis. School of Computer Science and Engineering, Sydney, Australia.Google Scholar
- Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. 2011. Making information flow explicit in HiStar. Commun. ACM 54, 11 (Nov. 2011), 93--101.Google ScholarDigital Library
Index Terms
- L4 Microkernels: The Lessons from 20 Years of Research and Deployment
Recommendations
From L3 to seL4 what have we learnt in 20 years of L4 microkernels?
SOSP '13: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems PrinciplesThe L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions which are deployed on a large scale and in safety-critical systems. In this paper we examine the lessons ...
seL4: formal verification of an OS kernel
SOSP '09: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principlesComplete formal verification is the only known way to guarantee that a system is free of programming errors.
We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to ...
Comprehensive formal verification of an OS microkernel
We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel.
We discuss the kernel design we used to make its verification tractable. We then describe the functional ...
Comments