The Trustworthy Systems group has developed a new Operating Systems framework, called LionsOS, that currently runs on Risc-V and aarch64. It works with multiple components each in its own address space talking to each other using seL4 notifications and queues in shared memory regions. LionsOS uses virtual machines as a way to support legacy software.
This project is largely engineering rather than research; it involves porting LionOS to x86_64, and especially, porting libvmm, the virtual machine library that provides hypervisor support, to x86_64.
Stretch goals include implementing or porting firewall components to provide and control network access between VMs, and between VMs and the outside world; and control software for shutrting down and rebooting VMs.
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.
- Performant LionsOS on x86_64
- Usable libvmm for x86_64
