Our Partners
Develop a highly robust, high-performance software stack that leverages the isolation guarantees of seL4 and aids its deployment. The stack should lend itself to formal verification without compromising performance, but even unverified will enable building highly robust systems for real-world ues.
The seL4 microkernel is unrivalled in both its assurance as well as performance. However, its API is inherently very low-level and hard to use, it lacks the functionality expected from an operating system, and is difficult to integrate into other projects.
We are addressing this by developing a software stack, aimed primarily at embedded and cyberphysical systems, that is easy to deploy by industry, provides a straightforward path to adding system services, without compromising performance.
We are designing a set of building blocks that naturally lead to correct, secure and performant use of the underlying seL4 kernel and its features. The idea is that you don't have to be an seL4, mikrokernel or formal-methods expert in order to build a robust and performant system. This means on the one hand that the design of the stack must lend itself to a highly robust and low-overhead implementation, and on the other hand must make it straightforward to use the basic building blocks we provide to build a good system.
Core to this approach are simple, clean and lean designs that can be well optimised, use seL4 to the best effect, and provide templates for proper use and extension of functionality. At the same time, we want our stack itself to be verified eventually, so design for verifiability is a core consideration. Together, these desired features pose significant systems research challenges.
The following sub-projects presently form part of the work on the robust software stack:
Current |
Past
|
|
|
Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus Myreen, Michael Norrish and Gernot Heiser Pancake: verified systems programming made sweeter Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023 |
|
 |
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, Lucy Parker, Ivan Velickovic, Peter Chubb and Ben Leslie Can we put the "S" into IoT? IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022 |
|
|
|
Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu Automatic verification of active device drivers ACM Operating Systems Review, Volume 48, Number 1, May, 2014 |
|
|
|
Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser The case for active device drivers Asia-Pacific Workshop on Systems (APSys), pp. 25–30, New Delhi, India, August, 2010 |
|
|
|
Leonid Ryzhyk On the construction of reliable device drivers PhD Thesis, UNSW, Sydney, Australia, January, 2010 |
|
|
|
Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser Automatic device driver synthesis with Termite ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009 |