Wen Shameng, Meng Qingkun, Feng Chao, Tang Chaojing
College of Electronic Science and Engineering, National University of Defense Technology, Changsha, China.
PLoS One. 2017 Nov 16;12(11):e0188229. doi: 10.1371/journal.pone.0188229. eCollection 2017.
Formal techniques have been devoted to analyzing whether network protocol specifications violate security policies; however, these methods cannot detect vulnerabilities in the implementations of the network protocols themselves. Symbolic execution can be used to analyze the paths of the network protocol implementations, but for stateful network protocols, it is difficult to reach the deep states of the protocol. This paper proposes a novel model-guided approach to detect vulnerabilities in network protocol implementations. Our method first abstracts a finite state machine (FSM) model, then utilizes the model to guide the symbolic execution. This approach achieves high coverage of both the code and the protocol states. The proposed method is implemented and applied to test numerous real-world network protocol implementations. The experimental results indicate that the proposed method is more effective than traditional fuzzing methods such as SPIKE at detecting vulnerabilities in the deep states of network protocol implementations.
形式化技术已被用于分析网络协议规范是否违反安全策略；然而，这些方法无法检测网络协议自身实现中的漏洞。符号执行可用于分析网络协议实现的路径，但对于有状态的网络协议，很难达到协议的深层状态。本文提出一种新颖的模型引导方法来检测网络协议实现中的漏洞。我们的方法首先抽象出一个有限状态机（FSM）模型，然后利用该模型引导符号执行。这种方法在代码和协议状态方面都实现了高覆盖率。所提出的方法已被实现并应用于测试众多实际的网络协议实现。实验结果表明，所提出的方法在检测网络协议实现深层状态中的漏洞方面比传统的模糊测试方法（如SPIKE）更有效。
