Formal Modelling and Analysis of Man in The Middle Prevention Control in Software Defined Network

Resumo

The Man-in-the-Middle (MITM) attack is still considered a threat to networks. On the other hand, Software-Defined Networks (SDN) has been gaining market space, precisely because of the ability to dynamically manipulate data flows through a programmable interface. Colored Petri Nets (CPN) are considered a proper tool for modeling distributed systems and security controls. The objective of this work is, using CPN, model and analysis a security control in SDN that could detect and correct the Man-In-The-Middle (MITM) attacks based on ARP spoofing. This goal is achieved modeling a SDN, a MITM attack and the proposed security control to reach a complete state space analysis. The state space analysis showed that a MITM attack is possible in a SDN environment increasing the number of possible states in 67%. The proposed security control could detect and correct the packets generated with forged data, preventing the attack, and decreasing by 96.22% the number of possible states while the SDN is under attack. Thus, this work obtained an effective security control to avoid MITM attacks based on ARP spoofing, did not falling on the main limitations presented in the previous solutions to avoid MITM attacks in traditional networks, such as: the existence of single point of failures or the need to update or patch the ARP protocol or system’s kernel at the devices connected to the network.