Abstract: Software-defined network gives programmability to the network,reduces the complexity of network management,and promotes the development of new network technology.As a device for data forwarding and policy enforcement,the permissions of SDN switches should not be stolen by unauthorized entities.However,the SDN switch does not always execute the commands issued by the controller.Malicious attackers attack the network covertly and fatally by eroding the SDN switch,which seriously affects the end-to-end communication quality of users.Communicationsequential process(CSP),as a modeling language designed for concurrent systems,can accurately describe the interaction between SDN switch-switch and switch-host.In this paper,CSP is used to model SDN switch and terminal host,and two abnormal switch location methods are analyzed theoretically.We verify the effectiveness of the two detection methods in the instantiated model system when the edge switch is maliciously forwarded as an egress switch,and the authentication results show that the abnormal behavior cannot be detected.In order to solve this problem,an anomaly detection method for edge switch is proposed in this paper.In this method,the host records the statistical information and triggers the packet_in message to complete the information transmission with the controller by constructing a special packet.The controller collects the statistical information and detects the abnormal forwarding behavior of the edge switch by analyzing the statistical information consistency between the edge switch and the host.Finally,based on the ryu controller,experiments are carried out on the mininet platform,and experimental results show that the edge switch anomaly detection method can successfully detect abnormal behavior.

Key words: Software defined network, Data plane security, Formal authentication and analysis, Communication sequence process, Damaged switch detection