Description of field of research:
seL4 is the world's first operating system (OS) kernel with a proof of implementation correctness, followed by proofs of security enforcement; it is at the same time the benchmark for microkernel performance. The seL4 Core Platform (sCP) is a minimal seL4-based OS aimed at embedded and cyberphysical systems. The sCP is intentionally kept lean and simple, to minimise overheads while ensuring correct use of seL4 mechanisms.
Its simplicity should enable verification of the sCP, extending seL4's assurance to the complete OS. This project is to investigate the use of SMT solvers to automatically verify the sCP implementation. The main challenges will be to formally specify the sCP API, and tweak the SMT problem, as well as the sCP implementation for verification to succeed.
School
Research Area
Operating systems | Formal methods
- Research Environment
- Expected Outcomes
- Reference Material/Links
- Our team
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 describing experience verifying the sCP using an SMT solver
- formal specification of at least a significant part of the sCP
- successful verification of at least a subset of the specified functionality
- potentially pull requests against the public sCP source
https://trustworthy.systems
https://sel4.systems
https://sel4.atlassian.net/browse/RFC-5
The code of the sCP will be open-sourced within days, most likely by the time this project is published
