Toward Automated Attack Discovery in SDN Controllers Through Formal Verification

Software Defined Networking (SDN) is a new networking paradigm that separates the control plane and the data plane. This allows to manage, program and scale networks from one place. While SDN increases network flexibility and usability, it also opens new attack surfaces due to the presence of centralised controllers and protocol weaknesses. OpenFlow communication is used between controllers and switches in many current SDN deployments. It can show problems in packet processing, topology discovery and rule installation. Conventional security techniques depend on manual evaluations or reactive defenses that detect threats only after they have been exploited. In this paper we introduce an Automated Attack Discovery Framework for SDN Controllers using Formal Verification methodologies. The proposed system models controllers, switches, hosts and their interactions with math, and automatically verifies security properties. The framework identifies possible attack paths from the bad hosts or hacked switches. Testing shows that the method can discover multiple vulnerabilities and attack scenarios, including novel ones. The proposed approach improves proactive security analysis, network reliability, and resilience for modern SDN environments.