Device driver bugs are the leading cause of operating-system exploits, and the lack of accurate specifications of device interfaces is a leading cause of driver bugs. We propose to address the specification issue by deriving formal specifications of devices from their Verilog implementation, and prove the correctness of the specification against the implementation. We demonstrate this approach by applying it to an open-source I2C controller. These specifications should enable synthesis or verification of drivers in the future.

We introduce Pancake, a new language for verifiable, low-level systems programming, especially device drivers. Pancake eschews complex type systems to make the language attractive to systems programmers, while at the same time aiming to ease the formal verification of code. We describe the design of the language and its verified compiler, and examine its usability, performance and current limitations through case studies of device drivers and related systems components for an seL4-based operating system.

Generalizing Fiore et al.'s use of the category of finite sets to model untyped Cartesian contexts and Tanaka's use of the category of permutations to model untyped linear contexts, we let S be an arbitrary pseudo-monad on Cat and let S1 model untyped contexts in general: this generality includes contexts for sub-structural logics such as the Logic of Bunched Implications and variants. Given a pseudo-distributive law of S over the (partial) pseudo-monad for free cocompletions, we define a canonical substitution monoidal structure on the category [(S1)op, Set], generalizing substitution monoidal structures for Cartesian and linear contexts and providing a natural substitution structure for Bunched Implications and its variants. We give a concrete description of the substitution monoidal structure. We then give an axiomatic definition of a binding signature, again extending the definitions for Cartesian and linear contexts. We investigate examples in detail, then prove the central result of the paper, yielding initial algebra semantics for binding signatures at the level of generality we propose.