Description of field of research
The seL4 Device Driver Framework (sDDF) is a specification and libraries for writing high-performance device drivers for systems based on the seL4 microkernel. It aims to combine performance with implementation simplicity by using a highly modular design, strict separation of concerns and simple, event-based sequential module implementation. Modules communicate via lock-free, bounded, single-producer, single-consumer queues and asynchronous, semaphore-like signalling.
While the resulting module simplicity aids verification of functional correctness, it shifts some complexity into inter-module communication protocols, and these are now the leading source of implementation bugs. The aim of this project is to use model checking to verify the correct implementation of those protocols.
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.
- Verified model of the signalling protocol of the seL4 networking system built on sDDF, proving deadlock-freedom, liveness as well as (stretch goal) more stringent progress properties;
- Automatic extraction of the model from the C implementation of the sDDF (stretch goal) or at least an informal argument that the model represents the code;
- Report describing the model and the verification.
