Model Checking Large Network Protocol Implementations
Model Checking Large Network Protocol Implementations
复制标题
DOI：
--
复制
发表时间：
2004-03
期刊：
影响因子：
--
通讯作者：
M. Musuvathi;D. Engler
中科院分区：
文献类型：
--
作者：
M. Musuvathi;D. Engler
网络协议必须工作。协议规范或实现错误的影响范围很广，从性能降低到安全漏洞，再到使整个网络瘫痪。然而，由于网络协议定义的状态空间呈指数级增长，因此很难对其进行测试。理想情况下，协议实现必须针对所有可能的协议状态下的所有可能事件（数据包到达、数据包丢失、超时等）进行验证。传统的检测手段只能探测到这些可能组合中的一小部分。本文主要研究如何利用模型检查这一形式化的验证技术有效地发现大型网络协议实现中的错误。模型检查包括对系统可能状态的系统探索，并且非常适合于发现潜伏在指数状态空间深处的复杂错误。它的主要限制是在软件上使用它所需要的努力。本文的主要贡献是新颖的技术，使我们能够以合理的努力对复杂的、真实的、经过良好测试的协议实现进行建模检查。我们在一个C模型检查器[30]中实现了这些技术，并将结果应用于Linux TCP/IP的实现，发现了协议实现中的四个错误。
Network protocols must work. The effects of protocol specification or implementation errors range from reduced performance, to security breaches, to bringing down entire networks. However, network protocols are difficult to test due to the exponential size of the state space they define. Ideally, a protocol implementation must be validated against all possible events (packet arrivals, packet losses, timeouts, etc.) in all possible protocol states. Conventional means of testing can explore only a minute fraction of these possible combinations. This paper focuses on how to effectively find errors in large network protocol implementations using model checking, a formal verification technique. Model checking involves a systematic exploration of the possible states of a system, and is well-suited to finding intricate errors lurking deep in exponential state spaces. Its primary limitation has been the effort needed to use it on software. The primary contribution of this paper are novel techniques that allow us to model check complex, real-world, well-tested protocol implementations with reasonable effort. We have implemented these techniques in CMC, a C model checker [30] and applied the result to the Linux TCP/IP implementation, finding four errors in the protocol implementation.