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.
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.
The code of the sCP will be open-sourced within days, most likely by the time this project is published