A Formal Model and Verification Problems for Software Defined Networks
https://doi.org/10.18255/1818-1015-2013-6-36-51
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 SDN.
About the Authors
V. A. Zakharov
Lomonosov Moscow State University
Russian Federation
Russian Federation
доцент, Applied Research Center for Computer Networks,
Leninskiye Gory, 1-52, Moscow, GSP-1, 119991, Russia
R. L. Smelyansky
Lomonosov Moscow State University
Russian Federation
Russian Federation
профессор, Applied Research Center for Computer Networks,
Leninskiye Gory, 1-52, Moscow, GSP-1, 119991, Russia
E. V. Chemeritsky
Lomonosov Moscow State University
Russian Federation
Russian Federation
аспирант, Applied Research Center for Computer Networks,
Leninskiye Gory, 1-52, Moscow, GSP-1, 119991, Russia
References
1. OpenFlow Switch Specification. Version 1.4.0, August 5, 2013. www.opennetworking.org.
2. Kim H., Feamster N. Improving network management with software defined networking // Communications Magazine. IEEE, 2013. P. 114—119.
3. Al-Shaer E., Marrero W., El-Atawy A., El Badawi K. Network Configuration in a Box: Toward End-to-End Verification of Network Reachability and Security // 17th IEEE International Conference on Network Protocols (ICNP’09). Princeton, New Jersey, USA, 2009. P. 123—132.
4. Mai H., Khurshid A., Agarwal R., Caesar M., Godfrey R.B., King S.T. Debugging of the Data Plane with Anteater // Proceedings of the ACM SIGCOMM conference. 2011. P. 290—301.
5. Kazemian P., Varghese G., McKeown N. Header space analysis: Static checking for networks // Proceedings of 9-th USENIX Symposium on Networked Systems Design and Implementation. 2012.
6. Khurshid A., Zhou W., Caesar M., Godfrey P.B. VeriFlow: Verifying Network-Wide Invariants in Real Time // Proceedings of International Conference "Hot Topics in Software Defined Networking"(HotSDN). 2012. P. 49—54.
7. Gutz S., Story A., Schlesinger C., Foster N. Splendid isolation: A Slice Abstraction for Software Defined Networks // Proceedings of International Conference "Hot Topics in Software Defined Networking"(HotSDN). 2012. P. 79—84.
8. Reitblatt M., Foster N., Rexford J.,Walker D. Consistent updates for software-defined networks: change you can believe in! // HotNets. 2011. V. 7.
9. Reitblatt M., Foster N., Rexford J., Schlesinger C., Walker D. Abstractions for Network Update // Proceedings of ACM SIGCOMM conference. 2012. P. 323—334.
10. Canini M., Venzano D., Peresini P., Kostic D., Rexford J. A NICE way to Test OpenFlow Applications // Proceedings of Networked Systems Design and Implementation, April 2012.
11. Immerman N. Languages that capture complexity classes // SIAM Journal of Computing. 1987. V. 16, No 4. P. 760—778.
12. Immerman N., Vardi M. Model checking and transitive closure logic // Lecture Notes in Computer Science. 1997. P. 291—302.
13. Alechina N., Immerman N. Reachability logic: efficient fragment of transitive closure logic // Logic Journal of IGPL. 2000. V. 8, No 3. P. 325—337.
14. Galil Z., Hierarchies of Complete Problems // Acta Informatica. 1976. No 6. P. 77—88.
Review
For citations:
Zakharov V.A., Smelyansky R.L., Chemeritsky E.V. A Formal Model and Verification Problems for Software Defined Networks. Modeling and Analysis of Information Systems. 2013;20(6):36-51. (In Russ.) https://doi.org/10.18255/1818-1015-2013-6-36-51
Views:
1161
Email this article 