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

  • Amina SaâdaouiEmail author
  • Nihel Ben Youssef Ben Souayeh
  • Adel Bouhoula
Conference paper
Part of the Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering book series (LNICST, volume 270)


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.

These techniques have been implemented and we proved the correctness of our method and demonstrated its applicability and scalability. The first results we obtained are very promising.


Flow entries Flow table SDN Misconfigurations FtDD Inference system Direct path Firewall 


  1. 1.
    Al-Shaer, E., Al-Haj, S.: Flowchecker: configuration analysis and verification of federated openflow infrastructures. In: 3rd ACM Workshop on Assurable and Usable Security Configuration, SafeConfig 2010, Chicago, IL, USA, 4 October 2010, pp. 37–44 (2010)Google Scholar
  2. 2.
    Alimi, R., Wang, Y., Yang, Y.R.: Shadow configuration as a network management primitive. In: Proceedings of the ACM SIGCOMM 2008 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Seattle, WA, USA, 17–22 August 2008, pp. 111–122 (2008)Google Scholar
  3. 3.
    Ball, T.: Vericon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 09–11 June 2014, pp. 282–293 (2014)CrossRefGoogle Scholar
  4. 4.
    Canini, M., Venzano, D., Peresíni, P., Kostic, D., Rexford, J.: A NICE way to test openflow applications. In: Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2012, San Jose, CA, USA, 25–27 April 2012, pp. 127–140 (2012)Google Scholar
  5. 5.
    All-in-one sdn app development starter vm (2018)Google Scholar
  6. 6.
    Cisco open network environment for government (2018)Google Scholar
  7. 7.
    Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis (awarded best paper). In: Proceedings of 2nd Symposium on Networked Systems Design and Implementation (NSDI 2005), Boston, Massachusetts, USA, 2–4 May 2005 (2005)Google Scholar
  8. 8.
    Foster, B., et al.: Frenetic: a network programming language. In: Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, 19–21 September 2011, pp. 279–291 (2011)Google Scholar
  9. 9.
    Gouda, M.G., Liu, A.X.: Structured firewall design. Comput. Netw. 51(4), 1106–1120 (2007)CrossRefGoogle Scholar
  10. 10.
    Griffin, T., Wilfong, G.T.: On the correctness of IBGP configuration. In: Proceedings of the ACM SIGCOMM 2002 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, 19–23 August 2002, Pittsburgh, PA, USA, pp. 17–29 (2002)Google Scholar
  11. 11.
    Hu, H., Han, W., Ahn, G.-J., Zhao, Z.: FLOWGUARD: building robust firewalls for software-defined networks. In: Proceedings of the Third Workshop on Hot Topics in Software Defined Networking, HotSDN 2014, Chicago, Illinois, USA, 22 August 2014, pp. 97–102 (2014)Google Scholar
  12. 12.
    Kazemian, P., Chan, M., Zeng, H., Varghese, G., McKeown, N., Whyte, S.: Real time network policy checking using header space analysis. In: NSDI, pp. 99–111. USENIX Association (2013)Google Scholar
  13. 13.
    Khurshid, A., Zou, X., Zhou, W., Caesar, M., Brighten Godfrey, P.: Veriflow: verifying network-wide invariants in real time. In: Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Lombard, IL, USA, 2–5 April 2013, pp. 15–27 (2013)Google Scholar
  14. 14.
    Limboole sat solver (2018)Google Scholar
  15. 15.
    Liu, A.X., Gouda, M.G.: Diverse firewall design. IEEE Trans. Parallel Distrib. Syst. (TPDS) 19(8), 1237–1251 (2008)CrossRefGoogle Scholar
  16. 16.
    McKeown, N., et al.: Openflow: enabling innovation in campus networks. Comput. Commun. Rev. 38(2), 69–74 (2008)CrossRefGoogle Scholar
  17. 17.
    Saadaoui, A., Ben Youssef Ben Souayeh, N., Bouhoula, A.: Formal approach for managing firewall misconfigurations. In: IEEE 8th International Conference on Research Challenges in Information Science, RCIS 2014, Marrakech, Morocco, 28–30 May 2014, pp. 1–10 (2014)Google Scholar
  18. 18.
    Saâdaoui, A., Ben Youssef Ben Souayeh, N., Bouhoula, A.: FARE: fdd-based firewall anomalies resolution tool. J. Comput. Sci. 23, 181–191 (2017)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Wundsam, A., Levin, D., Seetharaman, S., Feldmann, A.: Ofrewind: enabling record and replay troubleshooting for networks. In: USENIX Annual Technical Conference. USENIX Association (2011)Google Scholar

Copyright information

© ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2019

Authors and Affiliations

  • Amina Saâdaoui
    • 1
    Email author
  • Nihel Ben Youssef Ben Souayeh
    • 1
  • Adel Bouhoula
    • 1
  1. 1.Digital Security Research LabSup’Com, University of CarthageTunisTunisia

Personalised recommendations