Preserving Confidentiality during the Migration of Virtual SDN Topologies: A Formal Approach

Network virtualization provides a flexible solution to reduce costs, share network resources and improve recovery time upon failure. An important part of virtual network management consists in migrating them in order to optimize resource allocation and react to link failures. However, the migration process might entail the loss of security properties in the virtual network, such as confidentiality. In this paper, we present the first approach combining formal models and virtualization to prove confidentiality preservation during the migration process. We describe the network environment, the migration process and the confidentiality with a set of logical predicates that will be used by SNARK to obtain the formal proof of the preservation. We validate our theoretical approach by exhibiting confidentiality violation detection on an illustrative use case.