| Network protocols are hard to test due to the many nondeterministic events they handle. Protocol implementers must carefully handle all possible events (timeouts, packet losses, network failures) in all possible protocol and network states. Conventional testing can explore only a minute fraction of the exponential number of such combinations, leaving a residue of errors even in well-tested systems.; This thesis proposes CMC a C Model Checker specifically designed to find and diagnose deep errors in network protocol implementations. CMC works directly description. Thus, CMC avoids the upfront cost traditionally associated with model checking, making it practical to scale to large systems.; This thesis applies CMC to two network protocols: AODV & TCP. CMC checked three publicly available AODV implementations and found a total of 35 errors including an error in the underlying AODV protocol specification. CMC successfully checked the Linux TCP implementation, demonstrating its applicability to large, complex systems. It found four instances where the particular TCP implementation checked (version 2.4.19) fails to satisfy the TCP specification. |
