Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics
Finding Bugs in Network Protocols Using Simulation Code and Protocol-Specific Heuristics
复制标题
使用模拟代码和特定于协议的启发法查找网络协议中的错误
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Hou
中科院分区：
文献类型：
--
作者：
Ahmed Sobeih;Mahesh Viswanathan;D. Marinov;J. Hou
传统的网络仿真器能够很好地评估网络协议的性能，但缺乏验证协议正确性的能力。为了解决这个问题，我们扩展了J-Sim网络模拟器，使其具有模型检测功能，该功能可以探索网络协议的状态空间，以找到违反安全不变量的执行。在本文中，我们通过分析两个广泛使用的重要网络协议：AODV协议和定向扩散协议，论证了该集成工具在验证和性能评估中的有效性。我们的分析在AODV的J-Sim实现中发现了一个以前未知的错误。更重要的是，我们还发现了定向扩散的一个严重缺陷。为了能够分析这些相当复杂的协议，我们需要开发特定于协议的搜索启发式方法来指导状态空间探索。我们报告了我们的发现，发现了良好的搜索启发式方法来分析类似于AODV和定向扩散的网络协议。
Traditional network simulators perform well in evaluating the performance of network protocols but lack the capability of verifying the correctness of protocols. To address this problem, we have extended the J-Sim network simulator with a model checking capability that explores the state space of a network protocol to find an execution that violates a safety invariant. In this paper, we demonstrate the usefulness of this integrated tool for verification and performance evaluation by analyzing two widely used and important network protocols: AODV and directed diffusion. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV. More importantly, we also discovered a serious deficiency in directed diffusion. To enable the analysis of these fairly complex protocols, we needed to develop protocol-specific search heuristics that guide state-space exploration. We report our findings on discovering good search heuristics to analyze network protocols similar to AODV and directed diffusion.