From L3 to seL4 what have we learnt in 20 years of L4 microkernels?

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 which are deployed on a large scale and in safety-critical systems. In this paper we examine the lessons learnt in those 20 years about microkernel design and implementation. We revisit the L4 design papers, and examine the evolution of design and implementation from the original L4 to the latest generation of L4 kernels, especially 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 and high IPC performance remain the main drivers of design and implementation decisions.

References

1. Michael T. Alexander. Organization and features of the Michigan terminal system. In AFIPS Conference Proceedings, 1972 Spring Joint Computer Conference, pages 585--591, 1972.
2. Andrew Baumann, Paul Barham, Pierre-Evariste Dagand, Tim Harris, Rebecca Isaacs, Simon Peter, Timothy Roscoe, Adrian Schüpbach, and Akhilesh Singhania. The multikernel: A new OS architecture for scalable multicore systems. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October 2009. ACM.
3. Bernard Blackham and Gernot Heiser. Correct, fast, maintainable -- choose any three! In Proceedings of the 3rd Asia-Pacific Workshop on Systems (APSys), pages 13:1--13:7, Seoul, Korea, July 2012. doi: 10.1145/2349896.2349909.
4. Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury, and Gernot Heiser. Timing analysis of a protected operating system kernel. In Proceedings of the 32nd IEEE Real-Time Systems Symposium, pages 339--348, Vienna, Austria, November 2011. doi: 10.1109/RTSS.2011.38.
5. Bernard Blackham, Yao Shi, and Gernot Heiser. Improving interrupt response time in a verifiable protected microkernel. In Proceedings of the 7th EuroSys Conference, pages 323--336, Bern, Switzerland, April 2012. doi: 10.1145/2168836.2168869.
6. Per Brinch Hansen. The nucleus of a multiprogramming operating system. Communications of the ACM, 13: 238--250, 1970.
7. J. Bradley Chen and Brian N. Bershad. The impact of operating system structure on memory system performance. In Proceedings of the 14th ACM Symposium on Operating Systems Principles, pages 120--133, Asheville, NC, USA, December 1993.
8. Michael Condict, Don Bolinger, Dave Mitchell, and Eamonn McManus. Microkernel modularity with integrated kernel performance. Technical report, OSF Research Institute, June 1994.
9. Jack B. Dennis and Earl C. Van Horn. Programming semantics for multiprogrammed computations. Communications of the ACM, 9:143--155, 1966.
10. Dhammika Elkaduwe, Philip Derrin, and Kevin Elphinstone. Kernel design for isolation and assurance of physical memory. In 1st Workshop on Isolation and Integration in Embedded Systems, pages 35--40, Glasgow, UK, April 2008. ACM SIGOPS. doi: 10.1145/1435458.
11. Keir Fraser, Steven Hand, Rolf Neugebauer, Ian Pratt, Andrew Warfield, and Mark Williamson. 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), 2004.
12. Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang, and Gernot Heiser. Itanium --- a system implementor's tale. In Proceedings of the 2005 USENIX Annual Technical Conference, pages 264--278, Anaheim, CA, USA, April 2005.
13. Andreas Haeberlen. Managing kernel memory resources from user level. Diploma thesis, Dept of Computer Science, University of Karlsruhe, April 2003. URL http://os.ibds.kit.edu/english/97_639.php.
14. Hermann Härtig and Michael Roitzsch. Ten years of research on L4-based real-time systems. In Proceedings of the 8th Real-Time Linux Workshop, Lanzhou, China, 2006.
15. Hermann Härtig, Michael Hohmuth, Jochen Liedtke, Sebastian Schönberg, and Jean Wolter. The performance of μ-kernel-based systems. In Proceedings of the 16th ACM Symposium on Operating Systems Principles, pages 66--77, St. Malo, France, October 1997.
16. Gernot Heiser and Ben Leslie. The OKL4 Microvisor: Convergence point of microkernels and hypervisors. In Proceedings of the 1st Asia-Pacific Workshop on Systems (APSys), pages 19--24, New Delhi, India, August 2010.
17. Michael Hohmuth and Hermann Härtig. Pragmatic non-blocking synchronization for real-time systems. In Proceedings of the 2001 USENIX Annual Technical Conference, Boston, MA, USA, 2001.
18. Michael Hohmuth and Hendrik Tews. The VFiasco approach for a verified operating system. In Proceedings of the 2nd Workshop on Programming Languages and Operating Systems (PLOS), Glasgow, UK, July 2005.
19. Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko, and Yoonho Park. Flexible access control using IPC redirection. In Proceedings of the 7th Workshop on Hot Topics in Operating Systems, Rio Rico, AZ, USA, March 1999.
20. J. Leslie Keedy. On the programming of device drivers for in-process systems. Monads Report 5, Dept. of Computer Science, Monash University, Clayton VIC, Australia, 1979.
21. 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. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles, pages 207--220, Big Sky, MT, USA, October 2009. ACM. doi: 10.1145/1629575.1629596.
22. Adam Lackorzynski and Alexander Warg. Taming sub-systems: capabilities as universal resource access control in L4. In 2nd Workshop on Isolation and Integration in Embedded Systems, pages 25--30, Nuremburg, Germany, March 2009.
23. Adam Lackorzynski, Alexander Warg, Marcus Völp, and Hermann Härtig. Flattening hierarchical scheduling. In International Conference on Embedded Software, pages 93--102, Tampere, Finland, October 2012.
24. Ben Leslie, Peter Chubb, Nicholas FitzRoy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone, and Gernot Heiser. User-level device drivers: Achieved performance. Journal of Computer Science and Technology, 20(5):654--664, September 2005.
25. Roy Levin, Ellis S. Cohen, William M. Corwin, Fred J. Pollack, and William A. Wulf. Policy/mechanism separation in HYDRA. In Proceedings of the 5th ACM Symposium on Operating Systems Principles, pages 132--140, 1975.
26. Jochen Liedtke. Improving IPC by kernel design. In Proceedings of the 14th ACM Symposium on Operating Systems Principles, pages 175--188, Asheville, NC, USA, December 1993a.
27. Jochen Liedtke. 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), pages 2--11, Asheville, NC, USA, December 1993b. IEEE.
28. Jochen Liedtke. On μ-kernel construction. In Proceedings of the 15th ACM Symposium on Operating Systems Principles, pages 237--250, Copper Mountain, CO, USA, December 1995.
29. Jochen Liedtke. Towards real microkernels. Communications of the ACM, 39(9):70--77, September 1996.
30. Jochen Liedtke, Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, and Gyula Szalay. Two years of experience with a μ-kernel based OS. ACM Operating Systems Review, 25(2):51--62, April 1991.
31. Jochen Liedtke, Kevin Elphinstone, Sebastian Schönberg, Herrman Härtig, Gernot Heiser, Nayeem Islam, and Trent Jaeger. Achieved IPC performance (still the foundation for extensibility). In Proceedings of the 6th Workshop on Hot Topics in Operating Systems, pages 28--31, Cape Cod, MA, USA, May 1997a.
32. Jochen Liedtke, Nayeem Islam, and Trent Jaeger. Preventing denial-of-service attacks on a μ-kernel for WebOSes. In Proceedings of the 6th Workshop on Hot Topics in Operating Systems, pages 73--79, Cape Cod, MA, USA, May 1997b. IEEE.
33. Steven. B. Lipner. A comment on the confinement problem. In Proceedings of the 5th ACM Symposium on Operating Systems Principles, pages 192--196. ACM, 1975.
34. Richard J. Lipton and Lawrence Snyder. A linear time algorithm for deciding subject security. Journal of the ACM, 24(3):455--464, 1977. ISSN 0004-5411. doi: http://doi.acm.org/10.1145/322017.322025.
35. Paul E. McKenney, Dipankar Sarma, Andrea Arcangelli, Andi Kleen, Orran Krieger, and Rusty Russell. Read copy update. In Proceedings of the Ottawa Linux Symposium, 2002. URL http://www.rdrop.com/users/paulmck/rclock/rcu.2002.07.08.pdf.
36. Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. seL4: from general purpose to a proof of information flow enforcement. In IEEE Symposium on Security and Privacy, pages 415--429, San Francisco, CA, May 2013. ISBN 10.1109/SP.2013.35.
37. Roger M. Needham and R. D. H. Walker. The Cambridge CAP computer and its protection system. In Proceedings of the 6th ACM Symposium on Operating Systems Principles, pages 1--10. ACM, November 1977.
38. Michael Norrish. C formalised in HOL. PhD thesis, University of Cambridge Computer Laboratory, 1998.
39. Abi Nourai. A physically-addressed L4 kernel. BE thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, March 2005. Available from publications page at http://ssrg.nicta.com.au/.
40. John K. Ousterhout. Why aren't operating systems getting faster as fast as hardware? In Proceedings of the 1990 Summer USENIX Technical Conference, pages 247--56, June 1990.
41. Kaushik Kumar Ram, Jose Renato Santos, and Yoshio Turner. Redesigning Xen's memory sharing mechanism for safe and efficient I/O virtualization. In Proceedings of the 2nd Workshop on I/O Virtualization, Pittsburgh, PA, USA, 2010. USENIX.
42. Richard Rashid, Avadis Tevanian, Jr., Michael Young, David Golub, Robert Baron, David Black, William J. Bolosky, and Jonathan Chew. Machine-independent virtual memory management for paged uniprocessor and multiprocessor architectures. IEEE Transactions on Computers, C-37:896--908, 1988.
43. Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, and Gerwin Klein. seL4 enforces integrity. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, 2nd International Conference on Interactive Theorem Proving, volume 6898 of Lecture Notes in Computer Science, pages 325--340, Nijmegen, The Netherlands, August 2011. Springer. doi: http://dx.doi.org/10.1007/978-3-642-22863-6_24.
44. Jonathan S. Shapiro. Vulnerabilities in synchronous IPC designs. In Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, USA, May 2003. URL citeseer.ist.psu.edu/shapiro03vulnerabilities.html.
45. Jonathan S. Shapiro, Jonathan M. Smith, and David J. Farber. EROS: A fast capability system. In Proceedings of the 17th ACM Symposium on Operating Systems Principles, pages 170--185, Charleston, SC, USA, December 1999. URL http://www.eros-os.org/papers/sosp99-eros-preprint.ps.
46. Udo Steinberg. Personal communication, 2013.
47. Udo Steinberg and Bernhard Kauer. NOVA: A microhypervisor-based secure virtualization architecture. In Proceedings of the 5th EuroSys Conference, Paris, France, April 2010.
48. Udo Steinberg, Jean Wolter, and Hermann Härtig. Fast component interaction for real-time systems. In Euromicro Conference on Real-Time Systems, pages 89--97, Palma de Mallorca, Spain, July 2005.
49. Volkmar Uhlig. Scalability of Microkernel-Based Systems. PhD thesis, University of Karlsruhe, Karlsruhe, Germany, June 2005.
50. Michael von Tessin. The clustered multikernel: An approach to formal verification of multiprocessor OS kernels. In Proceedings of the 2nd Workshop on Systems for Future Multi-core Architectures, Bern, Switzerland, April 2012.
51. Matthew Warton. Single kernel stack L4. BE thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, November 2005.
52. Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. Making information flow explicit in HiStar. Communications of the ACM, 54(11): 93--101, November 2011.