Abstract
Software Defined Networking (SDN) is an approach to building computer networks that separate and abstract data planes and control planes of these systems. In a SDN a centralized controller manages a distributed set of switches. A set of open commands for packet forwarding and flow table updating was defined in the form of a protocol known as OpenFlow. In this paper we describe an abstract formal model of SDN, introduce a tentative language for specification of SDN forwarding policies, and set up formally model-checking problems for SDNs.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Open Flow Switch Specification. Version 1.4.0, 2013. www.opennetworking.org
Kim, H. and Feamster, N., Improving network management with software defined networking, Commun. Mag. IEEE, 2013, vol. 51, no. 2, pp. 114–119.
Al-Shaer, E., Marrero, W., El-Atawy, A., and El Badawi, K., Network configuration in a box: Toward end-to-end verification of network reachability and security, Proc. 17th IEEE Int. Conf. on Network Protocols (ICNP’09), Princeton, USA, 2009, pp. 123–132.
Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, R.B., and King, S.T., Debugging of the data plane with anteater, Proc. Assoc. for Compt. Mach. SIGCOMM Conf., 2011, pp. 290–301.
Kazemian, P., Varghese, G., and McKeown, N., Header space analysis: Static checking for networks, Proc. 9th USENIX Symp. on Networked Systems Design and Implementation 2012.
Khurshid, A., Zhou, W., Caesar, M., and Godfrey, P.B., VeriFlow: Verifying network-wide invariants in real time, Proc. Int. Conf. “Hot Topics in Software Defined Networking” (HotSDN), 2012, pp. 49–54.
Gutz, S., Story, A., Schlesinger, C, and Foster, N., Splendid isolation: A slice abstraction for software defined networks, Proc. Int. Conf. “Hot Topics in Software Defined Networking”(HotSDN), 2012, pp. 79–84.
Reitblatt, M., Foster, N., Rexford, J., and Walker, D., Consistent updates for software-defined networks: Change you can believe in!, HotNets, 2011, vol. 7.
Reitblatt, M., Foster, N., Rexford, J., Schlesinger, C., and Walker, D., Abstractions for network update, Proc. Assoc. for Compt. Mach. SIGCOMM Conf., 2012, pp. 323–334.
Canini, M., Venzano, D., Peresini, P., Kostic, D., and Rexford, J., A NICE way to test Open Flow applications, Proc. Networked Systems Design and Implementation, 2012.
Immerman, N., Languages that capture complexity classes, SIAM J. Compt., 1987, vol. 16, pp. 760–778.
Immerman, N. and Vardi, M., Model checking and transitive closure logic, Lect. Notes Compt. Sci., 1997, vol. 1254, pp. 291–302.
Alechina, N. and Immerman, N., Reachability logic: efficient fragment of transitive closure logic, Logic J. IGPL, 2000, vol. 8, pp. 325–337.
Galil, Z., Hierarchies of complete problems, Acta Informatica, 1976, no. 6, pp. 77–88.
Author information
Authors and Affiliations
Corresponding author
Additional information
Published in Russian in Modelirovanie i Analiz Informatsionnykh Sistem, 2013, No. 6, pp. 36–51.
The article was translated by the authors.
About this article
Cite this article
Zakharov, V.A., Smelyansky, R.L. & Chemeritsky, E.V. A formal model and verification problems for software defined networks. Aut. Control Comp. Sci. 48, 398–406 (2014). https://doi.org/10.3103/S0146411614070165
Received:
Published:
Issue Date:
DOI: https://doi.org/10.3103/S0146411614070165