Verifying Device Drivers with Pancake
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.
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:
It was also supported by National Cyber Security Centre previously.
Collaborations
We are collaborating with:
- Johannes Åman Pohjola at the University of Gothenburg
- Michael Norrish at ANU
- Magnus Myreen at Chalmers University of Technology.
Contact
- Johannes Åman Pohjola, j.amanpohjola<at>unsw.edu.au
People
Current |
Past |
Publications
|
 |
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 |