libvmm is a library for creating virtual machine monitors (VMMs) on the seL4 microkernel, and is a core component of LionsOS. It can boot Linux on AArch64 and x86-64, and on x86-64 it can also boot Windows 11 with a graphical desktop. Multi-core (multiple vCPU) guests are currently supported on AArch64, but not on x86-64. The goal of this project is to extend libvmm to support multi-core Linux guests on x86-64, with multi-core Windows 11 as a stretch goal.
More specifically, the project requires re-architecting the existing VMM from a single-vCPU design into one that runs multiple vCPUs across multiple physical cores, for example one VMM per vCPU with a way for them to communicate. The design is open: you will decide on the architecture and justify it. Key pieces of this project include bringing up secondary vCPUs (x86 INIT/SIPI sequence), delivering IPIs between vCPUs, and per-vCPU local APICs and timers.
School
Computer Science and Engineering
Research Area
Programming Languages and Software Engineering
Suitable for recognition of Work Integrated Learning (industrial training)?
Please check with project lead
- 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, implementation and evaluation of multi-core Linux guests in libvmm, including performance compared to Linux KVM; Stretch goal: multi-core Windows 11 guests; A report describing all the above.
This project requires a COMP9242 Advanced Operating Systems background.
Please check with project lead.