Model Checking Large Network Protocol Implementations

Network protocols must work. The effects of protocol specification or implementation errors range from reduced performance, to security breaches, to bringing down entire networks. However, network protocols are difficult to test due to the exponential size of the state space they define. Ideally, a protocol implementation must be validated against all possible events (packet arrivals, packet losses, timeouts, etc.) in all possible protocol states. This paper focuses on how to effectively find errors in large network protocol implementations using model checking, a formal verification technique. The authors have implemented these techniques in CMC, a C model checker and applied the result to the Linux TCP/IP implementation, finding four errors in the protocol implementation.