Testbeds and Research Infrastructures for the Development of Networks and Communications. 13th EAI International Conference, TridentCom 2018, Shanghai, China, December 1-3, 2018, Proceedings

Research Article

Automated and Optimized Formal Approach to Verify SDN Access-Control Misconfigurations

  • @INPROCEEDINGS{10.1007/978-3-030-12971-2_6,
        author={Amina Sa\~{a}daoui and Nihel Ben Youssef Ben Souayeh and Adel Bouhoula},
        title={Automated and Optimized Formal Approach to Verify SDN Access-Control Misconfigurations},
        proceedings={Testbeds and Research Infrastructures for the Development of Networks and Communications. 13th EAI International Conference, TridentCom 2018, Shanghai, China, December 1-3, 2018, Proceedings},
        proceedings_a={TRIDENTCOM},
        year={2019},
        month={2},
        keywords={Flow entries Flow table SDN Misconfigurations FtDD Inference system Direct path Firewall},
        doi={10.1007/978-3-030-12971-2_6}
    }
    
  • Amina Saâdaoui
    Nihel Ben Youssef Ben Souayeh
    Adel Bouhoula
    Year: 2019
    Automated and Optimized Formal Approach to Verify SDN Access-Control Misconfigurations
    TRIDENTCOM
    Springer
    DOI: 10.1007/978-3-030-12971-2_6
Amina Saâdaoui1,*, Nihel Ben Youssef Ben Souayeh1,*, Adel Bouhoula1,*
  • 1: Sup’Com, University of Carthage
*Contact email: amina.saadaoui@supcom.tn, nihel.benyoussef@supcom.tn, adel.bouhoula@supcom.tn

Abstract

Software-Defined Networking (SDN) brings a significant flexibility and visibility to networking, but at the same time creates new security challenges. SDN allows networks to keep pace with the speed of change by facilitating frequent modifications to the network configuration. However, these changes may introduce misconfigurations by writing inconsistent rules for Flow-tables. Misconfigurations can arise also between firewalls and Flow-tables in OpenFlow-based networks. Problems arising from these misconfigurations are common and have dramatic consequences for networks operations. Therefore, there is a need of automatic methods to detect and fix these misconfigurations. Given these issues, some methods have been proposed. Though these methods are useful for managing Flow-tables rules, they still have limitations in term of low granularity level and the lack of precise details of analyzed flow entries. To address these challenges, we present in this paper a formal approach that allows to discover Flow-tables misconfigurations using inference systems. The contributions of our work are the following: automatically identifying Flow-tables anomalies, using the Firewall to bring out real misconfigurations and proposing automatic method to deal with set-field action of flow entries.