论文标题
在网络协议实现中找到安全漏洞
Finding Security Vulnerabilities in Network Protocol Implementations
论文作者
论文摘要
网络协议的实现通常容易遵循开发人员访问内存区域和处理算术操作时的错误引起的漏洞。发现用于检查网络协议实现安全性的实用方法已被证明是一个具有挑战性的问题。主要原因是协议软件状态空间太大而无法探索。在这里，我们提出了一种新颖的验证方法，该方法将模糊与符号执行结合在一起，以验证网络协议实现中的复杂属性。我们使用模糊来对网络协议进行初步探索，而符号执行探索了程序路径和协议状态，这些状态是通过模糊发现的。通过这种组合，我们自动生成用于网络协议实现的高覆盖测试输入数据包。我们根据模糊和象征性执行进行了调查的各种方法，以了解如何有效地组合这些技术，然后选择合适的工具以进一步开发我们的模型。在我们的初步评估中，我们使用ESBMC，MAP2Check和Klee作为软件验证符和Spike作为Fuzzer，以检查其适用性以验证我们的网络协议实现。我们的实验结果表明，可以在我们的验证框架中进一步开发ESBMC，称为\ textit {fusebmc}，以有效地检测网络协议实现中的复杂安全漏洞。
Implementations of network protocols are often prone to vulnerabilities caused by developers' mistakes when accessing memory regions and dealing with arithmetic operations. Finding practical approaches for checking the security of network protocol implementations has proven to be a challenging problem. The main reason is that the protocol software state-space is too large to be explored. Here we propose a novel verification approach that combines fuzzing with symbolic execution to verify intricate properties in network protocol implementations. We use fuzzing for an initial exploration of the network protocol, while symbolic execution explores both the program paths and protocol states, which were uncovered by fuzzing. From this combination, we automatically generate high-coverage test input packets for a network protocol implementation. We surveyed various approaches based on fuzzing and symbolic execution to understand how these techniques can be effectively combined and then choose a suitable tool to develop further our model on top of it. In our preliminary evaluation, we used ESBMC, Map2Check, and KLEE as software verifiers and SPIKE as fuzzer to check their suitability to verify our network protocol implementations. Our experimental results show that ESBMC can be further developed within our verification framework called \textit{FuSeBMC}, to efficiently and effectively detect intricate security vulnerabilities in network protocol implementations.
