Skip to main content

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.

Microkernel-based operating systems

seL4 microkernel

The seL4 microkernel is a key part of our research program.

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.

For embedded processors that lack memory protection, we have also developed eChronos, an embedded real-time OS with some degree of formal verification.

Trustworthy components

We are designing a high-quality platform for building component-based systems on seL4. By implementing drivers, services and applications as separate components, many kinds of security and reliability problems can be prevented entirely.

Our CAmkES framework takes a description of a component system as its input, then automatically generates code for setting up the system and for communication between components. We are also working on automatic formal verification for the generated code.

Trustworthy virtualization

seL4 supports virtualisation on many hardware platforms (see full list). This allows us to support legacy software re-use, and also leverage seL4's verified properties to provide a strongly isolated virtual machine environment.

Real-time and mixed-criticality systems

Our real-time systems research aims to provide timing guarantees for complex systems that combine a large number of functions, some of which are safety-critical (mixed-criticality systems). This work includes analysing the temporal properties of seL4-based systems, as well as designing kernel mechanisms to support temporal isolation between different programs.

Kernel mechanisms for real-time systems

We are evolving the seL4 scheduler and API to support general mixed-criticality systems with real-time deadlines. This involves investigating the most appropriate kernel mechanisms for scheduling real-time tasks and sharing resources between them.

Worst-case execution time verification

In medical implants, avionics systems and industrial controllers, some critical operations need to be performed within strict time limits, otherwise disaster may result.

We have successfully shown worst-case time limits for all seL4 kernel operations on a modern ARM processor, using rigorous verification methods. This makes seL4 the only general-purpose OS kernel that can deliver hard real-time guarantees.

Trustworthy COTS hardware

A hardware fault triggered by cosmic rays, alpha particle strikes, etc. could invalidate seL4's strong mathematical proofs, as our proofs assume that the hardware behaves correctly. Commodity off-the-shelf (COTS) computer hardware tends to lack hardware dependability features, so they cannot detect and recover from such faults.

We are investigating how to modify seL4 and its API to support redundant software execution on multicore COTS processors, without sacrificing performance.

Cogent: low-cost verified OS components

Our Cogent programming language aims to make formal verification more affordable for all the device drivers and services that are needed in a modern operating system.

The Cogent toolchain automatically proves that error-prone tasks, such as memory management or error-handling, will be handled correctly. This allows proof engineers to spend their time on the core logic of the problem, i.e. the algorithms.

Information security and timing channels

We have several strands of research for using seL4 to provide strong information security properties.

Notably, we have proven that seL4 can guarantee information-flow security between user programs. This proof eliminates the possibility of information leaks based on the state of kernel or user memory. The CDDC project demonstrates seL4's information security capabilities.

Timing channel prevention

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 perform thorough quantitive evaluations of existing leaks, and have investigated defence mechanisms. Moreover, we are working on principled time protection mechanisms with the eventual goal of proving freedom from timing channels.

Our past projects

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

Contact

Gernot Heiser, gernot.heiser@data61.csiro.au

Publications

Browse our OS research publications.

Served by Apache on Linux on seL4.