Computer Science and Engineering
The seL4 Microkit and the operating system (OS) based on it that is under development in the Trustworthy Systems group. There should be a largely transparent way of providing persistence (via checkpoint/restart) for apps, possibly in a similar way as done on smartphones.
This project is to explore possible designs of such persistence support, specifically looking at the model used by iOS and Android, and examine the trade-offs involved with system-wide, transparent and consistent checkpoints vs per-application checkpoints. Provide a prototype implementation and evaluate.
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.
- Report on a detailed exploration of design options and trade-offs.
- Proof-of-concept implementation of the preferred model.
