Title
Improving the Formal Verification of Reachability Policies in Virtualized Networks
Abstract
Network Function Virtualization (NFV) and Software Defined Networking (SDN) are new emerging paradigms that changed the rules of networking, shifting the focus on dynamicity and programmability. In this new scenario, a very important and challenging task is to detect anomalies in the data plane, especially with the aid of suitable automated software tools. In particular, this operation must be performed within quite strict times, due to the high dynamism introduced by virtualization. In this article, we propose a new network modeling approach that enhances the performance of formal verification of reachability policies, checked by solving a Satisfiability Modulo Theories (SMT) problem. This performance improvement is motivated by the definition of function models that do not work on single packets, but on packet classes. Nonetheless, the modeling approach is comprehensive not only of stateless functions, but also stateful functions such as NATs and firewalls. The implementation of the proposed approach achieves high scalability in complex networked systems consisting of several heterogeneous functions.
Year
DOI
Venue
2021
10.1109/TNSM.2020.3045781
IEEE Transactions on Network and Service Management
Keywords
DocType
Volume
Network reachability,data plane verification,service function chains,network security policies
Journal
18
Issue
ISSN
Citations 
1
1932-4537
2
PageRank 
References 
Authors
0.37
0
6
Name
Order
Citations
PageRank
Daniele Bringhenti132.08
Guido Marchetto28620.64
Riccardo Sisto355656.79
Serena Spinoso4212.99
Fulvio Valenza55411.17
Jalolliddin Yusupov632.07