Checking the hardware-software interface in spec#

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.

REFERENCES

• 1: Thomas Ball , Ella Bounimova , Byron Cook , Vladimir Levin , Jakob Lichtenberg , Con McGarvey , Bohus Ondrusek , Sriram K. Rajamani , Abdullah Ustuner, Thorough static analysis of device drivers, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
• 2: Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte. The Spec# programming system: An overview. CASSIS, 2004
• 3: B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , S. Eggers, Extensibility safety and performance in the SPIN operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.267-283, December 03-06, 1995, Copper Mountain, Colorado, United States
• 4: Edoardo Biagioni, A structured TCP in standard ML., Proceedings of the conference on Communications architectures, protocols and applications, p.36-45, August 31-September 02, 1994, London, United Kingdom
• 5: Luca Cardelli. Type systems. The Computer Science and Engineering Handbook. CRC Press, 2004. Chapter 97.
• 6: Christopher L. Conway , Stephen A. Edwards, NDL: a domain-specific language for device drivers, Proceedings of the 2004 ACM SIGPLAN/SIGBED conference on Languages, compilers, and tools for embedded systems, June 11-13, 2004, Washington, DC, USA
• 7: Digital Equipment Corporation. DIGITAL Semiconductor 21140A PCI Fast Ethernet LAN Controller Hardware Reference Manual. http://www.intel.com/design/network/manuals/21140ahm.pdf
• 8: Dawson Engler , David Yu Chen , Seth Hallem , Andy Chou , Benjamin Chelf, Bugs as deviant behavior: a general approach to inferring errors in systems code, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada
• 9: Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen C. Hunt, James R. Larus, and Steven Levi. Language Support for Fast and Reliable Message-based Communication in Singularity OS. EuroSys, 2006.
• 10: Michael Golm , Meik Felser , Christian Wawersich , Jürgen Kleinöder, The JX Operating System, Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, p.45-58, June 10-15, 2002
• 11: Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, A principled approach to operating system construction in Haskell, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 12: F. Mérillon, L. Réveillère, C. Consel, R. Marlet, and G. Muller. Devil: An IDL for Hardware programming. Operating Systems Design and Implementation (OSDI), 2000.
• 13: Jun Sun , Wanghong Yuan , Mahesh Kallahalla , Nayeem Islam, HAIL: a language for easy and correct device access, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA [doi>10.1145/1086228.1086230]
• 14: Lea Wittie , Chris Hawblitzel, Type-safe operating system abstractions, Dartmouth College, Hanover, NH, 2005