Funding

Aim

Verification that seL4's system calls function as assumed by proofs about user-level programs.

Context

The formally verified seL4 microkernel is the most solid foundation for building secure systems. However, building on seL4 does, in itself, not guarantee that the operating system (OS) on top is secure or safe. This requires further proofs about the correct operation of the critical user-level code of the OS.

We are working on verification of such user-mode components, in particular the seL4 Microkit, the seL4 Device Driver Framework, and the LionsOS operating system built from these. Such proofs about user-level components inevitably rest on assumptions that the seL4 kernel correctly implements the system calls that these components use.

Problem

Why is this a problem, given that seL4's code was proved to correctly implement its specification?

In the user-mode code's view, system calls operate like a typical function call – that is, they perform the requested operation then return its result. This view allows reasoning about user-level code while largely ignoring the rest of the system – in fact, such independence is a core property of the abstraction provided by an OS kernel.

In reality, however, many system calls block the caller pending action of another user-level component, which means they switch execution to the other component(s) and eventually return to the original caller.

This may sound surprising, but to date, no OS verification project in the literature has proved that the kernel establishes a system call's functional property as seen by the user code, when its actual operation required it to block, waiting on a system call by another user. The property goes well beyond the functional correctness against an operational specification that was proved for seL4 (and a number of later systems), in that it requires that other activities have no unspecified effect on state relevant to the blocked system call under consideration.

Approach

The property we aim to prove is a Hoare triple spanning from the initial kernel invocation to returning to the original caller. We must compose such triples for the initial blocking call (i.e. that suspends the original caller) and any final unblocking calls (i.e. that would resume the original caller), with an arbitrary number of intervening irrelevant (to the blocked system call) entries into the kernel. To our knowledge, no prior formalism has been developed to facilitate this, despite being essential for synchronous communication between user-level components.

We are developing a formalism and infrastructure to prove and compose the required Hoare triples over seL4's abstract specification in Isabelle, and applying them to verify initially the system call requirements identified by our seL4 Microkit verification efforts.

Latest News

• 2026-02-01: Foresight Institute provides supporting funding for this project.
• 2025-01-20: Cyberagentur launches the ÖViT program, which funds this research through the PISTIs-V project.

Support

This research is financially supported by:

• A grant from the Foresight Institute.
• Cyberagentur under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program funds the PISTIs-V Project of which this research is a part.

Contact

• Rob Sison, r.sison<at>unsw.edu.au

People