A technique that combines symbolic execution with rule-based specifications to find both low- and high-level bugs in network protocol implementations.
Implementations of network protocols, such as DNS, DHCP and Zeroconf, are prone to ﬂaws, security vulnerabilities and interoperability issues caused by developer mistakes and ambiguous requirements in protocol speciﬁcations. Detecting such problems is not easy because (i) many bugs manifest themselves only after prolonged operation; (ii) reasoning about semantic errors requires a machine-readable speciﬁcation; and (iii) the state space of complex protocol implementations is large.
SymbexNet proposes a novel approach that combines symbolic execution and rule-based speciﬁcations to detect various types of ﬂaws in network protocol implementations. The core idea behind our approach is to (1) automatically generate high-coverage test input packets for a network protocol implementation using single- and multi-packet exchange symbolic execution (targeting stateless and stateful protocols, respectively) and then (2) use these packets to detect potential violations of manual rules derived from the protocol speciﬁcation, and check the interoperability of different implementations of the same network protocol.
SymbexNet was evaluated on multiple implementations of two network protocols: Zeroconf, a service discovery protocol, and DHCP, a network conﬁguration protocol, where it was able to discover non-trivial bugs as well as interoperability problems, most of which have been conﬁrmed by the developers.
SymbexNet: Testing Network Protocol Implementations with Symbolic Execution and Rule-Based Specifications
IEEE Transactions on Software Engineering (TSE 2014)
Rule-based Verification of Network Protocol Implementations using Symbolic Execution
IEEE International Conference on Computer Communications and Networks (ICCCN 2011)