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.
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. 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 for our work. The seL4 project has 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 personal digital assistants, mobile phones, and set-top boxes.
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 mobile phones, personal digital assistants, and set-top boxes. 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 unknowingly installed by end users.
The susceptibility to viruses, trojan horses, ad-ware, and spyware of modern desktop platforms is largely due 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, we have a strong collaboration with the NICTA Formal Methods and Logic and Computation groups in the form of the L4.verified project. A high degree of assurance can ultimately only be established by mathematical rigour.The collaboration 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.
The practical result of our work is the most trustworthy general purpose microkernel in the world.
Technical Information
Further technical details of the project are available here.
Availability
Binaries of seL4 on ARM and x86 architectures are available for academic research and education use. The release additionally contains the seL4 formal specification, user-level libraries and sample code, and a para-virtualised Linux (x86)
People
Current |
Past |
Publications
|
 |
Bernard Blackham, Yao Shi and Gernot Heiser Improving interrupt response time in a verifiable protected microkernel Proceedings of the 7th EuroSys Conference, Bern, Switzerland, April, 2012 |
|
 |
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, Vienna, Austria, November, 2011 |
|
|
|
Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein seL4 enforces integrity 2nd International Conference on Interactive Theorem Proving, Nijmegen, The Netherlands, August, 2011 |
|
|
|
Bernard Blackham, Yao Shi and Gernot Heiser Protected hard real-time: The next frontier Proceedings of the 2nd Asia-Pacific Workshop on Systems, Shanghai, China, July, 2011 |
|
|
|
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 |
|
|
|
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, Napa, CA, USA, May, 2011 |
|
|
|
June Andronick, David Greenaway and Kevin Elphinstone Towards proving security in the presence of large untrusted components Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010 |
|
|
|
David Cock Lyrebird – assigning meanings to machines Proceedings of the 5th Workshop on Systems Software Verification, Vancouver, Canada, October, 2010 |
|
|
|
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, Chicago, IL, USA, October, 2010 Invited paper |
|
|
|
Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Walker capDL: A language for describing capability-based systems Proceedings of the 1st Asia-Pacific Workshop on Systems, New Delhi, India, August, 2010 |
|
|
|
Michael von Tessin Towards high-assurance multiprocessor virtualisation Proceedings of the 6th International Verification Workshop, Edinburgh, UK, July, 2010 |
|
|
|
June Andronick From a proven correct microkernel to trustworthy large systems International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Paris, France, June, 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, 53(6), 107–115, (June, 2010) |
|
|
|
Dhammika Elkaduwe A principled approach to kernel memory management, PhD Thesis, School of Computer Science and Engineering, University of NSW, Sydney 2052, Australia, 2010 |
|
|
|
Gerwin Klein, Thomas Sewell and Simon Winwood Refinement in the formal verification of sel4 Springer-Verlag, March, 2010 |
|
|
|
Gerwin Klein Correct OS kernel? Proof? Done! USENIX ;login:, 34(6), 28–34, (December, 2009) |
|
|
|
Andrew Boyton A verified shared capability model Proceedings of the 4th Workshop on Systems Software Verification, Aachen, Germany, October, 2009 |
|
|
 |
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 Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009 Best Paper 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, Edinburgh, UK, August, 2009 |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Proceedings of Verified Software: Theories, Tools and Experiments 2008, Toronto, Canada, October, 2008 |
|
|
|
David Cock, Gerwin Klein and Thomas Sewell Secure microkernels, state monads and scalable refinement Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, Montreal, Canada, August, 2008 |
|
|
|
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, Glasgow, UK, April, 2008 |
|
|
|
Gernot Heiser Your system is secure? Prove it! USENIX ;login:, 32(6), 35–38, (December, 2007) |
|
|
|
Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone Verified protection model of the seL4 microkernel Technical Report NRL-1474, NICTA, October, 2007 |
|
|
|
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, 41(4), 3–11, (July, 2007) |
|
|
|
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, 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 Proceedings of the 1st International Workshop on Microkernels for Embedded Systems, 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), 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 , Victor Harbor, South Australia, Australia, January, 2006 |
|
|
|
Gernot Heiser Secure embedded systems need microkernels USENIX ;login:, 30(6), 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 |