Trustworthy Systems

UNSW Sydney
 
 
 
Our Partners University of Karlsruhe

The L4 Microkernel

The L4 microkernel provides a minimal and efficient basis for constructing operating system software for a broad range of systems from single-purpose embedded devices to multi-processor servers.

Prior to the commencement of the seL4 project, most of our 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.

Publications

2009

Abstract PDF Joshua LeVasseur
Device-driver reuse via virtual machines
PhD Thesis, UNSW, Sydney, Australia, May, 2009

2008

Abstract PDF
Presentation Video
Gernot Heiser
Do microkernels suck?
Other Conference Presentation, Linux.conf.au, Melbourne, Australia, January, 2008.

2007

plain text to be published Gernot Heiser
Virtualisation for embedded systems
Technical Report, Open Kernel Labs, November, 2007
Abstract link 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, Volume 80, Number 5, pp. 687–699, May, 2007
Preprint
Abstract PDF Carl van Schaik and Gernot Heiser
High-performance microkernels and virtualisation on ARM and segmented architectures
International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007

2006

Abstract PDF Sergio Ruocco
User-level fine-grained adaptive real-time scheduling via temporal reflection
IEEE Real-Time Systems Symposium, Rio De Janeiro, Brazil, December, 2006
Abstract PDF Geoffrey Lee and Charles Gray
L4/Darwin: Evolving UNIX
Conference for Unix, Linux and Open Source Professionals (AUUG), Melbourne, Vic, Australia, October, 2006
Slides
Abstract PDF Sergio Ruocco
Real-Time Programming and L4 Microkernels
Workshop on Operating System Platforms for Embedded Real-Time Applications (OSPERT), Dresden, DE, July, 2006
Abstract PDF Gernot Heiser, Volkmar Uhlig and Joshua LeVasseur
Are virtual-machine monitors microkernels done right?
ACM Operating Systems Review, Volume 40, Number 1, pp. 95–99, January, 2006

2005

Abstract PDF Gernot Heiser
Secure embedded systems need microkernels
USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 2005
Abstract PDF Harvey Tuch and Gerwin Klein
A unified memory model for pointers
International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 474–488, Montego Bay, Jamaica, December, 2005
Abstract PDF Kevin Elphinstone, Gernot Heiser, Ralf Huuck, Stefan M. Petters and Sergio Ruocco
L4cars
Embedded Security in Cars Conference (escar), Cologne, DE, November, 2005
Abstract PDF 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
Abstract PDF Harvey Tuch, Gerwin Klein and Gernot Heiser
OS verification — now!
Workshop on Hot Topics in Operating Systems (HotOS), pp. 7–12, Santa Fe, NM, USA, June, 2005
Abstract PDF Charles Gray, Matthew Chapman, Peter Chubb, David Mosberger-Tang and Gernot Heiser
Itanium — a system implementor's tale
USENIX, pp. 264–278, Anaheim, CA, USA, April, 2005
Best Student Paper Award
Abstract PDF Ben Leslie, Carl van Schaik and Gernot Heiser
Wombat: A portable user-mode Linux for embedded systems
Linux.conf.au, Canberra, April, 2005
Abstract PDF 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

2004

Abstract PDF 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
Abstract PDF Harvey Tuch and Gerwin Klein
Verifying the L4 virtual memory subsystem
Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, pp. 73–97, Sydney, Australia, October, 2004
Abstract PDF Kevin Elphinstone and Stefan Götz
Initial evaluation of a user-level device driver framework
Asia-Pacific Computer Systems Architecture Conference, Beijing, China, September, 2004
Abstract PDF Gerwin Klein and Harvey Tuch
Towards verified virtual memory in L4
TPHOLs Emerging Trends '04, pp. 16 pages, Park City, Utah, USA, September, 2004
Abstract PDF Ihor Kuz
L4 user manual — API version X.2
June, 2004

2003

Abstract PDF Andreas Haeberlen and Kevin Elphinstone
User-level management of kernel memory
Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003
Abstract PDF Chris Szmajda and Gernot Heiser
Generalised radix page table: A page table for modern architectures
Asia-Pacific Computer Systems Architecture Conference, pp. 290-304, Aizu-Wakamatsu City, Japan, September, 2003
Abstract PDF Adam Wiggins, Harvey Tuch, Volkmar Uhlig and Gernot Heiser
Implementation of fast address-space switching and TLB sharing on the StrongARM processor
Asia-Pacific Computer Systems Architecture Conference, Aizu-Wakamatsu City, Japan, September, 2003

2002

Abstract PDF Shane Stephens and Gernot Heiser
Fault tolerance and avoidance in biomedical systems
SIGOPS European Workshop, St Emilion, France, September, 2002
Abstract PDF 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
Abstract PDF 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

2001

Abstract PDF Gernot Heiser
Dealing with TLB tags
2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PDF Chris Szmajda
Calypso: A portable translation layer
2nd Workshop on Microkernels and Microkernel-based Systems, Lake Louise, Alta, Canada, October, 2001
Abstract PDF 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
Abstract PDF Mohit Aron, Yoonho Park, Trent Jaeger, Jochen Liedtke, Kevin Elphinstone and Luke Deller
The SawMill framework for VM diversity
Asia-Pacific Computer Systems Architecture Conference, pp. 3–10, Gold Coast, Australia, January, 2001

2000

Abstract PDF Alain Gefflaut, Trent Jaeger, Yoonho Park, Jochen Liedtke, Kevin Elphinstone, Volkmar Uhlig, Jonathon E. Tidswell, Luke Deller and Lars Reuther
The Sawmill multiserver approach
SIGOPS European Workshop, pp. 109–114, Kolding, Denmark, 2000

1999

Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
L4 reference manual: MIPS R4x00, version 1.11, kernel version 79
Sydney, Australia, May, 1999
Abstract PDF Kevin Elphinstone
Virtual memory in a 64-bit microkernel
PhD Thesis, UNSW, Sydney, Australia, March, 1999
Abstract PDF Trent Jaeger, Kevin Elphinstone, Jochen Liedtke, Vsevolod Panteleenko and Yoonho Park
Flexible access control using IPC redirection
Workshop on Hot Topics in Operating Systems (HotOS), pp. 191–196, Rio Rico, AZ, USA, March, 1999
Abstract PDF Kevin Elphinstone, Gernot Heiser and Jochen Liedtke
Page tables for 64-bit computer systems
Australasian Computer Architecture Conference, pp. 211-226, Auckland, New Zealand, January, 1999

1998

Abstract PDF 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
Abstract PDF 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

1997

Abstract PDF 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
Abstract PDF 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)
Workshop on Hot Topics in Operating Systems (HotOS), pp. 28–31, Cape Cod, MA, USA, May, 1997

1996

Abstract PDF Kevin Elphinstone, Stephen Russell, Gernot Heiser and Jochen Liedtke
Supporting persistent object systems in a single address space
International Workshop on Persistent Object Systems (POS), pp. 111–119, Cape May, NJ, USA, May, 1996
Abstract PDF Jochen Liedtke and Kevin Elphinstone
Guarded page tables on MIPS R4600 or an exercise in architecture-dependent micro optimization
ACM Operating Systems Review, Volume 30, Number 1, pp. 4–15, January, 1996

1995

Abstract PDF 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