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 Microkit is a minimal seL4-based OS framework aimed at embedded and cyberphysical systems.
The verification of the seL4 Microkit library relies on the kernel correctly implementing certain functional properties of seL4's system calls, phrased as postconditions on the system call's outputs it must meet if its caller satisfies preconditions on its inputs. Work at TS has recently begun on proving such properties are satisfied by the seL4 kernel's abstract specification in the Isabelle/HOL interactive theorem prover.
This project is to increase the coverage of functional properties proved about seL4's system calls, initially focusing on cases most relevant to their use by the seL4 Microkit. Stretch goals can include proving further such properties as guided by the informal specifications given in the seL4 Reference Manual.
School
Computer Science and Engineering
Research Area
Formal verification | 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.
- verification of a Microkit-relevant functional property for at least one seL4 system call;
- report describing experience and any new proof infrastructure developed to verify seL4 system call functional properties using Isabelle/HOL.
