Model checking system software with CMC

ABSTRACT

Complex systems have errors that involve mishandled corner cases in intricate sequences of events. Conventional testing techniques usually miss these errors. In recent years, formal verification techniques such as [5] have gained popularity in checking a property in all possible behaviors of a system. However, such techniques involve generating an abstract model of the system. Such an abstraction process is unreliable, difficult and miss a lot of implementation errors.CMC is a framework for model checking a broad class of software written in the C programming language. CMC runs the software implementation directly without deriving an abstract model of the code. We used CMC to model check an existing implementation of AODV (Ad Hoc On Demand Distance Vector) routing protocol and found a total of 29 bugs in two implementations [7],[6] of the protocol. One of them is a bug in the actual specification of the AODV protocol [3]. We also used CMC on the IP Fragmentation module in the Linux TCP/IPv4 stack and verified its correctness for up to 4 fragments per packet.

REFERENCES

• 1: Boris Beizer, Software testing techniques (2nd ed.), Van Nostrand Reinhold Co., New York, NY, 1990
• 2: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 3: C. Perkins, E. Royer, and S. Das. Ad Hoc On Demand Distance Vector (AODV) Routing. IETF Draft, http://www.ietf.org/internetdrafts/draft-ietf-manet-aodv-10.txt, January 2002.
• 4: 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]
• 5: 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]
• 6: Luke Klein-Berndt and et. al. Kernel AODV Implementation. http://w3.antd.nist/gov/wctg/aodv_kernel/.
• 7: F. Lilieblad and et al. Mad-hoc AODV Implementation. http://mad-hoc.flyinglinux.net/.
• 8: Charles E. Perkins, Elizabeth M. Royer, and Samir R. Das. Private Email Communication.
• 9: J. Postel. Internet Protocol. RFC 791, USC/Information Sciences Institute, September 1981.
• 10: 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