Finding Security Vulnerabilities in Network Protocol Implementations

TL;DR

This paper introduces a novel verification approach combining fuzzing and symbolic execution to detect security vulnerabilities in network protocol implementations, addressing the challenge of large state-spaces.

Contribution

It presents a new method that integrates fuzzing and symbolic execution for thorough verification of network protocols, and develops the FuSeBMC framework based on this approach.

Findings

ESBMC can be effectively integrated into FuSeBMC

The combined approach improves vulnerability detection coverage

Preliminary results show promising detection of security flaws

Abstract

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.