ERTOS Research
Overview
Most research activities of the ERTOS group are part of the Trustworthy Embedded Systems Project. This large project consists of a number of sub-projects or work packages. Some of these are primarily research-focussed, while others are technology demonstrators whose purpose is to showcase our technology as well as help us understand real-world requirements.
Trustworthy Embedded Systems
Under the overall project umbrella we presently have the following activities:
- Secure microkernel design and implementation: seL4
- The seL4 microkernel is the key enabler of most of our work. It provides a minimal and efficient lowest software level, and is the only part of our software that executes in the privileged mode of the hardware. It builds on the strengths of the L4 microkernel architecture, such as small size, high performance, and policy freedom, and extends it with a built-in capability model, which provides the secure software base upon which further secure software layers can be composed to form a trustworthy embedded system.
- Microkernel verification: L4.verified
- A formally-verified microkernel, mathematically proven to be functionally correct, is the trust foundation on which our approach to trustworthy embedded systems is based. The verification subproject performs such a proof on seL4.
- Component Architecture for Microkernel-Based Embedded Systems: CAmkES
- CAmkES is a framework for building efficient medium- to large-sized software systems on top of a microkernel. It leverages the provable protection and isolation properties of the underlying kernel.
- Security Architecture
- We will develop and formally model classes of software architectures, suitable for use on top of seL4, that satisfy the conflicting requirements of a small trusted computing base (TCB) and ability to meet the functional and performance requirements of embedded systems. These architectures will form the basis for formal security/safety guarantees for the whole system.
- Information Flow
- We are analysing the information flow properties of the seL4 kernel. Our aim is to prove the absence of unwanted direct information flows and covert storage channels, and to limit the bandwidth of covert timing channels. We are also investigating scheduling mechanisms that ensure temporal isolation of subsystems.
- Power/Energy Management
- Power management looks to improve the energy efficiency of computer systems by using advanced operating-system level techniques.
- Reliable Device Drivers
- Reliable device drivers are essential to building a reliable OS. We are exploring two complementary approaches to improving the reliability of device drivers:
- Virtualisation
- Virtualisation supports the safe co-existence of large legacy systems with critical sub-systems on the same device and is developing into a major enabler for the design of embedded systems with rich functionality.
- Secure Access Controller
- A multi-level secure system allows the secure co-existence of data with different security classifications on the same device. We are developing such a device as a technology demonstrator.
Former Projects
The research of the ERTOS group grew out of work on the L4 microkernel. Our previous work developed L4 APIs, designs and implementations suitable for embedded-systems use and resulted in its commercial deployment though Open Kernel Labs (OK Labs).
OK Labs has further developed our L4 version into what is now called OKL4, and provides products and services based on this system. We keep using OKL4 at ERTOS as a platform for research (where a stable, industrial-strength kernel is preferable to an evolving research platform) and teaching.
A number of other projects were completed and are no longer active. There is a list of such former projects.
Research Degrees
Looking for information on PhD or Masters by Research studies? Please check the education pages.