Skip to main content

The seL4 microkernel

seL4 key logo

seL4, the secure embedded L4 microkernel, is a key element of our research program. We developed seL4 to provide a reliable, secure, fast and verified foundation for building trustworthy systems.

seL4 enforces security within componentised system architectures by ensuring isolation between trusted and untrusted system components, and by carefully controlling software access to hardware devices in the system.

As a microkernel, seL4 contains only about 12,000 lines of C code plus some assembly code. This minimises the trusted computing base, and has enabled us to verify seL4's functional correctness and security properties using rigorous mathematical proof.

Why seL4?

seL4 is the world’s fastest operating system kernel designed for security and safety, and has been deployed in several real-world projects. It runs on a variety of hardware platforms, including x86, x86-64 and ARM, with a port to RISC-V in progress. seL4 can also run virtual machines to support legacy software.

seL4-based systems have flown a helicopter and have handled classified military information. An earlier variant, OKL4, has been deployed in over two billion phones.

seL4 is also the foundation for most of our current research in operating systems, and the seL4 verification project hosts much of our research on formal methods for software verification. In turn, our advancements in real-time OS design, covert channel mitigation, hardware fault resiliency and other areas are eventually incorporated back into seL4 itself.

Developing on seL4

seL4 is open source and freely available on GitHub. Comprehensive libraries, documentation and tutorials are also available on its website, seL4.systems.

We continue to develop seL4, providing regular releases of verified new features to the user community. See our development roadmap.

We have complemented seL4 with an ecosystem of freely available tools for componentised software architectures, enabling the user community to build large scale software applications on top of the high-assurance environment that it provides.

Technical information

seL4 is a third-generation microkernel that builds on the strengths of the L4 microkernel design. Our documentation site has technical information about the design, implementation and interface of seL4 for software developers, and our publications below provide information for researchers.

We also have historical technical notes that explain seL4's initial design, implementation and verification.

RTOS

The seL4 kernel is targeted at hardware that supports memory protection, which enables strong isolation functionality. More constrained hardware, such as small micro-controllers without memory protection can still benefit from high-assurance real-time operating systems, for instance in the eChronos project.

People

Current

Past

  • Adrian Danis
  • Bernard Blackham
  • David Cock
  • Matthew Fernandez
  • Michael von Tessin

Publications

Abstract PDF Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
Abstract
Slides
PDF Simon Biggs, Damon Lee and Gernot Heiser
The jury is in: Monolithic OS design is flawed
Asia-Pacific Workshop on Systems (APSys), Korea, August, 2018
Abstract PDF Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser
Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time
EuroSys Conference, Porto, Portugal, April, 2018
Abstract Slides
Video
Gernot Heiser
Flying autonomous aircraft: Mixed-criticality support in seL4
at linux.conf.au, Sydney, January, 2018
Abstract PDF Anna Lyons
Mixed-criticality scheduling and resource sharing for high-assurance operating systems
PhD Thesis, UNSW, 2018
Abstract PDF Darren Cofer, John Backes, Andrew Gacek, Daniel DaCosta, Michael Whalen, Ihor Kuz, Gerwin Klein, Gernot Heiser, Lee Pike, Adam Foltzer, Michael Podhradsky, Douglas Stuart, Jason Graham and Brett Wilson
Secure mathematically-assured composition of control models
Technical Report, Data61, CSIRO, September, 2017
Abstract PDF Kevin Elphinstone, Amirreza Zarrabi, Kent Mcleod and Gernot Heiser
A performance evaluation of rump kernels as a multi-server OS building block on seL4
Asia-Pacific Workshop on Systems (APSys), India, September, 2017
Abstract PDF Thomas Sewell
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, 2017
Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract
Slides
PDF Anna Lyons and Gernot Heiser
Mixed-criticality support in a high-assurance, general-purpose microkernel
Workshop on Mixed Criticality Systems, pp. 9–14, Rome, Italy, December, 2014
Abstract PDF Matthias Daum, Nelson Billing and Gerwin Klein
Concerned with the unprivileged: User programs in kernel refinement
Formal Aspects of Computing, Volume 26, Number 6, pp. 1205–1229, October, 2014
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
Abstract PDF Michael von Tessin
The clustered multikernel: An approach to formal verification of multiprocessor operating-system kernels
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, December, 2013
Abstract
Slides
PDF
Presentation Video
Kevin Elphinstone and Gernot Heiser
From L3 to seL4 – what have we learnt in 20 years of L4 microkernels?
ACM Symposium on Operating Systems Principles, pp. 133–150, Farmington, PA, USA, November, 2013
Abstract PDF Bernard Blackham
Towards verified microkernels for real-time mixed-criticality systems
PhD Thesis, UNSW, Sydney, Australia, October, 2013
2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Correct, fast, maintainable — choose any three!
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract
Slides
PDF Bernard Blackham, Vernon Tang and Gernot Heiser
To preempt or not to preempt, that is the question
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
Abstract
Slides
PDF Bernard Blackham, Yao Shi and Gernot Heiser
Improving interrupt response time in a verifiable protected microkernel
EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012
Abstract PDF Michael von Tessin
The clustered multikernel: An approach to formal verification of multiprocessor OS kernels
2nd Workshop on Systems for Future Multi-core Architectures, pp. 1–6, Bern, Switzerland, April, 2012
Abstract PDF Gernot Heiser, Toby Murray and Gerwin Klein
It's time for trustworthy systems
IEEE Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012
Abstract PDF Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser
Timing analysis of a protected operating system kernel
IEEE Real-Time Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011
Abstract PDF Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
seL4 enforces integrity
International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
Abstract PDF Bernard Blackham, Yao Shi and Gernot Heiser
Protected hard real-time: The next frontier
Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011
Abstract
Slides
PDF Gernot Heiser, Leonid Ryzhyk, Michael von Tessin and Aleksander Budzynowski
What if you could actually Trust your kernel?
Workshop on Hot Topics in Operating Systems, pp. 1–5, Napa, CA, USA, May, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Workshop on Hot Topics in Operating Systems, pp. 5, Napa, USA, May, 2011
Abstract PDF Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker
capDL: A language for describing capability-based systems
Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010
Abstract PDF Michael von Tessin
Towards high-assurance multiprocessor virtualisation
6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an operating-system kernel
Communications of the ACM, Volume 53, Number 6, pp. 107–115, June, 2010
Research Highlights paper
Abstract PDF Dhammika Elkaduwe
A principled approach to kernel memory management
PhD Thesis, UNSW, Sydney, Australia, May, 2010
Abstract
Slides
PDF
Presentation Video
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
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Abstract PDF
Presentation Video
Gerwin Klein, Philip Derrin and Kevin Elphinstone
Experience report: seL4 — formally verifying a high-performance microkernel
Proceedings of the 14th International Conference on Functional Programming, pp. 91–96, Edinburgh, UK, August, 2009
Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
Abstract PDF Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser
Towards a practical, verified kernel
Workshop on Hot Topics in Operating Systems, pp. 6, San Diego, CA, USA, May, 2007
Abstract PDF 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
Abstract PDF Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone
A memory allocation model for an embedded microkernel
International Workshop on Microkernels for Embedded Systems, pp. 28–34, Sydney, Australia, January, 2007
Abstract PDF 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
Abstract PDF Kevin Elphinstone, Gerwin Klein and Rafal Kolanski
Formalising a high-performance microkernel
Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), pp. 1-7, Seattle, USA, August, 2006
Abstract PDF 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 , pp. 39–43, Victor Harbor, South Australia, Australia, January, 2006
Abstract PDF Gernot Heiser
Secure embedded systems need microkernels
USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 2005
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
Served by Apache on Linux on seL4.