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 presently has network and storage (SDcard) drivers, but the framework itself is still fairly network-centric.
The aim of this project is to design and implement a high-performance storage layer. This implies understanding the different trade-offs between network and storage, and designing an appropriate model for caching, naming and secure sharing of devices. For performance, the approach will use an asynchronous interface (very much unlike Posix). The design should also be agnostic to the underlying persistent data structure (also known as the on-medium file system) and should re-use an existing one. This will add a core system service to the seL4 ecosystem.
School
Research Area
Operating systems
- Research Environment
- Expected Outcomes
- Reference Material/Links
- Our team
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.
- extension of the sDDF design to storage services, with an asynchronous client interface;
- implementation of the design that works on an Arm-based development board;
- performance evaluation and analysis;
- written report describing design, implementation and performance evaluation and comparison with Linux performance.
