Verifying Device Drivers with Pancake
Programming Languages
2025-06-02 v2 Cryptography and Security
Operating Systems
Abstract
Device driver bugs are the leading cause of OS compromises, and their formal verification is therefore highly desirable. To the best of our knowledge, no realistic and performant driver has been verified for a non-trivial device. We propose Pancake, an imperative language for systems programming that features a well-defined and verification-friendly semantics. Leveraging the verified compiler backend of the CakeML functional language, we develop a compiler for Pancake that guarantees that the binary retains the semantics of the source code. Usng automatic translation of Pancake to the Viper SMT front-end, we verify a performant driver for an Ethernet NIC.
Cite
@article{arxiv.2501.08249,
title = {Verifying Device Drivers with Pancake},
author = {Junming Zhao and Miki Tanaka and Johannes Åman Pohjola and Alessandro Legnani and Tiana Tsang Ung and H. Truong and Tsun Wang Sau and Thomas Sewell and Rob Sison and Hira Syeda and Magnus Myreen and Michael Norrish and Gernot Heiser},
journal= {arXiv preprint arXiv:2501.08249},
year = {2025}
}
Comments
15 pages, 5 figures