Description of field of research:

The seL4 Device Driver Framework (sDDF) is a specification and libraries for writing high-performance device drivers for systems based on the seL4 microkernel. It is presently very network-centric.

The aim of this project is to extend the sDDF to support storage devices, specifically an SD card for an Nvidia Xavier board. Ideally this will be combined with a simple file system. The success of this project will not only extend the sDDF to a new and important device class (and as such demonstrate the generality of the design), but will also enable native support for persistent storage for seL4-based systems.

School

Computer Science and Engineering

Research areas

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. extension of the sDDF design to storage devices;
  2. an SPI SD-card driver based on this design;
  3. a performant SDHC driver based on this design
  4. simple file system using the above driver (stretch goal);
  5. written report describing design and implementation of the above, as well as a performance evaluation and comparison with Linux performance.