maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2015-6-735-749mais-291Research ArticleОригинальные статьиArticlesМодель безопасности информационных потоков для программно-конфигурируемых сетейEnd-to-end Information Flow Security Model for Software-Defined NetworksЧалыйД. Ю.ChalyD. Ju.

канд. физ.-мат. наук., доцент,

ул. Советская, 14, г. Ярославль, 150000

PhD, Sovetskaya str., 14, Yaroslavl, 150000

dmitry.chaly@gmail.comНикитинЕ. С.NikitinE. S.

студент,

ул. Советская, 14, г. Ярославль, 150000

student, Sovetskaya str., 14, Yaroslavl, 150000,

nik.zhenya@gmail.comАнтошинаЕ. Ю.AntoshinaE. Ju.

аспирант,

ул. Советская, 14, г. Ярославль, 150000

graduate student, Sovetskaya str., 14, Yaroslavl, 150000

kantoshina@gmai.comСоколовВ. А.SokolovV. A.

доктор физ.-мат. наук, профессор,

ул. Советская, 14, г. Ярославль, 150000

doctor of science, Sovetskaya str., 14, Yaroslavl, 150000,

valery-sokolov@yandex.ruЯрославский государственный университет им. П.Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation201520122015226735749Copyright © Чалый Д.Ю., Никитин Е.С., Антошина Е.Ю., Соколов В.А., 20152015Чалый Д.Ю., Никитин Е.С., Антошина Е.Ю., Соколов В.А.Chaly D.J., Nikitin E.S., Antoshina E.J., Sokolov V.A.Данная работа распространяется под лицензией 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/291

Программно-конфигурируемые сети (ПКС, SDN, Software-defined Networks) являются новой парадигмой организации сетей, которая используется во многих современных приложениях, таких как виртуализация сети, управление доступом на основе политик безопасности и многих других. Программное обеспечение ПКС обеспечивает гибкость и быстрый темп инноваций в сети, однако оно имеет сложную природу, в связи с чем возникает необходимость в средствах обеспечения его корректности и безопасности. Абстрактные модели для ПКС могут решить эти задачи. Данная работа направлена на разработку моделей безопасного взаимодействия в ПКС, акцентируя внимание на таких свойствах безопасности, как конфиденциальность и, частично, целостность. Это критические свойства безопасности многопользовательских сетей, поскольку программное обеспечение, управляющее сетью, должно гарантировать, что конфиденциальные данные одного пользователя не будут переданы другим (нежелательным) пользователям. Мы определили понятие сквозной безопасности в контексте ПКС и предложили семантическую модель, позволяющую сделать обоснованный вывод о соблюдении конфиденциальности, и мы можем проверить, что конфиденциальные информационные потоки не смешиваются с не конфиденциальными. Мы показываем, что модель может быть расширена до обоснования соблюдения конфиденциальности в сетях с безопасными и небезопасными каналами связи, которые могут возникнуть, например, в беспроводных средах.

Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.

Статья публикуется в авторской редакции.

Software-defined networks (SDN) are a novel paradigm of networking which became an enabler technology for many modern applications such as network virtualization, policy-based access control and many others. Software can provide flexibility and fast-paced innovations in the networking; however, it has a complex nature. In this connection there is an increasing necessity of means for assuring its correctness and security. Abstract models for SDN can tackle these challenges. This paper addresses to confidentiality and some integrity properties of SDNs. These are critical properties for multi-tenant SDN environments, since the network management software must ensure that no confidential data of one tenant are leaked to other tenants in spite of using the same physical infrastructure. We define a notion of end-to-end security in context of software-defined networks and propose a semantic model where the reasoning is possible about confidentiality, and we can check that confidential information flows do not interfere with non-confidential ones. We show that the model can be extended in order to reason about networks with secure and insecure links which can arise, for example, in wireless environments.

The article is published in the authors’ wording.

ПКСбезопасностьформальные моделиSDNsecurityformal modelsРФФИ, МинобрнаукиReferencesE. Al-Shaer, S. Al-Haj, “FlowChecker: configuration analysis and verification of federated OpenFlow infrastructures”, SafeConfig 2010 : 2nd ACM Workshop on Assurable and Usable Security Configuration (October 4, 2010, Chicago, IL, USA), 37–44.E. Al-Shaer, S. Al-Haj, “FlowChecker: configuration analysis and verification of federated OpenFlow infrastructures”, SafeConfig 2010 : 2nd ACM Workshop on Assurable and Usable Security Configuration (October 4, 2010, Chicago, IL, USA), 37–44.C. J. Anderson et al., “NetKAT: semantic foundations for networks”, POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (January 22–24, 2014, San Diego, USA), 113–126.C. J. Anderson et al., “NetKAT: semantic foundations for networks”, POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (January 22–24, 2014, San Diego, USA), 113–126.E. Ju. Antoshina et al., “A translator with a security static analysis feature of an information flow for a simple programming language.”, Autom. Control and Comp. Sciences, 48:7 (2014), 589–593.E. Ju. Antoshina et al., “A translator with a security static analysis feature of an information flow for a simple programming language.”, Autom. Control and Comp. Sciences, 48:7 (2014), 589–593.M. Casado, N. Foster, A. Guha, “Abstractions for software-defined networks”, Communications of the ACM, 57:10 (2014), 86–95.M. Casado, N. Foster, A. Guha, “Abstractions for software-defined networks”, Communications of the ACM, 57:10 (2014), 86–95.M. Casado et al., “Ethane: taking control of the enterprise”, ACM SIGCOMM 2007: Data Communications Festival (Augest 27–31, 2007, Kyoto, Japan).M. Casado et al., “Ethane: taking control of the enterprise”, ACM SIGCOMM 2007: Data Communications Festival (Augest 27–31, 2007, Kyoto, Japan).N. Foster et al., “Frenetic: a network programming language”, The 16th ACM SIGPLAN International Conference on Functional Programming (September 19–21, 2011, Tokyo, Japan), 279–291.N. Foster et al., “Frenetic: a network programming language”, The 16th ACM SIGPLAN International Conference on Functional Programming (September 19–21, 2011, Tokyo, Japan), 279–291.S. Gutz et al., “Splendid isolation: a slice abstraction for software-defined networks”, ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (HotSDN) (August 13, 2012, Helsinki, Finland), 2012, 79–84.S. Gutz et al., “Splendid isolation: a slice abstraction for software-defined networks”, ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking (HotSDN) (August 13, 2012, Helsinki, Finland), 2012, 79–84.C.-Y. Hong et al., “Achieving high utilization with software-driven WAN”, ACM SIGCOMM 2013 (August 12 – 16, 2013, Hong Kong, China).C.-Y. Hong et al., “Achieving high utilization with software-driven WAN”, ACM SIGCOMM 2013 (August 12 – 16, 2013, Hong Kong, China).N. McKeown et al., “OpenFlow: enabling innovation in campus networks”, ACM Comp. Comm. Review, 38:2 (2008), 69 – 74.N. McKeown et al., “OpenFlow: enabling innovation in campus networks”, ACM Comp. Comm. Review, 38:2 (2008), 69 – 74.Open Networking Foundation, “OpenFlow switch specification v. 1.4.0”, URL: https://www.opennetworking.org/images/stories/downloads/sdn-resources/onfspecifications/openflow/openflow-spec-v1.4.0.pdf, Last accessed: 10.05.2015.Open Networking Foundation, “OpenFlow switch specification v. 1.4.0”, URL: https://www.opennetworking.org/images/stories/downloads/sdn-resources/onfspecifications/openflow/openflow-spec-v1.4.0.pdf, Last accessed: 10.05.2015.A. Sabelfeld, A.C. Myers, “Language-based information-flow security”, IEEE Journal on Selected Areas in Communications, 21 (2003), 5–19.A. Sabelfeld, A.C. Myers, “Language-based information-flow security”, IEEE Journal on Selected Areas in Communications, 21 (2003), 5–19.R. Smeliansky, “SDN for network security”, Modern Networking Technologies: SDN & NFV – The Next Generation of Computational Infrastructure (October 28–29, 2014, Moscow, Russia), 155–159.R. Smeliansky, “SDN for network security”, Modern Networking Technologies: SDN & NFV – The Next Generation of Computational Infrastructure (October 28–29, 2014, Moscow, Russia), 155–159.D. Zhang et al., “Jif: Java+ information flow”, URL: http://www.cs.cornell.edu/jif/, Last accessed: 10.05.2015.D. Zhang et al., “Jif: Java+ information flow”, URL: http://www.cs.cornell.edu/jif/, Last accessed: 10.05.2015.D. Zhang et al., “A Hardware Design Language for Timing-Sensitive Information-Flow Security”, ASPLOS 2015 : Architectural Support for Programming Languages and Operating Systems (Mar 14 – 18, 2015, Istanbul, Turkey).D. Zhang et al., “A Hardware Design Language for Timing-Sensitive Information-Flow Security”, ASPLOS 2015 : Architectural Support for Programming Languages and Operating Systems (Mar 14 – 18, 2015, Istanbul, Turkey).D. Hedin et al., “JSFlow: Tracking Information Flow in JavaScript and its APIs”, The 29th Symposium On Applied Computing (March 24 – 28, 2014, Gyeongju, Korea), 1663–1671.D. Hedin et al., “JSFlow: Tracking Information Flow in JavaScript and its APIs”, The 29th Symposium On Applied Computing (March 24 – 28, 2014, Gyeongju, Korea), 1663–1671.O. Arden et al., “Sharing Mobile Code Securely With Information Flow Control”, IEEE Symp. on Security and Privacy (SP), 2012, 191–205.O. Arden et al., “Sharing Mobile Code Securely With Information Flow Control”, IEEE Symp. on Security and Privacy (SP), 2012, 191–205.A. Cheung et al., “Using Program Analysis to Improve Database Applications”, IEEE Data Eng. Bull., 37:1 (2014), 48–59.A. Cheung et al., “Using Program Analysis to Improve Database Applications”, IEEE Data Eng. Bull., 37:1 (2014), 48–59.

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