Computer Science and Engineering
The high-performance I/O system for seL4, based on the seL4 device driver framework (sDDF), is designed for minimal overheads and thus uses asynchronous interfaces. This project is to design and implement an easier-to-use, Posix-style blocking interface for programmers who prefer this simplified (but less efficient) API.
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.
- Investigation of design choices (library that uses the existing asynchronous interface vs offering it directly as part of the seL4 framework and tradeoffs (need for copying, implementation simplicity, ...)
- Implementation and performance evaluation of the chosen model
- Report describing design, implementation and evaluation results.
