A survey on the verification of adversarial data planes in software-defined networks

As network policies are becoming increasingly nuanced and complex, so too are the mechanisms required to ensure that the network is functioning as intended. In particular, since the dawn of software-defined networking and the shift towards high-level descriptions of intended network policy, traditional tools such as ping and traceroute have been insufficient to test that complex data plane configurations have been correctly implemented. As a result, novel data plane verification solutions have been proposed that use formal methods to ensure that network policies are adhered to and that the data plane is free of bugs. While the number of these verification solutions continues to grow, only a few are equipped to verify the data plane when a malicious adversary is present. As research continues to expand the remit of data plane functionality, these solutions may become key to securing an increasingly valuable attack target. In this survey, we review the work that has been dedicated to preventing and detecting attacks on data planes in software-defined networks and discuss some of the unsolved problems in this field that must be addressed in future adversarial verification solutions.