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.
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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)
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)
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)
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)
All-in-one sdn app development starter vm (2018)
Cisco open network environment for government (2018)
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)
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)
Gouda, M.G., Liu, A.X.: Structured firewall design. Comput. Netw. 51(4), 1106–1120 (2007)
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)
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)
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)
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)
Limboole sat solver (2018)
Liu, A.X., Gouda, M.G.: Diverse firewall design. IEEE Trans. Parallel Distrib. Syst. (TPDS) 19(8), 1237–1251 (2008)
McKeown, N., et al.: Openflow: enabling innovation in campus networks. Comput. Commun. Rev. 38(2), 69–74 (2008)
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)
Saâdaoui, A., Ben Youssef Ben Souayeh, N., Bouhoula, A.: FARE: fdd-based firewall anomalies resolution tool. J. Comput. Sci. 23, 181–191 (2017)
Wundsam, A., Levin, D., Seetharaman, S., Feldmann, A.: Ofrewind: enabling record and replay troubleshooting for networks. In: USENIX Annual Technical Conference. USENIX Association (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering
About this paper
Cite this paper
Saâdaoui, A., Ben Youssef Ben Souayeh, N., Bouhoula, A. (2019). Automated and Optimized Formal Approach to Verify SDN Access-Control Misconfigurations. In: Gao, H., Yin, Y., Yang, X., Miao, H. (eds) Testbeds and Research Infrastructures for the Development of Networks and Communities. TridentCom 2018. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol 270. Springer, Cham. https://doi.org/10.1007/978-3-030-12971-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-12971-2_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-12970-5
Online ISBN: 978-3-030-12971-2
eBook Packages: Computer ScienceComputer Science (R0)