Our Partners
Scalable end-to-end verification of device drivers.
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.
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.
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.
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.
We are collaborating with researchers from ANU and Chalmers University of Technology.
Current |
Past |
|
 |
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 |