Operating-System Verification

Having pioneered the verification of real-world systems software with the seL4 microkernel, our focus now is to extend this to the verification of a full operating system, LionsOS, with end-to-end proofs of security. This involves three major areas of formal-methods research.

Verification for user-level components

seL4's isolation guarantees support the development of modular systems that can be verified independently of each other. We are developing techniques, generally using automated theorem proving based on SMT solvers.

The LionsOS design uses fine-grained modularity while keeping components as simple as possible, and achieving use-case diversity based on swapping component implementations. One the one hand, simplicity aids verification, on the other hand it implies that verification is an on-going effort: once a particular component has been verified, verifying an alternate implementation must be easy and cheap. This calls for a repeatable verification process accessible to system engineers.

Pancake: Verified systems language

A key tool to making verification of OS components easier and cheaper is our new systems language. Pancake has a simple, well-defined semantics suitable for implementing OS components. Its strength is a verified compiler, which guarantees that the generated binary preserves the semantics of the source code.

Pancake is a collaborative project by researchers at multiple institutions around the world, with most activity happening at TS.

Composing proofs

Having verified system components is a first step, but in itself not sufficient for achieving system-wide security or safety guarantees. This requires reasoning about compositions of concurrently executing components.

Specifically this requires reasoning about the behaviour of components that make seL4 system calls that lead to context switches, or are preempted as a result of events external to the component. It also requires reasoning about components interacting via shared memory.

Verifying Time Protection

We have introduced time protection as a principled approach for the prevention of microarchitectural timing channels. While there is still work in progress on generalising the approach, we are working on verifying the implementation of time protection in the seL4 kernel.

Reasoning about timeliness of MCS

A few years ago we introduced in seL4 a new scheduling model to support mixed-criticality real-time systems (MCS). This version of the kernel is presently being verified.

We are now working on developing a reasoning framework for MCS scheduling on the new kernel version. This comprises several activities:

• Reviving our worst-case execution-time (WCET) analysis, this time for the MCS version of the kernel and the open RISC-V architecture.
• Based on this, develop a timing model of the kernel and, based on this, a reasoning framework for MCS scheduling on seL4 and LionsOS.