The seL4 microkernel is known not only for its comprehensive formal verification story but also for being the benchmark for microkernel IPC performance. However, for the cost of protection in client-server interactions in a secure OS, the code required to marshal parameters to the IPC system call is also a factor. This project is to evaluate the performance cost of these stubs and the potential for the compiler optimising them away on bare seL4. In a second step, this analysis is to be extended to the interfaces required for the CAmkES framework. If there is time, look at the potential for generating efficient stubs from an interface generator.
School
Computer Science and Engineering
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.
- Report describing the results of the performance analysis
- Potentially pull requests against the libsel4 repository for optimised stub code
