TCP - IP White Papers
Model Checking Large Network Protocol Implementations
Overview 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.
| Publisher | Stanford University | File Format | |
|---|---|---|---|
| Date Published | April 2007 | ||
| Format | White Papers | ||
| Topics | |||
-
Did you find this white paper useful?
White Paper RSS
Download
Register
