The University of New South Wales

Secure Microkernel Project (seL4)

The seL4 microkernel is a key enabler of our work. It provides a minimal and efficient lowest software level, and is the only part of our software that executes in the privileged mode of the hardware. It is a third-generation microkernel that builds on the strengths of the L4 microkernel architecture, such as small size, high performance, and policy freedom, and extends it with a built-in capability model, which provides a mechanism to enforce security guarantees at the operating system and application levels.

Click here to download seL4

Why microkernel?

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 manages the hardware at the lowest level, and it is not subject to protection or fault isolation mechanisms provided by the hardware — in fact, it is responsible for controlling the hardware 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 general purpose kernels in existence and is known for its excellent performance, making it an ideal original starting point for build a trustworthy software foundation. The seL4 project extended L4's applicability to application domains requiring strong security guarantees, and also made it more amenable to formal verification of correctness.

Overview of seL4

Strong security is a fundamental requirement for some existing and emerging embedded application domains and devices, such as smartphones, cyber military systems, medical devices, and unmanned aerial vehicles.

It is widely acknowledged that to build a secure system, security must be considered in all layers of the system—from hardware to software applications. It is also widely acknowledged that it is extremely difficult (if not impossible) to retrofit security mechanisms to an existing insecure system. Security is becoming a critical component of new embedded devices, such as smartphones and automotive consoles. There is an expectation from users and service providers that such devices will store sensitive data owned by either party, i.e., data that either party wishes to control access to and dissemination of. Such devices are also expected to run third-party applications whose origin, quality and functionality is not directly or even indirectly controlled by the embedded-device supplier. Given that end-users are unlikely to be able or willing to identify applications of dubious nature (or outright malicious intent), any secure embedded system must be capable of enforcing security requirements between application instances on an individual device, in an environment where hostile applications are present.

The susceptibility to viruses, trojan horses, ad-ware, and spyware of modern desktop platforms can be attributed to the inability of the underlying base system to apply and enforce the principle of least authority, which undermines the ability of higher-level layers to provide security. The inability of users to finely control their own software results in uncontrolled propagation of viruses, the disclosure or modification of private data, or denial of service to the user. Attempts to secure platforms via various scanners, fire walls, and integrity checkers have been of only limited success, and largely unsatisfactory if one requires strong guarantees regarding control of their data.

seL4 provides the secure software base upon which further secure software layers (system and application services) can be composed to form a trustworthy embedded system. The system could be as simple as an industrial controller needing isolation between two activities it manages, or as complex as virtualisation infrastructure requiring strong isolation between the virtual machines it provides to clients. Both scenarios rely on the guarantees provided by the underlying kernel.

To provide a high degree of assurance of the guarantees, a successful collaboration with NICTA's Formal Methods team in the form of the L4.verified project, has resulted in the formal modelling of the kernel's programming interface, and the formal verification of the implementation of the modelled interface. The mathematical proof covers not only the design at differing levels of depth, but also the implementation of the design down to the programming language level.

Thus the extremely high degree of assurance provided by seL4 is from sound and complete mathematical rigour (not potentially in-exhaustive testing). The practical result of our work is the most trustworthy general purpose microkernel in the world.

seL4 is now a foundation of continuing work at SSRG that aims to extend the guarantees provided by the kernel by proving further security and safety properties, enabling construction of systems on seL4 that retain security and safety guarantees of the kernel, and extending the kernel to tackle new problem domains (e.g. real-time scheduling). See the Trustworthy Systems Project for an overview of our current activities.

Technical Information

Further technical details of the project are available here.

Availability

http://seL4.systems has teh latest news on seL4 availability. Binaries of seL4 are avauilable now for non-commercial use, see the download page.

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

Publications

Abstract to be published Matthias Daum, Nelson Billing and Gerwin Klein
Concerned with the unprivileged: User programs in kernel refinement
Formal Aspects of Computing
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
CORE John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation
ACM SIGBED Paul Caspi Memorial Dissertation Award
Abstract
Slides
PDF Bernard Blackham and Gernot Heiser
Correct, fast, maintainable – choose any three!
Proceedings of the 3rd Asia-Pacific Workshop on Systems (APSys), pp. 13:1–13: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
Proceedings of the 3rd Asia-Pacific Workshop on Systems (APSys), pp. 8:1–8:7, Seoul, Korea, July, 2012
Abstract
Slides
PDF Bernard Blackham, Yao Shi and Gernot Heiser
Improving interrupt response time in a verifiable protected microkernel
Proceedings of the 7th EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012
Abstract
Slides
PDF Michael von Tessin
The clustered multikernel: An approach to formal verification of multiprocessor OS kernels
Proceedings of the 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 2012, Number 2, pp. 67–70, March, 2012
Abstract
Slides
PDF Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser
Timing analysis of a protected operating system kernel
Proceedings of the 32nd 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
Proceedings of the 2nd International Conference on Interactive Theorem Proving, pp. 325–340, Nijmegen, The Netherlands, August, 2011
Abstract
Slides
PDF Bernard Blackham, Yao Shi and Gernot Heiser
Protected hard real-time: The next frontier
Proceedings of the 2nd Asia-Pacific Workshop on Systems (APSys), pp. 1:1–1: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?
Proceedings of the 13th Workshop on Hot Topics in Operating Systems, Napa, CA, USA, May, 2011
Abstract PDF Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood
Provable security: How feasible is it?
Proceedings of the 13th Workshop on Hot Topics in Operating Systems, pp. 28–32, Napa, CA, USA, May, 2011
Abstract PDF June Andronick, David Greenaway and Kevin Elphinstone
Towards proving security in the presence of large untrusted components
Proceedings of the 5th Systems Software Verification, Vancouver, Canada, October, 2010
Abstract PDF David Cock
Lyrebird – assigning meanings to machines
Proceedings of the 5th Systems Software Verification, pp. 1–9, Vancouver, Canada, October, 2010
Abstract PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
Proceedings of the 5th ACM Workshop on Scalable Trusted Computing (ACMSTC), pp. 3–9, Chicago, IL, USA, October, 2010
Invited paper
Abstract PDF Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker
capDL: A language for describing capability-based systems
Proceedings of the 1st Asia-Pacific Workshop on Systems (APSys), pp. 31–36, New Delhi, India, August, 2010
Abstract
Slides
PDF Michael von Tessin
Towards high-assurance multiprocessor virtualisation
Proceedings of the 6th International Verification Workshop, pp. 110–125, Edinburgh, UK, July, 2010
Abstract PDF June Andronick
From a proven correct microkernel to trustworthy large systems
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), pp. 1–9, Paris, France, June, 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 PDF Gerwin Klein
Correct OS kernel? Proof? Done!
USENIX ;login:, Volume 34, Number 6, pp. 28–34, December, 2009
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
Best Paper Award!
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 Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Proceedings of Verified Software: Theories, Tools and Experiments 2008, pp. 99–114, Toronto, Canada, October, 2008
Abstract PDF Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone
Kernel design for isolation and assurance of physical memory
1st Workshop on Isolation and Integration in Embedded Systems, pp. 35-40, Glasgow, UK, April, 2008
Abstract PDF Gernot Heiser
Your system is secure? Prove it!
USENIX ;login:, Volume 32, Number 6, pp. 35–38, December, 2007
Abstract PDF Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone
Verified protection model of the seL4 microkernel
Technical Report NRL-1474, NICTA, October, 2007
Abstract PDF 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, July, 2007
Abstract PDF 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, pp. 117–122, 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
Proceedings of the 1st International Workshop on Microkernels for Embedded Systems (MIKES), 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