Trustworthy Systems

UNSW Sydney
 
 
 
Our Partners The seL4 Foundation Breakaway Consulting

seL4-Based Robust Software Stack

Security is No Excuse for Bad Performance!

Aim

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.

Problem

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.

Solution

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.

Approach

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.

Building blocks

The following sub-projects presently form part of the work on the robust software stack:



Contact

People

Current

Past


Publications

plain text to be published 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
Abstract PDF 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
Abstract
Slides
PDF
Presentation Video
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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Leonid Ryzhyk
On the construction of reliable device drivers
PhD Thesis, UNSW, Sydney, Australia, January, 2010
Abstract PDF 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