Virtual network embedding with formal reachability assurance

Networks are becoming increasingly software-defined and automated. In this context, SDN and NFV allow service providers to use the network infrastructure more efficiently with reduced cost and to develop secure services. This procedure of efficient mapping of virtual networks on the substrate network is delegated to an orchestrator component of NFV that automatically manages its constituent virtualized network functions (VNFs). However, incomplete or inconsistent configuration of VNFs and service graphs may be vulnerable to potential security threats and could cause breakdown of services and of the supporting infrastructure. The main purpose of this paper is to provide an approach for allocation and formal verification that can ensure at the same time that policies such as reachability or isolation are never violated and that optimization is achieved. This ability to orchestrate and automate service validation makes assurance of reliable service delivery possible and simplifies security management tasks for network administrators.