Model checking system software with CMC
Madanlal Musuvathi, Andy Chou, David L. Dill, Dawson Engler · 2002
Complex systems have errors that involve mishandled cor-ner cases in intricate sequences of events. Conventional test-ing techniques usually miss these errors. In recent years, formal verification techniques such as [5] have gained pop-ularity in checking a property in all possible behaviors of a system. However, such techniques involve generating an ab-stract 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 ab-stract model of the code. We used CMC to model check an existing implementation of AODV (Ad Hoc On Demand Dis-tance Vector) routing protocol and found a total of 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 fragments per packet. 1