A security policy model transformation and verification approach for software defined networking

Software-defined networking (SDN) has been increasingly utilized to enforce the security of complex networks. However SDN-based security enforcement mechanisms rely heavily on some specific security policies containing underlying network information. Facing the increasingly complex and huge SDN networks, we urgently need a novel security policy management mechanism which can be completely transparent to any underlying network information. That is it can permit network managers to define the high-level security policy model without containing any underlying information, and by means of model transformation, high-level security policy model can be automatically transformed into its corresponding lower-level security policy model containing underlying information. Moreover, we must ensure the system model of data plane updated by the low-level security policy model can hold all of security properties defined in high-level security policy model. Based on these insights, we propose a security policy model transformation and verification approach for SDN in this paper. We first specify the security policies used in SDN networks as a formal security policy model (SPM). Then we establish the system model of SDN's data plane and the mapping rules between the policy objects of SPM and the system objects of system model of data plane. Based on these mapping rules, we propose a security policy model transformation mechanism which transforms SPM into the low-level security policy model, RSPM. In order to verify the system model of data plane updated by RSPM can hold all of security properties defined in SPM, we propose a security policy verification mechanism based on model checking techniques and a group of validation conditions. Finally, we utilize a comprehensive case to illustrate the feasibility of this approach. (C) 2020 Elsevier Ltd. All rights reserved.