The L4 Microkernel

L4 is a microkernel, which is at the core of our approach to enabling the design and implementation of better embedded software. It forms the basis of our embedded OS platform which aims to support the development of secure and trustworthy embedded systems. The small size of L4 is the enabler for projects aiming at proving the correctness of the kernel and providing a complete timing model.

Basic Idea

Trustworthiness of a system has a lot to do with its size, even well-engineered code has of the order of several defects per thousand lines of code (loc). Hence, a bigger system has inherently more bugs than a small system.

This is particularly relevant for the kernel, as it is not subject to protection mechanisms. Therefore any kernel bug is potentially fatal for the system — the kernel is always part of the trusted computing base (TCB). Minimising the exposure to faults means minimising the TCB, hence a small kernel. L4 is one of the smallest kernels in existence and is known for its excellent performance, making it an ideal basis for our work.

Work on L4

Most of our past L4 activities were based on L4Ka::Pistachio from the Karlsruhe L4KA Team. We have contributed and were maintaining the ARM, MIPS, Alpha and PowerPC-64 ports, and have dramatically improved the performance of the Itanium port.

The design and implementation of L4Ka::Pistachio are influenced by the desire to achieve a scalable, high-performance platform for desktop and server use. This implied a number of design decisions which make the kernel suboptimal for embedded use. We have therefore created a new specification, called L4-embedded, and a corresponding implementation called NICTA::Pistachio-embedded.

Our embedded version of L4 was successfully commercialised, initially via direct engagement with QUALCOMM and other companies. This lead to spinning out our development team into the new company Open Kernel Labs (OK Labs). OK Labs has further developed L4-embedded into what is now called OKL4, and provides products and services based on this system.

Internally we are now using OKL4 for projects that use the microkernel, such as component architectures and power management. Active research on L4 itself happens mostly in two projects:

seL4 is developing a new L4 API that is suitable for applications with very high security requirements, including provable separation properties. A second objective of the project is to develop a kernel implementation that is suitable for formal verification. This work is based on our experience with the L4-embedded API, and is influenced by Jonathan Shapiro's EROS operating system, and has similar objectives as the L4.sec project at Dresden University of Technology and the Coyotos project.
L4.verified is formalising the seL4 API, and developing a formal proof of the correspondence between that formal model and the actual implementation of the kernel. This will, for the first time, bridge the assertion gap between proofs of security properties of kernel models (as required e.g. by Common Criteria) and the actual code that implements the model.

People

Current

Past

Publications

		Gernot Heiser Hypervisors for consumer electronics Proceedings of the 6th IEEE Consumer Communications and Networking Conference, Las Vegas, NV, USA, January, 2009
		Rafal Kolanski and Gerwin Klein Mapped separation logic Proceedings of VSTTE 2008 — Verified Software: Theories, Tools and Experiments, Toronto, Canada, October, 2008
		David Cock Bitfields and tagged unions in C: verification through automatic generation Proceedings of the 5th International Verification Workshop (VERIFY'08), Sydney, Australia, August, 2008
		David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August, 2008
		Joshua LeVasseur, Volkmar Uhlig, Yaowei Yang, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser Pre-virtualization: soft layering for virtual machines Proceedings of the 13th IEEE Asia-Pacific Computer Systems Architecture Conference, Hsinchu, Taiwan, August, 2008 Best Paper Award!
		Harvey Tuch Formal memory models for verifying C systems code, PhD Thesis, University of NSW, Sydney 2052, Australia, 2008
		Gernot Heiser Trustworthy ⇐ trusted ⇐ proof Proceedings of the 1st Conference on Future of Trust in Computing, Berlin, Germany, July, 2008
		Gernot Heiser The role of virtualization in embedded systems 1st Workshop on Isolation and Integration in Embedded Systems, Glasgow, UK, April, 2008
		Rafal Kolanski A logic for virtual memory Proceedings of the 3rd Workshop on Systems Software Verification 2008, Sydney, Australia, February, 2008
		Harvey Tuch Structured types and separation logic Proceedings of the 3rd Workshop on Systems Software Verification 2008, Sydney, Australia, February, 2008
		Gernot Heiser Do microkernels suck? 9th Linux.Conf.Au, Melbourne, January, 2008
		Gerwin Klein Operating system verification — an overview Sadhana, ?(?), (2008) To appear.
		Gernot Heiser Your system is secure? Prove it! USENIX ;login:, 32(6), 35–38, (December, 2007)
		Kevin Elphinstone, David Greenaway and Sergio Ruocco Lazy scheduling and direct process switch — merit or myths? Proceedings of the 3rd Workshop on Operating System Platforms for Embedded Real-Time Applications, Pisa, Italy, July, 2007 Preliminary version
		Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters Towards trustworthy computing systems: taking microkernels to the next level ACM Operating Systems Review, 41(4), 3–11, (July, 2007)
		Jia Meng, Lawrence C. Paulson and Gerwin Klein A termination checker for Isabelle Hoare logic 4th International Verification Workshop - VERIFY'07, Bremen, Germany, July, 2007
		Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007
		Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser Verifying a high-performance micro-kernel 7th Annual High-Confidence Software and Systems Conference, Baltimore, MD, USA, May, 2007
		Ihor Kuz, Yan Liu, Ian Gorton and Gernot Heiser CAmkES: a component model for secure microkernel-based embedded systems Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems, 80(5), 687–699, (May, 2007) Preprint
		Timothy Roscoe, Kevin Elphinstone and Gernot Heiser Hype and virtue Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007
		Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone A memory allocation model for an embedded microkernel Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007
		Harvey Tuch, Gerwin Klein and Michael Norrish Types, bytes, and separation logic Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, January, 2007
		Carl van Schaik and Gernot Heiser High-performance microkernels and virtualisation on ARM and segmented architectures Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007
		Sergio Ruocco User-Level Fine-Grained Adaptive Real-Time Scheduling via Temporal Reflection Proceedings of the 27th IEEE Real-Time Systems Symposium, Rio De Janeiro, Brazil, December, 2006
		Geoffrey Lee and Charles Gray L4/Darwin: evolving UNIX Conference for Unix, Linux and Open Source Professionals, Melbourne, Vic, Australia, October, 2006 Slides
		Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty Running the manual: an approach to high-assurance microkernel development Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, OR, USA, September, 2006
		Kevin Elphinstone, Gerwin Klein and Rafal Kolanski Formalising a high-performance microkernel Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August, 2006
		Sergio Ruocco Real-Time Programming and L4 Microkernels Proceedings of the 2nd Workshop on Operating System Platforms for Embedded Real-Time Applications, Dresden, Germany, July, 2006
		Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone Kernel data – first class citizens of the system Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January, 2006
		Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur Are virtual-machine monitors microkernels done right? ACM Operating Systems Review, 40(1), 95–99, (January, 2006)
		Rafal Kolanski and Gerwin Klein Formalising the L4 microkernel API Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006
		Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, 30(6), 9–13, (December, 2005)
		Harvey Tuch and Gerwin Klein A unified memory model for pointers Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Montego Bay, Jamaica, December, 2005
		Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco L4cars 3rd Embedded Security in Cars Conference (escar), Cologne, Germany, November, 2005
		Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur Are virtual-machine monitors microkernels done right? Technical Report PA005103, NICTA, October, 2005
		Joshua LeVasseur, Volkmar Uhlig, Matthew Chapman, Peter Chubb, Ben Leslie and Gernot Heiser Pre-virtualization: slashing the cost of virtualization Technical Report PA005520, NICTA, October, 2005
		Harvey Tuch, Gerwin Klein and Gernot Heiser OS verification — now! Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Santa Fe, NM, USA, June, 2005
		Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang and Gernot Heiser Itanium — a system implementor's tale Proceedings of the 2005 Annual USENIX Technical Conference, Anaheim, CA, USA, April, 2005 Best Student Paper Award!
		Ben Leslie, Carl van Schaik and Gernot Heiser Wombat: a portable user-mode Linux for embedded systems Proceedings of the 6th Linux.Conf.Au, Canberra, April, 2005
		Rafal Kolanski A formal model of the L4 micro-kernel API using the B method Technical Report Technical Report 05-00029-1, National ICT Australia, 2005
		Kevin Elphinstone Future directions in the evolution of the L4 microkernel Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004
		Harvey Tuch and Gerwin Klein Verifying the L4 virtual memory subsystem Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October, 2004
		Kevin Elphinstone and Stefan Goetz Initial evaluation of a user-level device driver framework Proceedings of the 9th Asia-Pacific Computer Systems Architecture Conference, Beijing, China, September, 2004
		Gerwin Klein and Harvey Tuch Towards verified virtual memory in L4 TPHOLs Emerging Trends '04, Park City, Utah, USA, September, 2004
		Ihor Kuz L4 user manual — API version X.2 June, 2004
		Andreas Haeberlen and Kevin Elphinstone User-level management of kernel memory Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
		Christan Szmajda and Gernot Heiser Generalised radix page table: a page table for modern architectures Proceedings of the 8th Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
		Shane Stephens and Gernot Heiser Fault tolerance and avoidance in biomedical systems Proceedings of the 10th SIGOPS European Workshop, St Emilion, France, September, 2002
		Daniel Potts, Simon Winwood and Gernot Heiser Design and implementation of the L4 microkernel for Alpha multiprocessors Technical Report UNSW-CSE-TR-0201, School of Computer Science and Engineering, February, 2002
		Volkmar Uhlig, Uwe Dannowski, Espen Skoglund, Andreas Haeberlen and Gernot Heiser Performance of address-space multiplexing on the pentium Technical Report 2002-1, Computer Science Department, University of Karlsruhe, 2002
		Gernot Heiser Dealing with TLB tags 2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001
		Cristan Szmajda Calypso: a portable translation layer 2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001
		Daniel Potts, Simon Winwood and Gernot Heiser L4 reference manual: Alpha 21x64 Technical Report UNSW-CSE-TR-0104, School of Computer Science and Engineering, March, 2001
		Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller The SawMill framework for VM diversity Proceedings of the 6th Australasian Computer Systems Architecture Conference, Gold Coast, Australia, January, 2001
		Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin J. Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther The Sawmill multiserver approach Proceedings of the 9th SIGOPS European Workshop, Kolding, Denmark, 2000
		Kevin Elphinstone Virtual memory in a 64-bit microkernel, PhD Thesis, University of NSW, Sydney 2052, Australia, 1999
		Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Proceedings of the 4th Australasian Computer Architecture Conference, Auckland, New Zealand, January, 1999
		Kevin Elphinstone, Gernot Heiser and Jochen Liedtke Page tables for 64-bit computer systems Technical Report UNSW-CSE-TR-9804, School of Computer Science and Engineering, August, 1998
		Alan Au and Gernot Heiser L4 User Manual — version 1.0 Technical Report UNSW-CSE-TR-9801, School of Computer Science and Engineering, April, 1998
		Kevin Elphinstone, Gernot Heiser and Jochen Liedtke L4 reference manual – MIPS R4x00 — Version 1.0 Technical Report UNSW-CSE-TR-9709, School of Computer Science and Engineering, December, 1997
		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) Proceedings of the 6th Workshop on Hot Topics in Operating Systems, Cape Cod, MA, USA, May, 1997
		Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke Supporting persistent object systems in a single address space Proceedings of the 7th International Workshop on Persistent Object Systems, Cape May, NJ, USA, May, 1996
		Jochen Liedtke and Kevin Elphinstone Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization Technical Report UNSW-CSE-TR-9503, School of Computer Science and Engineering, November, 1995

Return Home