maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-6-36-51mais-156Research ArticleОригинальные статьиArticlesФормальная модель и задачи верификации программно-конфигурируемых сетейA Formal Model and Verification Problems for Software Defined NetworksЗахаровВладимир АнатольевичZakharovV. A.

Центр прикладных исследований компьютерных сетей, доцент,

119991, Москва, ГСП-1, Ленинские горы, д. 1, стр. 52

доцент, Applied Research Center for Computer Networks,

Leninskiye Gory, 1-52, Moscow, GSP-1, 119991, Russia

zakh@cs.msu.suСмелянскийРуслан ЛеонидовичSmelyanskyR. L.

Центр прикладных исследований компьютерных сетей, профессор,

119991, Москва, ГСП-1, Ленинские горы, д. 1, стр. 52

профессор, Applied Research Center for Computer Networks,

Leninskiye Gory, 1-52, Moscow, GSP-1, 119991, Russia

rsmeliansky@arccn.ruЧемерицкийЕвгений ВикторовичChemeritskyE. V.

Центр прикладных исследований компьютерных сетей, аспирант,

119991, Москва, ГСП-1, Ленинские горы, д. 1, стр. 52

аспирант, Applied Research Center for Computer Networks,

Leninskiye Gory, 1-52, Moscow, GSP-1, 119991, Russia

echemeritskiy@arccn.ruМосковский государственный университет им. М.В. ЛомоносоваРоссияLomonosov Moscow State UniversityRussian Federation2013201220132063651Copyright © Захаров В.А., Смелянский Р.Л., Чемерицкий Е.В., 20132013Захаров В.А., Смелянский Р.Л., Чемерицкий Е.В.Zakharov V.A., Smelyansky R.L., Chemeritsky E.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/156

Программно-коммутируемые сети (ПКС) — это класс компьютерных телекоммуникационных сетей, появившийся несколько лет назад в стремлении упростить проектирование и повысить гибкость управления сетями за счет разделения потоков данных (пакетов) и потоков управления (сообщений и команд), циркулирующих в сетях. ПКС представляет собой распределенную систему, в которой один или несколько контроллеров управляют множеством сетевых коммутаторов, обеспечивающих продвижение пакетов по каналам сети. Функциональные возможности и порядок взаимодействия коммутаторов и контроллеров ПКС определяются протоколом OpenFlow. На основе аппарата булевых функций и дискретных преобразователей нами предложена формальная модель ПКС, введен прототип формального языка спецификаций, поставлены задачи верификации моделей ПКС и получены оценки их сложности. Для одной из задач верификации моделей ПКС описан метод ее решения, на основе которого разработано программно-инструментальное средство верификации ПКС.

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.

программно-конфигурируемая сетькоммутаторконтроллерправило коммутациипакетформальная модельспецификацияверификация моделейsoftware defined networkswitchcontrollerforwarding rulepacketformal modelspecificationmodel checkingРФФИ, фонд «Сколково»ReferencesOpenFlow Switch Specification. Version 1.4.0, August 5, 2013. www.opennetworking.org.OpenFlow Switch Specification. Version 1.4.0, August 5, 2013. www.opennetworking.org.Kim H., Feamster N. Improving network management with software defined networking // Communications Magazine. IEEE, 2013. P. 114—119.Kim H., Feamster N. Improving network management with software defined networking // Communications Magazine. IEEE, 2013. P. 114—119.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.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.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.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.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.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.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.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.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.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.Reitblatt M., Foster N., Rexford J.,Walker D. Consistent updates for software-defined networks: change you can believe in! // HotNets. 2011. V. 7.Reitblatt M., Foster N., Rexford J.,Walker D. Consistent updates for software-defined networks: change you can believe in! // HotNets. 2011. V. 7.Reitblatt M., Foster N., Rexford J., Schlesinger C., Walker D. Abstractions for Network Update // Proceedings of ACM SIGCOMM conference. 2012. P. 323—334.Reitblatt M., Foster N., Rexford J., Schlesinger C., Walker D. Abstractions for Network Update // Proceedings of ACM SIGCOMM conference. 2012. P. 323—334.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.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.Immerman N. Languages that capture complexity classes // SIAM Journal of Computing. 1987. V. 16, No 4. P. 760—778.Immerman N. Languages that capture complexity classes // SIAM Journal of Computing. 1987. V. 16, No 4. P. 760—778.Immerman N., Vardi M. Model checking and transitive closure logic // Lecture Notes in Computer Science. 1997. P. 291—302.Immerman N., Vardi M. Model checking and transitive closure logic // Lecture Notes in Computer Science. 1997. P. 291—302.Alechina N., Immerman N. Reachability logic: efficient fragment of transitive closure logic // Logic Journal of IGPL. 2000. V. 8, No 3. P. 325—337.Alechina N., Immerman N. Reachability logic: efficient fragment of transitive closure logic // Logic Journal of IGPL. 2000. V. 8, No 3. P. 325—337.Galil Z., Hierarchies of Complete Problems // Acta Informatica. 1976. No 6. P. 77—88.Galil Z., Hierarchies of Complete Problems // Acta Informatica. 1976. No 6. P. 77—88.

The authors declare that there are no conflicts of interest present.