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

Summary: 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. [ABSTRACT FROM AUTHOR]

Copyright of International Journal of Communication Systems is the property of Wiley-Blackwell and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)