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.
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.
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.
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.
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.
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:
In the past, we have also worked on a number of hardware development projects.
Gernot Heiser, gernot@unsw.edu.au
Browse our OS research publications.