Rule-Based Verification of Network Protocol Implementations Using Symbolic Execution
The secure and correct implementation of network protocols for resource discovery, device configuration and network management is complex and error-prone. Protocol specifications contain ambiguities, leading to implementation flaws and security vulnerabilities in network daemons. Such problems are hard to detect because they are often triggered by complex sequences of packets that occur only after prolonged operation. The goal of this paper is to find semantic bugs in network daemons. The authors' approach is to replay a set of input packets that result in high source code coverage of the daemon and observe potential violations of rules derived from the protocol specification.