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.
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.
High-performance IO systems
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
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:
- performance that is in the ballpark of a mainline, insecure system such as Linux;
- ability to support a wide range of use cases, from cyberphysical systems to mobile devices, public clouds and defence-grade enterprise systems;
- suitability for proof of security enforcement, meaning the trusted computing base must be small, modular with only well-defined inter-module dependencies.
Our past projects
- CDDC — the Cross-Domain Desktop Compositor is a military-grade high-assurance device for connecting to multiple networks of different classification
- Dingo — untangling the interface between device drivers and the OS
- eChronos — an embedded real-time OS with some degree of formal verification.
- Energy management — managing energy and power in embedded operating systems
- Multiprocessor-kernel verification — verification of an early version of the multiprocessor seL4 kernel
- QB50 — seL4 on a satellite payload
- Termite — automatic synthesis of device drivers
- Trustworthy components — the CAmkES framework and its verification
- Trustworthy COTS hardware — use the redundancy of off-the-shelf multicore processors to protect against random hardware faults
- Verification-enhanced compiler optimisation — optimising code based on formally proven properties
- Research in virtualisation techniques — see our virtualisation page for details
- Worst-case execution-time analysis of seL4
In the past, we have also worked on a number of hardware development projects.
Gernot Heiser, firstname.lastname@example.org
Browse our OS research publications.