Packet processing and data plane program verification: A survey with tools, techniques, and challenges

In today's era of fast-growing network-enabled devices combined, it increases the complexity of the network. This leads to the massive data packet transfer on the network via the data plane in a software-defined networking environment. The programmable packet processing in a data plane may introduce indirect bugs that are hard to catch manually. To avoid catastrophic after-effects, such programs need to be formally verified. Researchers have proposed various tools and techniques to verify the data plane program using the P4 language. Most of the researchers have used the concept of assertion and symbolic execution to provide P4 verification approaches. As symbolic execution does not scale up well, researchers have proposed different techniques, which include the use of constraints, slicing of the program, parallelization, data plane verification, program verification, and so on. The tools have experimented with different choices for compiler optimization. In this article, we perform a pervasive survey on various verification tools and techniques based on data plane programming using domain-specific language like P4 from the inception of the concept. We have compared the packet processing tools developed as per the requirement of time with their ideology and the impact of change.