The seL4 Device Driver Framework (sDDF) provides the basis for high-performance I/O in Lions OS, currently under development in TS. It is highly modular, with components communicating via shared memory and semaphore-like seL4 Notifications. sDDF performance is dependent on an efficient signalling protocol, which avoids signalling components when they cannot make progress, while maintaining deadlock- and livelock-freedom. These properties have been verified using the SPIN model-checker.
However, these proofs are only useful as long as the model is a correct abstraction of the actual sDDF. Presently the models are manually derived from inspecting the source code, or the source code is adapted to implement a verified model. The aim of this project is to provide more assurance that the model is a fair representation of the sDDF communication. The project is therefore to develop a tool that tries to establish correspondence between the model and the C implementation. The ultimate aim is to prove that the C implementation refines the SPIN model, this project is a first step towards this aim.
School
Computer Science and Engineering
Research Area
Formal methods | 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.
- Tool that matches the SPIN model against the communication system calls in the sDDF implementation, and either reports success or indicates where it fails to establish correspondence;
- report describing the approach.
