The high-performance I/O system for seL4, based on the seL4 device driver framework (sDDF) and the lwip protocol stack, is presently highly optimised for UDP traffic (outperforming Linux) but not for TCP. The project is to measure and analyse TCP performance, identify bottlenecks and improve or rewrite the respective functionality of lwip and possibly other parts of the system.

School

Computer Science and Engineering

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. Improved networking system with performance competitive with Linux
  2. Report describing the approach, implementation and evaluation results.
Senior  Systems Consultant Peter Chubb
Senior Systems Consultant
Junior Systems Engineer