End-to-end information flow security model for software-defined networks

Программно-конфигурируемые сети (ПКС, SDN, Software-defined Networks) являются новой парадигмой организации сетей, которая используется во многих современных приложениях, таких как виртуализация сети, управление доступом на основе политик безопасности и многих других. Программное обеспечение ПКС обеспечивает гибкость и быстрый темп инноваций в сети, однако оно имеет сложную природу, в связи с чем возникает необходимость в средствах обеспечения его корректности и безопасности. Абстрактные модели для ПКС могут решить эти задачи. Данная работа направлена на разработку моделей безопасного взаимодействия в ПКС, акцентируя внимание на таких свойствах безопасности, как конфиденциальность и, частично, целостность. Это критические свойства безопасности многопользовательских сетей, поскольку программное обеспечение, управляющее сетью, должно гарантировать, что конфиденциальные данные одного пользователя не будут переданы другим (нежелательным) пользователям. Мы определили понятие сквозной безопасности в контексте ПКС и предложили семантическую модель, позволяющую сделать обоснованный вывод о соблюдении конфиденциальности, и мы можем проверить, что конфиденциальные информационные потоки не смешиваются с не конфиденциальными. Мы показываем, что модель может быть расширена до обоснования соблюдения конфиденциальности в сетях с безопасными и небезопасными каналами связи, которые могут возникнуть, например, в беспроводных средах.
Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.
Статья публикуется в авторской редакции.