Computer Science and Engineering
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. The sDDF is presently fully static, which iss sufficient for supporting a large class of embedded systems.
However, hot-pugging/unplugging devices, long a standard requirement for laptop and desktop computers, is also increasingly required in some embedded/cyberphysical systems. For example, devices (eg wifi) may need to be turned off to conserve energy, SD cards may be inserted for adding or upgrading software components, or USB device may be connected for maintenance.
This project is to propose, design, implement and evaluate support for hot-plugging in the sDDF.
School
Research Area
Operating systems
- 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.
- A design, prototype implementation and evaluation of dynamically adding/removing devices in the sDDF;
- Report describing the design, implementation and evaluation.
