Checking the Hardware-Software Interface in Spec#

Kevin Bierhoff and Chris Hawblitzel

Abstract

Research operating systems are often written in type-safe, high-level languages. These languages perform automatic static and dynamic checks to give basic assurances about run-time behavior. Yet such operating systems still rely on unsafe, low-level code to communicate with hardware, with little or no automated checking of the correctness of the hardware-software interaction. This paper describes experience using the Spec# language and Boogie verifier to statically specify and statically verify the safety of a driver's interaction with a network interface, including the safety of DMA.

Details

Publication typeInproceedings
Published inPLOS 07: 4th workshop on Programming languages and operating systems
PublisherAssociation for Computing Machinery, Inc.
> Publications > Checking the Hardware-Software Interface in Spec#