Improving the Formal Verification of Reachability Policies in Virtualized Networks. Bringhenti, D., Marchetto, G., Sisto, R., Spinoso, S., Valenza, F., & Yusupov, J. IEEE Transactions on Network and Service Management, 18(1):713-728, 2021.
![Improving the Formal Verification of Reachability Policies in Virtualized Networks [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper doi abstract bibtex 21 downloads
Paper doi abstract bibtex 21 downloads 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.
@Article{2021TNSM,
author = {D. {Bringhenti} and G. {Marchetto} and R. {Sisto} and S. {Spinoso} and F. {Valenza} and J. {Yusupov}},
journal = {IEEE Transactions on Network and Service Management},
title = {Improving the Formal Verification of Reachability Policies in Virtualized Networks},
year = {2021},
number = {1},
pages = {713-728},
volume = {18},
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.},
doi = {10.1109/TNSM.2020.3045781},
keywords = {Reachability Verification, Policy Verification, Security Function Modeling},
url = {https://iris.polito.it/retrieve/handle/11583/2859052/435762/TNSM2021.pdf},
}Downloads: 21
{"_id":"htpEpe49saAzCwBSX","bibbaseid":"bringhenti-marchetto-sisto-spinoso-valenza-yusupov-improvingtheformalverificationofreachabilitypoliciesinvirtualizednetworks-2021","authorIDs":["anJrBcCdr4LzzWetx"],"author_short":["Bringhenti, D.","Marchetto, G.","Sisto, R.","Spinoso, S.","Valenza, F.","Yusupov, J."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["D."],"propositions":[],"lastnames":["Bringhenti"],"suffixes":[]},{"firstnames":["G."],"propositions":[],"lastnames":["Marchetto"],"suffixes":[]},{"firstnames":["R."],"propositions":[],"lastnames":["Sisto"],"suffixes":[]},{"firstnames":["S."],"propositions":[],"lastnames":["Spinoso"],"suffixes":[]},{"firstnames":["F."],"propositions":[],"lastnames":["Valenza"],"suffixes":[]},{"firstnames":["J."],"propositions":[],"lastnames":["Yusupov"],"suffixes":[]}],"journal":"IEEE Transactions on Network and Service Management","title":"Improving the Formal Verification of Reachability Policies in Virtualized Networks","year":"2021","number":"1","pages":"713-728","volume":"18","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.","doi":"10.1109/TNSM.2020.3045781","keywords":"Reachability Verification, Policy Verification, Security Function Modeling","url":"https://iris.polito.it/retrieve/handle/11583/2859052/435762/TNSM2021.pdf","bibtex":"@Article{2021TNSM,\r\n author = {D. {Bringhenti} and G. {Marchetto} and R. {Sisto} and S. {Spinoso} and F. {Valenza} and J. {Yusupov}},\r\n journal = {IEEE Transactions on Network and Service Management},\r\n title = {Improving the Formal Verification of Reachability Policies in Virtualized Networks},\r\n year = {2021},\r\n number = {1},\r\n pages = {713-728},\r\n volume = {18},\r\n 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.},\r\n doi = {10.1109/TNSM.2020.3045781},\r\n keywords = {Reachability Verification, Policy Verification, Security Function Modeling},\r\n url = {https://iris.polito.it/retrieve/handle/11583/2859052/435762/TNSM2021.pdf},\r\n}\r\n\r\n","author_short":["Bringhenti, D.","Marchetto, G.","Sisto, R.","Spinoso, S.","Valenza, F.","Yusupov, J."],"key":"2021TNSM","id":"2021TNSM","bibbaseid":"bringhenti-marchetto-sisto-spinoso-valenza-yusupov-improvingtheformalverificationofreachabilitypoliciesinvirtualizednetworks-2021","role":"author","urls":{"Paper":"https://iris.polito.it/retrieve/handle/11583/2859052/435762/TNSM2021.pdf"},"keyword":["Reachability Verification","Policy Verification","Security Function Modeling"],"metadata":{"authorlinks":{"valenza, f":"https://bibbase.org/show?bib=https%3A%2F%2Fraw.githubusercontent.com%2FFulvioValenza%2Fbibliography%2Fmain%2FValenza_bibliography.bib&commas=true"}},"downloads":21},"bibtype":"article","biburl":"https://raw.githubusercontent.com/FulvioValenza/bibliography/main/Valenza_bibliography.bib","creationDate":"2021-03-12T07:57:29.785Z","downloads":21,"keywords":["reachability verification","policy verification","security function modeling"],"search_terms":["improving","formal","verification","reachability","policies","virtualized","networks","bringhenti","marchetto","sisto","spinoso","valenza","yusupov"],"title":"Improving the Formal Verification of Reachability Policies in Virtualized Networks","year":2021,"dataSources":["JbiX35GNqPCF3nids","JotHtgcQ35FTMtuP5","oHcDH9GXBbkp4t9gm","csYhy47rJJgSM7jjJ","hZL94qE5m3pMWuJwA","8EGSmY4udryikjQyX","nMy6C9RcR4TJMDbmB","Ka2S54TRk8na4h8uK","qgD6ZecrgthN9jyS8","yf5ybPwJxfS5zDTx9","8iJ7pScsBCJNMEwBL","XZnEt8kdXurbtCWoc","R3zwdw7JArkWqNexb"]}