Trustworthy Systems

Our Partners NCSC Technology Innovation Institute Australian National University Chalmers University of Technology


Verifying Device Drivers with Pancake

Pancake logo

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.

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 the Technology Innovation Institute. It was also supported by National Cyber Security Centre previously.

Collaborations

We are collaborating with Michael Norrish at ANU and Magnus Myreen at Chalmers University of Technology.

Contact

People

Publications

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