Description of field of research:

The seL4 is a strict microkernel, meaning that all device drivers are user-level programs, as are network protocol stacks and file systems. This means that I/O operations require extra context switches compared to a monolithic system such as Linux, where all those components are inside the kernel.

seL4 has a device driver framework (DDF), which specifies driver interfaces and protocols, but the DDF is so far not fully optimised. This project is to perform a detailed analysis of the DDF performance for a typical network-I/O configuration, consisting of a web server, a TCP/IP stack and an Ethernet driver, all in separate address spaces, comparing this with a corresponding Linux configuration. This analysis will identify performance bottlenecks, and their root cause as either design or implementation shortcomings. These will then be fixed, with the aim of resultant performance no more than 10% worse than Linux.

Research Area

Operating systems

The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.

  1. report describing the analysis, improvements and performance comparison to Linux
  2. pull request against the DDF mainline