Checking the hardware-software interface in spec#
Kevin Bierhoff, Chris Hawblitzel · 2007
Research operating systems are often written in type-safe, highlevel 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. 1.