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.

seL4 can be downloaded by following the instructions at http://sel4.systems/Download

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 TS 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

seL4, its proofs, as well as userspace libraries and tools are open-source software and can be accessed from http://seL4.systems.

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

		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
		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
		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
		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
		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
		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 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, 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, 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
		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 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, 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 Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), 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