Description of field of research:
seL4 is the world's most secure operating-system (OS) kernel. It is a microkernel that does not provide any application-oriented services, these are implemented on top in an OS personality.
One challenge with any new OS is the availability of device drivers, a mechanism for re-using Linux drivers is key to overcoming this challenge.
The project is to enable such re-use by providing a high-performance interface between virtual machines (VMs) on seL4 and the seL4 Device Driver framework (sDDF). This can then used to host Linux drivers in a minimal Linux kernel running inside a VM to provide device access to the sDDF.
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.
- Design of a high-performance, asynchronous interface between VMs and sDDF, based on the Linux virtIO standard
- Implementation of such an interface for one or more device classes, including at least network devices, and optionally storage, frame buffer, USB
- Performance evaluation and analysis of the above
- Report describing design, implementation, performance evaluation, incl comparison to native Linux performance
