CMC: a pragmatic approach to model checking real code

ABSTRACT

Many system errors do not emerge unless some intricate sequence of events occurs. In practice, this means that most systems have errors that only trigger after days or weeks of execution. Model checking [4] is an effective way to find such subtle errors. It takes a simplified description of the code and exhaustively tests it on all inputs, using techniques to explore vast state spaces efficiently. Unfortunately, while model checking systems code would be wonderful, it is almost never done in practice: building models is just too hard. It can take significantly more time to write a model than it did to write the code. Furthermore, by checking an abstraction of the code rather than the code itself, it is easy to miss errors.The paper's first contribution is a new model checker, CMC, which checks C and C++ implementations directly, eliminating the need for a separate abstract description of the system behavior. This has two major advantages: it reduces the effort to use model checking, and it reduces missed errors as well as time-wasting false error reports resulting from inconsistencies between the abstract description and the actual implementation. In addition, changes in the implementation can be checked immediately without updating a high-level description.The paper's second contribution is demonstrating that CMC works well on real code by applying it to three implementations of the Ad-hoc On-demand Distance Vector (AODV) networking protocol [7]. We found 34 distinct errors (roughly one bug per 328 lines of code), including a bug in the AODV specification itself. Given our experience building systems, it appears that the approach will work well in other contexts, and especially well for other networking protocols.

REFERENCES

• 1: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 2: K. Bhargavan, D. Obradovic, and C. Gunter. Formal verification of standards for distance vector routing protocols, 1999.
• 3: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 4: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 5: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 6: Crispan Cowan, Calton Pu, Dave Maier, Jonathan Walpole, Peat Bakke, Steve Beattie, Aaron Grier, Perry Wagle, Qian Zhang, and Heather Hinton. Stack Guard:Automatic adaptive detection and prevention of buffer-overflow attacks. In Proc. 7th USENIX Security Conference, pages 63--78, San Antonio, Texas, jan 1998.
• 7: C.Perkins, E. Royer, and S. Das. Ad Hoc On Demand Distance Vector (AODV) Routing.IETF Draft, http://www.ietf.org/internet-drafts/draft-ietf-manet-aodv-10.txt, January 2002.
• 8: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 9: David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking, 1998.
• 10: David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
• 11: D.R. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the Fourth Symposium on Operating Systems Design and Implementation, October 2000.
• 12: Erik Nordstrom et al. Ad hoc protocol evaluation testbed. http://apetestbed.sourceforge.net/.
• 13: Erik Nordstrom et al. AODV-UU Implementation. http://user.it.uu.se/henrikl/aodv/.
• 14: David Evans , John Guttag , James Horning , Yang Meng Tan, LCLint: a tool for using specifications to check code, Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, p.87-96, December 06-09, 1994, New Orleans, Louisiana, United States
• 15: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 16: J. Hajek. Automatically verified data transfer protocols. In Proceedings of the 4th ICCC, pages 749--756, 1978.
• 17: Sudheendra Hangal , Monica S. Lam, Tracking down software bugs using automatic anomaly detection, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581377]
• 18: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 19: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 20: Luke Klein-Berndt and et.al. Kernel AODV Implementation. http://w3.antd.nist.gov/wctg/aodv_kernel/.
• 21: F. Lilieblad and et.al. Mad-hoc AODV Implementation. http://mad-hoc.flyinglinux.net/.
• 22: S. McCanne and S. Floyd. UCB/LBNL/VINTnetwork simulator - ns (version 2), April 1999. http://www.isi.edu/nsnam/ns/.
• 23: K.L. McMillan and J. Schwalbe. Formal verification of the gigamax cache consistency protocol. In Proceedings of the International Symposium on Shared Memory Multiprocessing, pages 242--51. Tokyo, Japan Inf. Process. Soc., 1991.
• 24: G. Nelson. Techniques for program verification. Available as Xerox PARC Research Report CSL-81-10, June, 1981, Stanford University, 1981.
• 25: David Y. W. Park , Ulrich Stern , Jens U. Sakkebæk , David L. Dill, Java Model Checking, Proceedings of the 15th IEEE international conference on Automated software engineering, p.253, September 11-15, 2000
• 26: Charles E. Perkins, Elizabeth M. Royer, and Samir R.Das. Private Email Communication.
• 27: Rational Software. Purify: Advanced runtime error checking for C/C++ developers. http://www.rational.com/products/purify_unix/.
• 28: Ulrich Stern , David L. Dill, A new scheme for memory-efficient probabilistic verification, IFIP TC6/ 6.1 international conference on formal description techniques IX/protocol specification, testing and verification XVI on Formal description techniques IX : theory, application and tools: theory, application and tools, p.333-348, January 1996, Kaiserslautern, Germany
• 29: Ulrich Stern , David L. Dill, Automatic verification of the SCI cache coherence protocol, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.21-34, October 02-04, 1995
• 30: C.H. West. General technique for communications protocol validation. IBM Journal of Research and Development, 22(4), 1978.

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Data abstraction
      D.2.8 Metrics
          Subjects: Process metrics

General Terms:
Performance, Verification