The seL4 Device Driver Framework (sDDF) provides the basis for high-performance I/O in LionsOS, currently under development in TS. It presents a highly modular design with a (compared to Linux) much simplified driver model.
The sDDF presently specifies driver interfaces for a number of device classes, this project is to contribute another class. Of specific interest are:
- HID devices
- video capture (camera)
School
Computer Science and Engineering
Research Area
Operating systems
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- Research environment
- Expected outcomes
- Supervisory team
- Reference material/links
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.
- Specification of sDDF driver interfaces;
- Implementation – depending on the device class and the complexities of the interface, this could be a native driver written from scratch, a native driver ported from a different OS, or a a driver embedded in its normal OS running as a guest in a virtual machine on top of seL4 (a “driver OS”);
- Performance evaluation (keeping in mind that a driver OS will have limited ability to test the performance limits of the design).
