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.
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, Arm and RISC-V. 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.
seL4 is open source and freely available on GitHub. It is now under the stewardship of the seL4 Foundation. Comprehensive libraries, documentation and tutorials are also available on its website, seL4.systems.
We continue to develop seL4 in close collaboration with our partners in the seL4 Foundation, including 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.
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.
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.
Current |
Past
|
|
 |
Mathieu Paturel, Isitha Subasinghe and Gernot Heiser First steps in verifying the seL4 Core Platform Asia-Pacific Workshop on Systems (APSys), Seoul, KR, August, 2023 |
|
|
 
|
Gernot Heiser seL4 update: Foundation and TS R&D news Invited talk at the Trusted Computing Center of Excellence 2023 Summit, May, 2023 |
|
|
|
Jason Belt, John Hatcliff, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren Cofer, David Hardin, Karl Hoech, Konrad Slind, Ihor Kuz and Kent Mcleod Model-driven development for the seL4 microkernel using the HAMR framework Journal of Systems Architecture, Volume 134, pp. 102789, 2023 |
|
|
|
Gernot Heiser State of seL4-related research Keynote at the seL4 Summit, October, 2022 |
|
|
|
Gernot Heiser seL4 overview: Principles, abstractions, use Invited talk at the seL4 Summit, October, 2022 |
|
|
|
Lucy Parker The seL4 device driver framework Talk at the seL4 2022 Summit, October, 2022 |
|
|
|
Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer and John Shackleton Cyberassured systems engineering at scale IEEE Security and Privacy, Volume 20, Number 3, pp. 52–64, March, 2022 |
|
|
|
Gernot Heiser The seL4 report: State of the seL4 ecosystem Keynote at the Trusted Computing Center of Excellence 2022 Summit, February, 2022 |
|
|
|
Gernot Heiser The seL4 Foundation – growing through upheaval On-line, January, 2022 |
|
|
|
Gernot Heiser The formally verified seL4 microkernel – a high-assurance foundation for MCS Keynote at IEEE Conference on Embedded and Real-Time Computing and Applications, August, 2020 |
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein Towards provable timing-channel prevention ACM Operating Systems Review, Volume 54, Issue 1, pp. 1-7, August, 2020 |
|
|
|
Nils Wistoff, Moritz Schneider, Frank Gürkaynak, Luca Benini and Gernot Heiser Prevention of microarchitectural covert channels on an open-source 64-bit RISC-V core Workshop on Computer Architecture Research with RISC-V (CARRV), Valencia, Spain, May, 2020 |
|
|
|
Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020 |
|
|
|
Gernot Heiser Verified seL4 on secure RISC-V processors at linux.conf.au, Gold Coast, January, 2020 |
|
|
|
Yanyan Shen, Gernot Heiser and Kevin Elphinstone Fault tolerance through redundant execution on COTS multicores: Exploring trade-offs International Conference on Dependable Systems and Networks (DSN), pp. 188-200, Portland, Oregon, USA, June, 2019 |
|
|
|
Gernot Heiser, Gerwin Klein and Toby Murray Can we prove time protection? Workshop on Hot Topics in Operating Systems (HotOS), pp. 23-29, Bertinoro, Italy, May, 2019 |
|
|
|
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser Time protection: The missing OS abstraction EuroSys Conference, Dresden, Germany, March, 2019 Best Paper Award |
|
|
|
Yanyan Shen Microkernel mechanisms for improving the trustworthiness of commodity hardware PhD Thesis, UNSW, Sydney, Australia, March, 2019 |
|
|
|
Gernot Heiser What's new in the world of seL4? Talk at FOSDEM'19, Brussels, February, 2019 |
|
|
|
Darren Cofer, Andrew Gacek, John Backes, Michael Whalen, Lee Pike, Adam Foltzer, Michael Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser and Douglas Stuart A formal approach to constructing secure air vehicle software IEEE Computer, Volume 51, Issue 11, pp. 14-23, November, 2018 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser The quest for the perfect API Invited "Fireside Talk" at VMware on occasion of the virtualisation pioneer's 20th anniversary, April, 2018 |
|
|
|
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 |
|
|
|
Gernot Heiser Flying autonomous aircraft: Mixed-criticality support in seL4 at linux.conf.au, Sydney, January, 2018 |
|
|
|
Anna Lyons Mixed-criticality scheduling and resource sharing for high-assurance operating systems PhD Thesis, UNSW, 2018 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, 2017 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Sean Peters, Adrian Danis, Kevin Elphinstone and Gernot Heiser For a microkernel, a big lock is fine Asia-Pacific Workshop on Systems (APSys), Tokyo, JP, July, 2015 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013 |
|
|
|
Bernard Blackham and Gernot Heiser Correct, fast, maintainable — choose any three! Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
Gernot Heiser, Toby Murray and Gerwin Klein It's time for trustworthy systems IEEE Symposium on Security and Privacy, Volume 10, Number 2, pp. 67–70, March, 2012 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 |
|
|
|
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 (HotOS), pp. 1–5, Napa, CA, USA, May, 2011 |
|
|
|
Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood Provable security: How feasible is it? Workshop on Hot Topics in Operating Systems (HotOS), pp. 5, Napa, USA, May, 2011 |
|
|
|
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 |
|
|
|
Michael von Tessin Towards high-assurance multiprocessor virtualisation 6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010 |
|
|
|
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 |
|
|
|
Dhammika Elkaduwe A principled approach to kernel memory management PhD Thesis, UNSW, Sydney, Australia, May, 2010 |
|
|
|
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 Best Paper Award Hall of Fame Award |
|
|
|
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 |
|
|
|
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, Volume 41, Number 4, pp. 3–11, December, 2007 |
|
|
|
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser Towards a practical, verified kernel Workshop on Hot Topics in Operating Systems (HotOS), pp. 6, 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 |
|
|
|
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 |
|
|
|
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 Verified Software: Theories, Tools and Experiments, pp. 1-7, Seattle, USA, August, 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 , pp. 39–43, Victor Harbor, South Australia, Australia, January, 2006 |
|
|
|
Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, Volume 30, Number 6, pp. 9–13, December, 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 |