Computer Science and Engineering
The seL4 Microkit provides a simple programming model for seL4-based systems, aimed at supporting embedded systems. Developing directly on an embedded platform restricts the available tools, and it would be preferable use a full Linux environment for development.
There exists a rudimentary library for emulating Microkit interfaces on Linux, using UIO to map sDDF shared memory into the space, and to map between notification events and Linux IRQs. There also exists the ability to pass a block device through to a Linux VMM. This leaves the following tasks:
- maturation of the library including (synchronous) protected procedure calls;
- inclusion of simple ways to map device registers and IRQs into UIO;
- actual use cases of drivers developed using this framework.
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 framework that allows using a standard editor, make, GCC, and GDB inside a Linux VMM to build and debug components that can then be deployed natively.
- Report describing the system.
