Computer Science and Engineering
The seL4 Core Platform (seL4CP) provides support for virtual machines (VMs) for running legacy software stacks. At present, these need to be packaged with the seL4CCP boot image. This project is to provide support for booting a VM from a separate disk image (possibly across a network) containing a standard Linux distribution.
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.
- Design and prototype implementation of late loading of a Linux image into an seL4 VM.
- Report describing the above.
