Trustworthy Systems develops LionsOS, a fast, statically-architected OS for cyberphysical systems. LionsOS has been shown to perform extremely well in benchmarks and has a large body of drivers to support it in the seL4 Device Driver Framework. LionsOS is not just an operating system however, it also presents a philosophy for designing software with strict separation of concerns in an event-driven programming style. LionsOS has now matured sufficiently to support real-world applications.
The project is to evaluate the developer experience for LionsOS when writing a real, large application. Students will be tasked with re-implementation of our machine queue (MQ) system in the lab, a distributed tool which allows us to easily run experimental OS images on a fleet of dozens of machines in our server room; it is heavily used for development and CI testing. Currently, the machine queue works by using ssh to connect to some utility servers and invoking commands to manage access to boards. A new, LionsOS version of the machine queue will instead offer a dedicated server to multiplex access to boards and to interact with surrounding infrastructure to boot machines. I.e. we will be replacing the ssh-based design with a more robust architecture.
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.
- A large application on LionsOS and evaluate the developer experience.
- Identification of points of friction in working with LionsOS and essential dependencies like the sDDF and Acacia.
- Evaluation of the necessity of the POSIX compatibility layer.
- Stretch goal: implementation of a POSIX subset which works on Linux as well as LionsOS.
- A report describing all the above.
Please check with project lead.