Skip to main content

Showing 1–1 of 1 results for author: Legnani, A

Searching in archive cs. Search in all archives.
.
  1. arXiv:2501.08249  [pdf, ps, other

    cs.PL cs.CR cs.OS

    Verifying Device Drivers with Pancake

    Authors: Junming Zhao, Miki Tanaka, Johannes Åman Pohjola, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish, Gernot Heiser

    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 back… ▽ More

    Submitted 29 May, 2025; v1 submitted 14 January, 2025; originally announced January 2025.

    Comments: 15 pages, 5 figures

    ACM Class: D.2.4; D.3.4; D.4.6