Model checking concurrent linux device drivers

ABSTRACT

The S<scp>lam</scp> toolkit demonstrates that predicate abstraction enables automated verification of real world Windows device drivers. Our predicate abstraction-based tool DDV<scp>erify</scp>enables the automated verification of Linux device drivers and provides an accurate model of the relevant parts of the kernel. We report on benchmarks based on Linux device drivers, confirming the results that S<scp>lam</scp> established for the Windows world. Furthermore, we take predicate abstraction one step further and introduce a technique to verify concurrent software with shared memory

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: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 3: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 4: G. Basler, D. Kroening, and G. Weissenbacher. SAT-based summarisation for Boolean programs. In SPIN Workshop on Model Checking of Software, volume 4595 of LNCS, 2007.
• 5: Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004 [doi>10.1109/TSE.2004.22]
• 6: E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2988 of LNCS. Springer, 2004.
• 7: E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. SATABS: SAT-based predicate abstraction for ANSI-C. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3440 of LNCS. Springer, 2005.
• 8: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 9: B. Cook, D. Kröning, and N. Sharygina. Symbolic model checking for asynchronous Boolean programs. In SPIN Workshop on Model Checking of Software, volume 3639 of LNCS. Springer, 2005.
• 10: Michael D. Ernst , Jeff H. Perkins , Philip J. Guo , Stephen McCamant , Carlos Pacheco , Matthew S. Tschantz , Chen Xiao, The Daikon system for dynamic detection of likely invariants, Science of Computer Programming, v.69 n.1-3, p.35-45, December, 2007 [doi>10.1016/j.scico.2007.01.015]
• 11: Patrice Godefroid, Software Model Checking: The VeriSoft Approach, Formal Methods in System Design, v.26 n.2, p.77-101, March 2005 [doi>10.1007/s10703-005-1489-x]
• 12: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 13: A. Gurfinkel, O. Wei, and M. Chechik. Yasm: A software model-checker for verification and refutation. In Computer Aided Verification (CAV), volume 4144 of LNCS. Springer, 2006.
• 14: T. A. Henzinger, R. Jhala, R. Majumdar, and S. Qadeer. Thread-modular abstraction refinement. In Computer Aided Verification (CAV), volume 2725 of LNCS. Springer, 2003.
• 15: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 16: K. L. McMillan. The SMV system. Technical Report CMU-CS-92-131, Carnegie Mellon University, 1992.
• 17: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, ACM SIGOPS Operating Systems Review, v.36 n.SI, Winter 2002 [doi>10.1145/844128.844136]
• 18: Hendrik Post , Wolfgang Küchlin, Automatic data environment construction for static device drivers analysis, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181215]
• 19: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 20: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multi-threaded programs, ACM SIGOPS Operating Systems Review, v.31 n.5, p.27-37, Dec. 1997
• 21: S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technische Universität München, 2002.
• 22: T. Witkowski. Formal verification of Linux device drivers. Master's thesis, Dresden University of Technology, 2007.
• 23: Y. Xie and A. Aiken. Saturn: A SAT-based tool for bug detection. In Computer Aided Verification (CAV), volume 3576 of LNCS. Springer, 2005.
• 24: Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, ACM Transactions on Computer Systems (TOCS), v.24 n.4, p.393-423, November 2006 [doi>10.1145/1189256.1189259]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.5 Reliability

General Terms:
Reliability, Verification

Keywords:
device driver, linux, model checking, predicate abstraction