SYMBEXNET: Testing Network Protocol Implementations with Symbolic Execution and Rule-Based Specifications
SYMBEXNET: Testing Network Protocol Implementations with Symbolic Execution and Rule-Based Specifications
复制标题
DOI：
10.1109/tse.2014.2323977
复制
发表时间：
2014-07-01
影响因子：
7.4
通讯作者：
Pietzuch, Peter
中科院分区：
文献类型：
--
作者：
Song, JaeSeung;Cadar, Cristian;Pietzuch, Peter
DNS、DHCP 和 Zeroconf 等网络协议的实现很容易出现由于开发人员的错误和协议规范中不明确的要求而导致的缺陷、安全漏洞和互操作性问题。检测此类问题并不容易，因为 (i) 许多错误只有在长时间运行后才会显现出来； (ii) 对语义错误的推理需要机器可读的规范； (iii) 复杂协议实现的状态空间很大。本文提出了一种新颖的方法，该方法结合了符号执行和基于规则的规范来检测网络协议实现中的各种类型的缺陷。我们的方法背后的核心思想是（1）使用单数据包交换符号执行和多数据包交换符号执行（分别针对无状态和有状态协议）自动为网络协议实现生成高覆盖率测试输入数据包，然后（2）使用这些数据包来检测对源自协议规范的手动规则的潜在违反，并检查同一网络协议的不同实现的互操作性。我们提出了一个基于这些技术的系统 SYMBEXNET，并在两种网络协议的多种实现上对其进行了评估：Zeroconf（服务发现协议）和 DHCP（网络配置协议）。 SYMBEXNET 能够发现重要的错误以及互操作性问题，其中大部分已得到开发人员的确认。
Implementations of network protocols, such as DNS, DHCP and Zeroconf, are prone to flaws, security vulnerabilities and interoperability issues caused by developer mistakes and ambiguous requirements in protocol specifications. 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 specification; and (iii) the state space of complex protocol implementations is large. This article presents a novel approach that combines symbolic execution and rule-based specifications to detect various types of flaws 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 specification, and check the interoperability of different implementations of the same network protocol. We present a system based on these techniques, SYMBEXNET, and evaluate it on multiple implementations of two network protocols: Zeroconf, a service discovery protocol, and DHCP, a network configuration protocol. SYMBEXNET is able to discover non-trivial bugs as well as interoperability problems, most of which have been confirmed by the developers.