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.

Lions OS: Secure, fast, adaptable

Lions OS structure

The seL4 microkernel provides strong data and resource isolation and low-overhead cross-address-space communication. As such, it is ideally suited as the basis of a highly modular OS. Unfortunately, systems built on top of seL4 are largely semi-monolithic, with heavyweight components providing services to applications, similar to OSes built on other, less-performant microkernels.

With the Lions Operating System we are working on changing this, by developing a highly modular, yet performant OS for embedded, cyber-physical and IoT systems. Furthermore, we are working on formally proving that Lions OS is secure, in that it will guarantee that the system adheres to its security policy. This verification is enabled by the highly modular design of the OS, with individual modules kept as simple as possible, an approach we call radical simplicity.

Lions OS builds on the seL4 Microkit, a thin abstraction layer that greatly simplifies the seL4 API, and the high-performance seL4 Device Driver Framework (sDDF), which has demonstrated networking performance that beats Linux.

Mixed-criticality support

Real Time System block diagram

We have enhanced 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.

We performed a complete, sound and high-assurance worst-case execution-time (WCET) analysis of seL4 (for Armv6 processors). We plan to re-establish this analysis for an open-source, 64-bit RISC-V processor, using execution latencies extracted from the processor source.

We also plan to develop a reasoning framework for schedulability analysis of mixed-criticality systems on top of the seL4 MCS kernel.

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.

We are presently working on verifying time protection, i.e. proving the absence of cross-domain leakage through microarchitectural timing channels on a implementation of time protection in seL4.

Provably secure, general-purpose 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:

  • 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.

Contact

Gernot Heiser, gernot@unsw.edu.au

Publications

Browse our OS research publications.