Trustworthy Systems

Trustworthy operating systems

We aim to build operating systems with guaranteed levels of security, safety, reliability and efficiency. We tackle this challenge with a broad spectrum of OS research activities, in addition to our formal verification projects.

seL4 microkernel

seL4

The seL4 microkernel is at the core of all our OS research.

seL4 is a tiny and efficient kernel that comes with comprehensive proofs of correctness. It provides other components in a system with essential security and reliability mechanisms.

Being a general-purpose kernel, seL4 supports a variety of software architectures and application domains. This makes it an ideal foundation for us to conduct further research. Additionally, we deploy seL4 in realistic applications and external engagements.

Mixed-criticality support

RT

We have amended the seL4 model to treat time as a first-class resource in order to provide temporal isolation as required by mixed-criticality real-time systems (MCS). These combine a large number of functions, some of which are safety-critical while others are not (or less so). We are presently refining this model to support a wider class of MCS. The MCS-supporting kernel is also presently undergoing verification.

Time protection

Timing channels

Modern computer processors are also highly susceptible to timing-channel attacks, which exploit timing-based information leaks to steal secret data. Timing channels are presently invisible to the conventional specification methods used in our seL4 formal proofs.

We performed thorough quantitive evaluations of existing leaks. We then proposed time protection as a principled, fundamental approach for the systematic prevention of timing channels. This goes hand-in-hand with improvements to the hardware, which we are investigating with our collaborators at ETH Zurich.

High-performance IO systems

Device virtualisation

Microkernels are all about modularity and isolation, and I/O is no different. In an seL4-based system, device drivers run in usermode, so do network stacks and file systems; each in its own address space. Achieving I/O performance comparable to monolithic systems requires careful design and implementation. We are working on suitable device-driver framework that define device and I/O interfaces suitable for achieving high performance.

Furthermore, when sharing an I/O device with one or more virtual machines, we need an appropriate device virtualisation framework, which presents to the VM an interface of a simple device, whose (para-virtualise) driver communicates with the isolated and shared real driver. The actual device driver is then multiplexed between its various clients. We are working on such a high-performance device virtualisation framework for seL4.

Provably secure operating systems

Provably secure operating systems

We are working on the design and implementation of general-purpose operating systems that are secure in a strong sense: provably able to enforce a system-wide security policy.

Obviously such a design is based on seL4, which provide provable isolation and controlled communication. On top is a system structure that ensures access to information only happens according to the centrally-defined security policy. Key challenges are:

Our past projects

In the past, we have also worked on a number of hardware development projects.

Contact

Gernot Heiser, gernot@unsw.edu.au

Publications

Browse our OS research publications.