Process Algebra Based Symbolic Verification Framework for Software-Defined Networking

Abstract

There have been continuous efforts and progresses regarding the research on the verification for Software Defined Networks (SDN), since incomplete or malicious programmable SDN entities could cause break-down of underlying networks shared by heterogeneous devices and stake-holders. In SDN world, it becomes important to verify the safety properties of SDN using formal method before the deployment of SDN applications. In this paper, we propose VeriSDN, a novel framework for the symbolic verification of SDN based on the formal method, especially with process algebra called pACSR which is an extended version of packet based Algebra of Communicating Shared Resources (ACSR). In our framework, OpenFlow’s flow tables are translated into pACSR descriptions and analyzed by means of a symbolic algorithm. The result will be the Boolean expression that satisfies when the property holds. pACSR processes are well suited to expresses concurrently running communicating switches and a controller. Packets in SDN can be described in pACSR as parameters passed via channels and handled with predefined predicates (PP) and be modified with predefined functions (PF). Even though our method is developed mainly for verification of the off-line case where flow tables are dynamically modified, however, we believe that it can be applied to the running switches with reasonable numbers. Furthermore, our method is transparent to the operators so the underlying verification process is hidden to the operators and there is no burden to understand the details of formal verification method by the operators.