The seL4 Device Driver Framework (sDDF) provides the basis for high-performance I/O in Lions OS, currently under development in TS. It presents a highly modular design with location-transparent, asynchronous shared-memory-based communication between components. Components are presently implemented as seL4 active servers and seL4 Notifications.

This project is evaluate an alternative approach, namely using passive servers invoked by protected procedure calls. This forces the server to execute on the caller's core, but uses a more efficient seL4 system call. The trade-off is not obvious and will likely depend on multiple aspects 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. Thorough evaluation of sDDF using the passive-server model for some components, such as copiers.
  2. Report describing the evaluation, and the proposed design.
Scientia Professor and John Lions Chair Gernot Heiser
Scientia Professor and John Lions Chair