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 policy isolated in individual components (as well as overall configuration parameters). It is not a-priori clear that such a simple design will provide good performance under all circumstances; other systems implement feedback loops to tune performance aspects dynamically.
This project is to stress and analyse the queueing behaviour of I/O data in sDDF networking, using extreme cases, such as a low-priority client degrading service to high-priority clients by generating excessive input traffic. It should try to answer the question of whether existing parameters (queue sizes, priorities, budgets and virtualiser-implemented queue-processing policies) are sufficient to handle extreme cases, including malicious clients that collude with external data sources.
School
Research Area
Operating systems | Networks
- 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.
- Thorough evaluation of sDDF under stress, using the existing policy parameters;
- Report describing the evaluation, and learnings about the suitability of the existing approach, and, if appropriate, suggestions on how to improve it.
