Verifying Device Drivers with Pancake
Junming Zhao, Miki Tanaka, Johannes {\AA}man Pohjola, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish, Gernot Heiser

TL;DR
This paper introduces Pancake, a new imperative language for systems programming with a verified compiler, enabling the formal verification of realistic device drivers, demonstrated by verifying an Ethernet NIC driver.
Contribution
Pancake's design and verified compiler backend facilitate the formal verification of complex, real-world device drivers, a task previously unachieved in the field.
Findings
Verified an Ethernet NIC driver using Pancake
Demonstrated the feasibility of verifying realistic device drivers
Ensured binary semantics preservation through verified compilation
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSocial Robot Interaction and HRI
