Trustworthy Systems

Funding Cyberagentur Our Partners University of Gothenburg Australian National University Chalmers University of Technology

Pancake logo

Pancake Systems Language

for verified OS components

Aim

Scalable end-to-end verification of device drivers.

Context

Pancake is a new programming language for imperative, space-constrained programming, designed from the ground up with ease of verification in mind. It has a verified compiler, built on the lower parts of the CakeML compiler. Pancake is an international collaboration, development is centered at TS.

Pancake and CakeML compilation passes Verifying drivers with Pancake

Problem

Faulty device drivers are a major source of operating system failures. The seL4 kernel can mitigate this by isolating faulty drivers from other system components. But when drivers perform a mission-critical function, a truly trustworthy system requires formally verified device drivers.

Solution

We will use Pancake to develop and formally verify device drivers. This allows driver development in a low-level language where systems programmers have the control necessary to fine-tune performance and memory usage, while also allowing us to leverage existing verification infrastructure from the CakeML ecosystem. We will likely use Pancake to aid verification of other OS components as well.

Memory safety of the Pancake language, combined with a simple and unambiguous semantics, will enable a significant reduction of effort for verifying a device driver implementation with interactive theorem proving (ITP). We may also be able to re-use the CakeML framework for generating the driver logic from a higher-level specification.

Approach

The Pancake compiler and associated verification tools are still under development. We will contribute to their development, focussing particularly on features that are important for device drivers, such as support for memory-mapped device registers.

Device driver verification needs formal specifications of devices to be useful. This is a particular challenge since driver code is often reused for different devices or operating systems. Truly scalable verification requires similarly reusable device specifications and driver proofs. We will leverage insights from our previous work on device driver synthesis, where devices were successfully modelled using high-level state machines.

Development

CakeML is open source and freely available on GitHub. You can locate the Pancake development at cakeml/pancake.

Support

The Pancake work is financially supported by:

It was previously supported by National Cyber Security Centre and the Technology Innovation Institute.

Collaborations

We are collaborating with:



Latest News

Contact

People

Publications

Abstract PDF Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser
Verifying device drivers with Pancake
arXiv preprint, January, 2025
Abstract PDF Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus Myreen, Michael Norrish and Gernot Heiser
Pancake: verified systems programming made sweeter
Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023