автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Исследование методов контроля функционирования программно-конфигурируемых сетей

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

Факультет вычислительной математики и кибернетики

ИССЛЕДОВАНИЕ МЕТОДОВ КОНТРОЛЯ ФУНКЦИОНИРОВАНИЯ ПРОГРАММНО-КОНФИГУРИРУЕМЫХ СЕТЕЙ

05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

имени М.В. Ломоносова

На правах рукописи

Чемерицкий Евгений Викторович

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

МОСКВА-2015

005561950

Работа выполнена на кафедре автоматизации систем вычислительных комплексов факультета вычислительной математики и кибернетики Федерального государственного бюджетного образовательного учреждения высшего образования «Московский государственный университет имени М. В. Ломоносова».

Научный руководитель: доктор физико-математических наук,

член-корреспондент РАН, заведующий Лабораторией вычислительных комплексов факультета вычислительной математики и кибернетики Федерального государственного бюджетного образовательного учреждения высшего образования «Московский государственный университет имени М. В. Ломоносова», профессор Смелянский Руслан Леонидович.

Официальные оппоненты: Доктор физико-математических наук,

профессор департамента программной инженерии факультета компьютерных наук Федерального государственного автономного образовательного учреждения высшего профессионального образования «Национальный исследовательский университет «Высшая школа экономики» Ломазова Ирина Александровна

Доктор технических наук, заведующий кафедрой Вычислительной техники института автоматики и вычислительной техники «Национальный исследовательский университет «Московский энергетический институт», профессор Топорков Виктор Васильевич

Ведущая организация: Федеральное государственное автономное

образовательное учреждение высшего образования «Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики»

Защита диссертации состоится "25 "С&ГГЯБРЯ 2015 г. в Л часов на заседании диссертационного совета Д 501.001.44 при Московском государственном университете имени М.В.Ломоносова по адресу: 119991, ГСП-1, Москва, Ленинские горы, МГУ, 2-й учебный корпус, факультет вычислительной математики и кибернетики, аудитория 685.

С диссертацией можно ознакомиться в Научной библиотеке Московского государственного университета имени М.В. Ломоносва по адресу: 119192, г. Москва, Ломоносовский проспект, д. 27 - а так же на официальном сайте факультета ВМК МГУ http://www.cmc.msu.ru в разделе «Диссертации».

Автореферат разослан " " Я^Ъ^СГ/}_20/£г.

Ученый секретарь

диссертационного совета Д 501.001.44 доктор физико-математических наук, доцент

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы диссертации

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

Коммутаторы ПКС представляют собой очень простые устройства в сравнении с роутерами и коммутаторами традиционных сетей. Они лишь исполняют инструкции по обработке проходящих через них пакетов данных, которые контроллер динамически формирует и загружает в них. Они не содержат программного обеспечения, реализующего стек протоколов TCP/IP. Тем самым контроллер получает возможность гранулярной настройки поведения каждого ПКС коммутатора, а сам коммутатор избавляется от множества служебных протоколов, предназначенных, прежде всего, для согласования работы коммутационного оборудования.

Работа посвящена исследованию ПКС, в которых взаимодействие между контроллером и подключёнными к нему коммутаторами обеспечивается протоколом OpenFlow. Низкоуровневые абстракции этого протокола позволяют контроллеру устанавливать и удалять правила обслуживания пакетов непосредственно. Тем самым, OpenFlow освобождает сетевых инженеров от необходимости распутывать нетривиальные зависимости между настроечными параметрами и поведением оборудования, что существенно упрощает администрирование сети.

Перечисленные особенности ПКС и OpenFlow позволили описывать поведение коммутационных устройств набором установленных в них правил обслуживания пакетов и одновременно ограничили изменения конфигурации сети воздействиями контроллера. В результате у исследователей появилась удобная возможность для наблюдения за глобальным состоянием сети, что стимулировало развитие и применение формальных методов для анализа компьютерных сетей.

Настоящая работа посвящена исследованиям в области одного из наиболее многообещающих и востребованных на практике направлений использования формальных методов в контексте ПКС - проверке соответствия поведения ПК С требованиям политик маршрутизации. В работе рассматривается два разных класса требований и соответствующих им свойств ПКС: логические свойства правил маршрутизации пакетов в масштабах сети, а так же максимальное время передачи пакетов по заданному маршруту с учётом взаимного влияния потоков друг на друга.

Цель работы

Целью данной работы является исследование и разработка методов и средств для оценки свойств ПКС по известной конфигурации ей компонентов и проверке соответствия этих свойств предъявляемым к ней требованиям политик маршрутизации.

Для достижения поставленной цели необходимо решить следующие задачи:

• Предложить формальный язык для спецификации политик маршрутизации, выражающих свойства достижимости в пространстве состояний пакетов;

• Построить математическую модель ПКС и алгоритм для проверки модельного представления ПКС на соответствие спецификациям предложенного языка;

• Разработать математическую модель ПКС и алгоритм оценки для максимальной сквозной задержки при передаче пакетов через инфраструктуру сети;

• Выполнить программную реализацию и провести экспериментальное исследование предложенных алгоритмов.

Основные результаты работы

Основные результаты диссертационной работы следующие:

1. Разработаны язык спецификации политик маршрутизации и реляционная модель поведения ПКС, в рамках которой строго описана семантика этого языка. Впервые было показано, что для задания статических свойств ПКС достаточно логики первого порядка с оператором транзитивного замыкания;

2. Построен алгоритм проверки соответствия конфигурации ПКС заданному множеству политик маршрутизации, для которого определена структура данных, позволяющая эффективно представлять отношения, моделирующие поведение ПКС;

3. Построена математическая модель функционирования ПКС с временем, в рамках которой поставлена задача и построены алгоритмы вычисления верхней оценки задержки передачи пакетов через последовательность коммутаторов с учётом текущей нагрузки на сеть;

4. Все разработанные алгоритмы были реализованы и прошли экспериментальную апробацию.

Научная новизна

Впервые формализм логики первого порядка, дополненной оператором транзитивного замыкания, был использован в качестве языка для спецификации свойств достижимости в ПКС. Для данного языка были разработаны оригинальные методы проверки соответствия конфигурации ПКС его произвольным спецификациям;

Для исследуемого класса сетей впервые был предложен алгоритм вычисления достижимой верхней оценки для задержки передачи пакета, обладающий полиномиальной сложностью.

Практическая ценность

Результаты настоящей работы могут быть использованы в качестве базы для разработки новых методов и средств исследования разнообразных свойств компьютерных сетей по их конфигурациям. Распространение инструментальных средств указанного вида способно снизить затраты на обслуживания сетей и повысить продуктивность сетевых администраторов, наделив их возможностью заблаговременно выявлять несоответствия между настройками сетевого оборудования и требованиями, предъявляемыми к поведению сети. Полученные в работе результаты могут быть рекомендованы к использованию при проектировании и модернизации вычислительных систем реального времени.

Методы исследования

При получении основных результатов работы использовались методы математической логики, формальной верификации, теории сетевого исчисления (network calculus), а так же линейного программирования.

Апробация работы

Результаты работы докладывались на научно-исследовательском семинаре кафедры автоматизации систем вычислительных комплексов (АСВК) факультета ВМК МГУ, на научном семинаре лаборатории вычислительных комплексов кафедры АСВК, а также на следующих конференциях:

1. IV международном семинаре «Программные семантики, спецификации и верификация (PSSV-2013)» (Екатеринбург, 2013);

2. Международной научной конференции «Управление и виртуализация в современных сетях (Сети 2014: SDN & NFV)» (Москва, 2014);

3. Международной научно-практической конференции «Инструменты и методы анализа программ (ТМРА-2014)» (Кострома, 2014);

4. Международном семинаре «Formal Foundations for Networking (Dagstuhl Seminar 15071)» (Дапшуль, 2015).

Публикации

По теме диссертации опубликовано 11 печатных работ, в том числе 3 работы в журналах «Моделирование и анализ информационных систем» (МАИС) и «Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление», входящих в перечень ведущих рецензируемых научных журналов ВАК РФ, а также 5 работ, индексируемых системой Scopus. Список работ приведен в конце автореферата.

Структура и объём диссертации

Диссергация состоит из введения, двух глав, заключения, трёх приложений и списка литературы. Объём работы - 200 страниц. Список литературы содержит 131 наименование.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ Во введении обоснована актуальность диссертационной работы и дано краткое описание задачи.

В первой главе представлены результаты исследований м его до в и средств проверки соответствия правил передачи пакетов в сети требованиям политик

маршрутизации. В этой главе описано устройство ПКС сети, Open Flow протокол и взаимодействие контроллера с ПКС коммутаторами; дана классификация свойств ПКС и приведены примеры типичных политик маршрутизации. Свойства ПКС подразделяются на локальные и глобальные, статические и динамические. Среди динамических свойств ПКС особо выделяются свойства дискретного и реального времени.

Приведен обзор формальных языков, применяемых для описания свойств распределённых вычислительных систем: темпоральные логики CTL, LTL и CTL*, а так же пропозициональное ^-исчисление. Дополнительно рассмотрена логика первого порядка с оператором транзитивного замыкания FO[TC], который оказался удобным для описания разнообразных свойств достижимости. По результатам обзора сделан вывод о перспективности логики транзитивного замыкания FO[TC] для описания статических свойств ПКС, и темпоральной логики линейного времени LTL - для описания динамических свойств ПКС.

Проведён обзор формализмов, подходящих для построения модели ПКС. По итогам проведённого обзора простейшие компоненты ПКС, пакеты и шаблоны применяющихся к ним правил обслуживания - было предложено представлять булевыми наборами. Правила обработки пакетов, реализованных текущей конфигурацией ПКС - отношениями преобразования булевых наборов, выражающих состояния пакетов в сети. В качестве наиболее перспективного представления для таких отношений были выбраны упорядоченные двоичные решающие диаграммы OBDD. Для описания поведения ПКС построенная реляционная модель конфигурации сети дополнена конечным автоматом, описывающим поведение контроллера.

По результатам проведённых обзоров было разработано две математических модели ПКС: статической и динамической.

Статическая модель ПКС предназначена для описания сети коммутаторов с заданными таблицами правил OpenFlow. Эта модель не охватывает контроллер и не учитывает возможность изменения таблиц коммутации.

В рамках статической модели ПКС для описания заголовков пакетов, номеров портов и уникальных имен коммутаторов используются двоичные векторы вида h = (/ilfh2, , р = (Po>Pi>—>Pk) и w = (yt^v/z, ...,wm)

соответственно. Для обозначения отдельных элементов векторов используются квадратные скобки, например, h[i] = fy.

Если начальный бит номера коммутатора равен единице р[0] = 1, то такой порт называется входным, иначе - выходным портом коммутатора. Множества всех заголовков, входных, выходных и всех портов, а так же уникальных имён коммутаторов обозначаются записями Ж, IT, OP, Уи W соответственно.

Выходной порт р = (0,0,...,0) считается портом для сброса пакетов и обозначать записью drop. Выходной порт р = (0,1,1,..., 1) считается выходным портом управления и обозначается записью octr - через этот порт коммутатор направляет сообщения контроллеру. Порт р = (1,1,1,..., 1) - это входной порт канала управления. Он обозначается записью Ictr, и через этот порт коммутатор получает команды от контроллера.

Пары (h, р), h £ Jf, р е Т называются локальными состояниями пакетов, а пары вида (p,w),p 6 - точками сети. Тройки (h,p,w),h 6Jf,p £

Р, w £ W называются (глобальными) состояниями пакетов. Для обозначения множества глобальных состояний пакетов используется символ S.

Шаблоном заголовка называется троичный вектор z = (avo2, —>0n)> гДе cr( е {ОД,*}, 1 < i< N, а шаблоном порта - подобного же рода троичный вектор у = (<51( 8г,..., Sk) . Шаблоны используются как для выбора правил коммутации пакетов, так и для модификации заголовков пакетов.

Предполагается, что при обслуживании пакетов коммутаторы выполняют над ними два типа действий: действие коммутации OUTPUT (у), где у - шаблон порта коммутатора, и действие модификации заголовка SET_FIELD (z), где z -шаблон заголовка пакета.

Конечная последовательность действий называется инструкцией обработки пакетов. Правилом коммутации пакетов называется тройка г = (г, у, а), где z и у - это шаблоны заголовка и порта, а а - инструкция.

Топология сети и функциональность коммутаторов описываются бинарными отношениями на множествах точек и локальных состояний пакетов; эти отношения задаются посредством квантифицированных булевых формул. В указанных формулах используются две параметризованные вспомогательные функции Ua (и, v) и Еа (и), где а 6 {0,1,*}, а и, и - двоичные векторы:

• если и = *, то Ua(u, 1?) = и = v и Еа(и) = 1;

• если о- е {0,1}, то Ua(u,v) = и = а и Еа(и) = и = о.

Действие а = OUTPUT (у) отправляет пакеты без изменения их заголовков во все выходные порты, имена которых подпадают под шаблон

у = (8^82, ...,Sk). Действие b = SET_FIELD (z) изменяет заголовки пакетов в соответствии с шаблоном z = а2, бит заголовка пакета hi остается

неизменным, если соответствующий ему символ шаблона сг( равен « *»; в противном случае этот бит принимает значение at. Семантика обоих действий описывается бинарными отношениями на множестве локальных состояний пакетов HxJ>:

R0«h,p),{h',p'» = Af=1(h[i] = h'[i])AAf=0[/Sl(p'H,Pm) /?b«h,p>,(h',p'» = Af=ay5i(h^ [t],h[i]) AAf=0(pM = P M)

Инструкция а вычисляет последовательную композицию составляющих ее действий. Если а - пустая последовательность, то пакет сбрасывается.

Семантика инструкции а описывается бинарным отношением Ra, которое определяется так:

• если инструкция а - пустая, то Ra = false-,

• если а = а,р, то отношение Ra задается следующими формулами в зависимости от действия а:

о если а - это действие коммутации пакета, то

Ka((h,p>,<h',p'» = Ka((h, Р). <h', р'» V Rp ((h, р>, <h', р'» о если а - это действие модификации заголовка пакета, то

fia«h,p>,<h',p'» = 3h" (i?aC(h, р>, (h",p'>) А ty?((h",p), (h',p'»)

Правило коммутации пакетов г = (z, у, а) применяет инструкцию $\alpha$ ко всем тем пакетам, локальные состояния которых подпадают под соответствующие шаблоны заголовка у и порта z.

Семантика правила определяется бинарным отношением Rr на множестве локальных состояний пакетов Jf х 3>:

йг((Ь,р), (h',p'>) = precondr((h, р}) Л йа((Ь, р), {h', р')) precondr(( h, р» = Af=1^((h[t]) лЛ^о^СрИ) Предикат precondr называется предохранителем правила г. Таблицей коммутации называется пара (D,p), где D = {г1( г2,..., гп} -множество правил коммутации, а /? - инструкция по умолчанию. Коммутатор применяет правила таблицы ко всем пакетам, поступающим на его входные порты. Если ни одно из правил множества D нельзя применить к пакету, то этот пакет обрабатывается инструкцией /?.

Семантика таблицы коммутации tab задается бинарным отношением:

*tab«b,P>,(h',p'» = Vf=1/?ri«h,p),(h',p')) V

(-1 ( Л&1 precandrt «h, p))) Л Rß((h, p>, <h', p'))) Для обозначения всевозможных таблиц коммутации для заданной сети используется запись Tab. Показано, что топология сети полностью определяется отношением пересылки пакетов Т £ (ОТ х W) х (IP х W) .Точки, вовлеченные в отношение Т, называются внутренними точками сети; все прочие точки сети считаются её внешними точками. Для обозначения множеств внешних входных и внешних выходных точек сети используются записи In и Out.

Предполагается, что внешние точки подключены к внешним устройствам (контроллерам, серверам, сетевым шлюзам и так далее), которые находятся вне сферы влияния контроллера ПКС.

Для заданного множества коммутаторов W и топологии Т конфигурацией сети называется всюду определенная функция Nef. W -> Tab, ассоциирующая с каждым коммутатором сета некоторую таблицу коммутации пакетов. Семантика сети с заданной конфигурацией Net определяется отношением на множестве состояний пакетов.? = Jf х Т х W:

RNet({ h,p,w>,<h',p',w'» = (CWet«h, p, w>, (h', p', w'» Л Out((p', w'))) V 3p" (CWit«h, p, w), (h', p", w')) Л Г«р", w), (p', w'») CNet«h,p,w),(h',p",w'» = Vw6W RNet(W)((h P). (h', P')) Л AfëxCwp] = w'[i])

Если отношение RNet(s,s') выполняется для пары состояний пакетов s = (h, p, w) и s' = (h', p', w*), то пакет с заголовком h, поступающий на порт р коммутатора w, может быть за один скачок (hop) отправлен либо на входной порт р' коммутатора w', либо на устройство, подключенное к внешнему выходному порту р' коммутатора w.

Семантика статической модели ПКС Net определяется отношением одношаговой маршрутизации пакетов RNet((h, p,w), (h', p',w')) , которое составляет реализуемые сетью правила коммутации пакетов, а также свойствами Out«p,w» и Out((p,w)), описывающими множество внешних точек сети. Располагая этими отношениями можно проследить маршруты всех потоков, проходящих через сеть при заданной ее конфигурации.

Динамическая модель ПКС предназначена для описания поведения контроллера. В этой модели контроллер представлен в виде автомата, получающего сообщения от коммутаторов на входе и генерирующего

последовательности команд для их реконфигурации на выходе. Множество допустимых сообщений в модели контроллера ограничено лишь заголовками тех пакетов, которые могут достичь контроллера, будучи отправленными из какой-либо внешней точки сети.

В качестве формальной модели контроллера ПКС построен автомат А = (S,C,Q, q0,&), где

• S и С — входной и выходной алфавиты соответственно,

• Q - множество внутренних состояний управления контроллера,

• q0, q0QQ- начальное состояние управления, и

• Д, Д S Qx.Sx.Cx.Q~ отношение переходов.

Для каждой конфигурации сети Net контроллер А может получать только такие сообщения, которые были индуцированы пакетами, поступившими на внешние точки сети. Рефлексивно-транзитивное замыкание R¡jet отношения одношаговой коммутации RNet позволяет определить множество сообщений Event(Net), допустимых в конфигурации Net следующим образом:

Event (Net) = {<h, р, w): Visible({h, p, w))}

Visible({h,p,w)) = 3 h' ,p' ,w' ,h' ': (/n((h,p,w)) Л R^ef ((h' ,p' ,w' >,<h' ' ,p,w>) A ШеСЬ! ' , p, w,h, octr, w

Динамическая модель ПКС полностью определяется множествами W, У, Jf коммутаторов, портов и заголовков пакетов, отношением пересылки пакетов Т и контроллером А.

Частичным прогоном ПКС М = QV,P,H,T,A) называется (конечная или бесконечная) последовательность вида:

run = (Net0, Яо) (Netv q^ 3 - Д (Net0 q¡) {Netl+V qi+1) -

где для каждого i, 0 < i:

• Nett - конфигурация ПКС, qt и st - состояния контроллера и пакета;

• s¡+1 6 Event(Neti);

• отношение переходов контроллера А содержит четверку (<j(, s(+1, új¡, qt+i). для которой конфигурация NetM получается из Nett путём применения к ней последовательности команд обновления конфигурации cu¡.

Полный прогон ПКС - это частичный прогон, который либо является бесконечным, либо завершается в состоянии ПКС (Nett, q¡), для которого

9

выполнено соотношение Event(Net{) = 0 .Для заданной ПКС М и конфигурации сети Net0 запись Run(M,Net0) обозначает множество полных прогонов М, начинающихся парой (Net0, q0).

Для спецификации политик маршрутизации построена 3-х уровневая иерархия языков, в которой выражения языка нижележащего уровня выступают в роли атомарных высказываний для языка вышележащего уровня:

Язык первого уровня £0 предназначен для описания свойств простейших элементов сети - отдельных состояний пакетов и их множеств - например, шаблонов правил коммутации. Поскольку семантика этих компонентов сети определяется двоичными векторами, математическую основу этого языка составляет булева алгебра.

Рассмотрим множество переменных Var = [Х1,Х2,...} , принимающих значения из множества состояний пакетов S = Jí х Р XW = {0,l}w+k+m .Спецификацией состояния пакета называется всякая булева формула ф над множеством булевых переменных №[/] ¡ X¡ е {Var}, 1 < j < N + к + m} и связок -i, Л. Множество всех таких формул обозначается записью £0. Формулы из £0 позволяют выразить любую булеву функцию на множестве состояний пакетов или, что то же самое, выделить любое подмножество указанных состояний. Язык £0 был использован при задании отношений, специфицирующих поведение коммутирующих элементов сети.

Язык второго уровня £г описывает глобальные статические требования, значительная часть которых представляет собой ограничения на отношения коммутации и маршрутизации. Математической основой языка Хг является логика первого порядка, расширенная оператором транзитивного замыкания.

В языке L-i используются единственный двухместный предикатный символ R и два одноместных предикатных символа / и О; это наименьший язык, удовлетворяющий следующим требованиям:

• если ф е £„, то ф 6

• если X,Y Е Var , то атомарные выражения R(X,Y) , 1(Х) , О (У) принадлежат ;

• если ф1нф2- формулы из £ъпХ е Var, то формулы (-i ifa), (tpt А тр2) и (3 X фх) так же принадлежат £х;

• если rp(X,Y) - формула из£ít содержащая не более двух свободных переменных, то ТС( ф(Х, Y)) е £г.

Семантика языка £г определяется с помощью отношений из статической модели сети. Пусть Net - некоторая конфигурация сети, и s = (h,p,w) и s' = (h', р', w'> - пара состояний пакетов. Тогда

Net Р= /(X)[(h, р, w>] тогда и только тогда, когда (р, w) е In;

Net 1= О (X) [(h, р, w)] тогда и только тогда, когда (р, w> е Out;

Net l= R (X, Г) [s, s'] тогда и только тогда, когда (s, s') 6 RNet;

Net 1= TC(jp(_X,Y))[s,s'] тогда и только тогда, когда существует конечная последовательность состояний пакетов s0, s1( ...,sb где 0 < I, что S0 = s и Sj = s, и для каждого i, 1 <i<l выполнено условие Net 1= ip(X, К) st].

Отношение выполнимости для прочих формул L1 определяется стандартным образом.

Поскольку язык построен на базе логики транзигавного замыкания FO[TC], то он обладает большей выразительной мощностью, чем темпоральные логики LTL, CTL, CTL* и -исчисления. Что касается алгоритмической сложности его использования - в работе доказана следующая

Теорема 1. Задача верификации модели сети Net t= гр относительно замкнутых формул языка £t является PSPACE-полной.

Язык третьего уровня £г предназначен для описания динамических требований к поведению ПКС. Эти требования описывают желаемую реакцию контроллера на сообщения, поступающие от коммутаторов. В качестве математической основы языка £г предлагается использовать фрагмент языка темпоральной логики линейного времени FO[TC], атомарными высказываниями которого выступают замкнутые формулы языка £х.

Синтаксис языка £2 определяется следующим образом. Пусть L0(X~) и £-l(X) - множества всех тех формул языков £0 и £г соответственно, в которых единственная свободная переменная X. Тогда LTL(£X) - это наименьший язык, удовлетворяющий следующим требованиям:

• если ф(Х) В £г(Х), то т/>(Х) <= LTL^y,

• если ФШ.Ч^СХ) 6 LTL(M , то формулы (-.Ф(Х)) , (Ф(Х)лФ(Х)) , (X Ф(Х)) и (ФДО и Ч»(Х)) принадлежат LTL(£{).

Оценка истинности формул из LTL{£i) производится на бесконечных последовательностях сетевых конфигураций t для заданного состояния

пакета s:

• если ф(Х) 6 А СЮ, то {WeíJI^! t= ip(s) тогда и только тогда, когда Metí >= i>(s)$,

• {WetJ^i 1= X Ф(в) тогда и только тогда, когда {ATef¡}^2 •= <Ks)>

• {Nett}f=1 t= Ф(я) U ^Cs) тогда и только тогда, когда t= 4*(s) для некоторого к, 1<, к, и Netj 1= Ф(в) для каждого j,l < j < к,

• семантика связок -i и А определяется обычным образом.

Язык спецификации политик маршрутизации £2 состоит из множества выражений вида ф(Х) => Ф(Х) $, где ф(Х) е £0(Х), а Ф(Х) - темпоральная формула языка LTL(£{). Семантика этих выражений определяется посредством отношения выполнимости на прогонах формальных моделей ПКС.

Для заданного прогона run модели ПКС М и выражения ф(Х) Ф(Х) языка £г отношение run t= фОО => Ф(Х) имеет место тогда и только тогда, когда {Wet¡}^n t= 0(s„) для каждого n, 1 < п, удовлетворяющего условию

<Ks„) = 1.

Политика маршрутизации PFP задаётся ограничением ф на множество допустимых начальных конфигураций сети, представляющим собой замкнутую формулу языка £t , и конечным множеством {фгСХ) => Фг(Х), ...,фп(Х) => Фп(Х)} выражений языка £г . Считается, что ПКС М реализует политику маршрутизации РРР в том случае, когда для любой сетевой конфигурации Net0, удовлетворяющей условию Net0 t= ф $, каждый прогон run из множества Run(_M,Net0~) удовлетворяет соотношению <£t(X) => Ф4(Х), 1 < i< п. Таким образом, задача верификации моделей ПКС состоит в том, чтобы проверить для заданной формальной модели ПКС М, удовлетворяет ли она спецификации политики коммутации $PFP$.

Для случая, когда контроллер ПКС представляет собой конечный автомат, сформулированная задача верификации разрешима. Показано, что указанная задача сводится к хорошо известной проблеме верификации конечных моделей программ для темпоральной логики WL.Ha основе проведенных теоретических исследований было построено программное средство верификации сетевых конфигураций относительно их спецификаций на языке Х^, состоящее из трех компонентов:

1. Конструктор моделей строит множество двоичных решающих диаграмм OBDD; описывающих конфигурацию ПКС.

2. Анализатор спецификаций предназначен для разбора выражений языка спецификации политик маршрутизации

3. Верификатор ПКС позволяет убедиться в том, что свойства заданной конфигурации ПКС удовлетворяют множеству предъявляемых к ней требований, или, наоборот, обнаружить факт их нарушения.

Наиболее интересной частью разработанной программной реализации является применение аппарата двоичных диаграмм ОВБО для компактного и эффективного представления модели. В частности, в разделе исследован вопрос выбора наилучшего порядка двоичных переменных и проведения над диаграммами некоторых специфических для поставленной задачи операций. Дано строгое описание грамматики разработанного языка и примеры спецификаций для некоторых наиболее распространённых политик маршрутизации.

В работе показано, что задача проверки соответствия конфигурации ПКС заданным требованиям политик маршрутизации сводится к задаче проверки выполнимости описывающих эти требования формул языка на множестве^ отношений, моделирующих ПКС. Этот факт был использован при разработке верификатора: он преобразует значения отношений, полученных на этапе анализа конфигурации сети, в деревья вычислений, полученные от анализатора спецификаций, и производит поочерёдное их вычисление:

• Если хотя бы одна формула выдаёт ложное значение, конфигурация сети нарушает требования политик маршрутизации и считается некорректной;

• Иначе, если все формулы выполняются - конфигурация корректна.

В конце этой главы представлены методики проведения и результаты экспериментальных исследований построенных средств. Результаты проведенных экспериментов показали, что они могут успешно применяться на практике. Кроме того, построенные средства позволили обнаружить в конфигурации сети ошибки, которые не удалось выявить другими методами.

Во второй главе рассматривается задача получения верхней оценки сквозной задержки передачи данных в сети. Показано что данная задача относится к проблеме управления качеством сервиса в сети.

Приводится краткое описание основных методов управления качеством сервиса, с которым обслуживаются передающиеся через сеть потоки данных, а так же соответствующих им моделям распределения ресурсов. В частности, в

этом разделе рассматриваются модель интегрированных сервисов и модель дифференцированных сервисов.

В модели интегрированных сервисов резервирование ресурсов происходит в процессе установки соединения и не может изменяться до момента его завершения. Поэтому для обслуживания каждого соединения выделяется такое количество ресурсов, которое было бы достаточным для удовлетворения требований использующего это соединение приложения на пике нагрузки. Такой подход чреват фрагментацией ресурсов: сеть не справляется с нагрузкой, не смотря на то, что часть её ресурсов не используется.

Основная идея модели дифференцированных ресурсов - введение приоритетов на множестве соединений. Коммутаторы заранее определяют несколько классов обслуживания, а передающиеся через сеть соединения выбирают наиболее подходящие из предложенных классов. Объём сетевых ресурсов, который выделяется для обслуживания каждого конкретного класса обслуживания, не фиксирован. Гарантируется лишь то, что более высоким классам обслуживания будет предоставлено больше ресурсов, чем менее приоритетным. Указанные особенности модели дифференцированных сервисов позволяют избежать простаивания оборудования, что выгодно отличает её от модели интегрированных ресурсов. Поэтому в качестве наиболее актуальной модели распределения ресурсов была выбрана модель дифференцированных сервисов.

Далее в этой главе приводится описание внутреннего устройства коммутатора, а так же рассматриваются способы реализации моделей интегрированных и дифференцированных сервисов в коммутационном оборудовании, анализируются разные методы буферизации: буферизация на выходе (OQ), буферизация на входе (IQ), виртуальная буферизация на выходе (VOQ), множественная виртуализация на выходе (MOQ) и комбинированная буферизация (CIOQ).

Для постановки задачи получения верхней оценки сквозной задержки и построения модели передачи пакета через сеть было выбрано сетевое исчисление (network calculus)'. Сетевое исчисление изучают зависимости между

1 J.-Y. Le Boudée, P. Thiran. Network Calculus: a theory of deterministic queuing systems for the internet // Lecture Notes in Computer Science (LNCS), volume 2050, Berlin, Germany: Springer Verlag, 2001.

производительностью элементов сети и качеством сервиса, с которым обрабатываются передаваемые через эту сеть потоки данных. В основе теории лежит идея получения детерминированных оценок путём рассмотрения наилучших и наихудших, с точки зрения заданной характеристики, сценариев работы отдельных частей сети и эффективного комбинирования этих сценариев между собой.

Модель ТСИ описывает коммутационную сеть следующим образом:

• Сеть разбивается на множество обработчиков. Разные обработчики могут моделировать элементы сети различного масштаба, начиная от физической линии или очереди пакетов внутри сетевого устройства и заканчивая коммутаторами и даже целыми подсетями;

• Поведение обработчика определяется кривой сервиса, которая отражает его производительность и используемые им правила расцределения ресурсов между проходящими через него потоками;

• Для каждого потока данных задаётся маршрут их передачи через обработчики и кривая нагрузки, которая описывает характерные для_ этого потока ограничения на скорость поступления данных в сеть.

В качестве кривых сервиса и кривых нагрузки используется класс Т накопительных функции времени, которые выражают общее количество данных, переданных этими модельными сущностями с момента начала отсчёта.

Т = {f: аг0 -> К.г0 U {+ оэ} |LeftContinuous(О A NonDecreasing(f) A Causal(f)}

NonDecreasing(f) £=' Vtx < t2: f(tx) < f(t2) LeftContinuous (0 = Vt0 e E: lim f(t) = f(t„)

t-<to-0

Causal® d=±r Vt = 0 -> f(t) = 0

Функцией прибытия (отправки) потока данных для обработчика S называется такая накопительная функция А еТ (D вТ), которая описывает зависимость суммарного количества данных потока, поступивших на этот обработчик (переданных этим обработчиком), от времени.

Периодом отставания называется временной интервал, в течение которого отставание b(t) обработчика строго положительно. Если момент t е R. находится внутри периода отставания [SBP(t);EBP(t)] , то его границы задаются формулами:

SBP(t) = sup{u £ t |A(u) = D(u)}

EBP(t) = inf{u Й: 11 A(u) = D(u)}

После получения данных обработчики способны временно удерживать их внутри себя. Зависимость объёма хранящихся в обработчике S данных от времени называется его отставанием b(t) и представляется в виде разности функций прибытия А и отправки D обслуживаемого им потока данных:

b(t) = A(t) - D(t)

Задержкой d(t) обработчика S называется время, которое порция данных, поступившая в S в момент времени t, пробудет внутри этого обработчика.

Для произвольного обработчика S и любой пары соответствующих этому обработчику функций прибытия А и отправки D, (A, D) е S, его отставание b(t) ограничено сверху вертикальным отклонением v(A, D) этих потоков. Более того, если обработчик S обслуживает данные по дисциплине FIFO, его задержка d(t) ограничена сверху их горизонтальным отклонением h (A, D):

Vt е К: b(t) < v(A, D) = sup{A(t) - D(t)} t

Vt 6 Ш: d(t) < h (A, D) = sup{inf{t > 0|A(t) < D(t + t)}} t

Каждый обработчик S может быть описан перечислением соответствующих ему пар вида (A, D) и задан отношением вида Sc-TxT.

На практике для описания обработчика используют кривые сервиса: (нестрогой) кривой сервиса называется такая функция р В Т , что при обслуживании потока с функцией прибытия А е З7 для его функции отправки D £ У выполняется:

D(t) > mf{A(s) + P(t - s)}

Строгой кривой сервиса обработчика S называется всякая такая функция ps 6 Т, что в процессе обслуживания потока с функцией прибытия А и функцией отправки D, (A, D) G S, в течение каждого периода отставания [s; t] элемент S обрабатывает, по меньшей мере, ps(t — s) данных:

D(t) — D(s) > Ps(t — s)

Как и в случае функции производительности Р обработчика, построение сколь-нибудь точной функции прибытия А 6 Т для заданного потока данных на практике может вызвать затруднения. Поэтому для описания потоков

поступления данных используется тот же приём, что и для описания обработчиков: явная зависимость функции поступления А от времени заменяются зависимостью от длительности интервала передачи данных.

Кривой нагрузки для потока с функцией прибытия АеТ называется такая функция а 6 Т, что для каждого временного интервала длины т количество переданных в течение него данных этого потока не превышает величины а(т): Vt: Vt: A(t + т) - A(t) S а(т)

Теория сетевого исчисления определяет над множеством накопительных функций операции поточечного сложения и минимума. Построенная с их помощью Min-Plus алгебра используется для выражения зависимостей между потоками данных, поступающими на входы обработчиков, и потоками данных, передаваемыми через их выходы. При этом используются операции прямой и обратной Min-Plus свёртки, обозначенные символами ®и0 соотвестсвенно. if ® дШ ш 0М{/О) + g(t - s)} (W 0 g)(t) « sup {w(t + u) - g(u)}

tiUSO

Указанные операции позволяют компактно сформулировать основные результаты теории сетевого исчисления: Если обработчик с кривой сервиса р е Т обслуживает поток данных, ограниченный кривой нагрузки а £ 7, то:

1. Для отставания b(t) выполнена формула:

b(t) < (ос 0 Р)(0)

2. При дисциплине FIFO для задержки выполняется неравенство:

d(t) < inffr > ОI (а © Р)(-т) < 0}

3. Поток обработанных данных ограничен кривой прибытия a'(t) :

a'(t) = (cc©P)(t)

Одна из основных сложностей применения теории сетевого исчисления на практике обусловлена высокой сложностью вычисления прямой и обратной свёртки. Однако известны быстрые алгоритмы для вычисления этих операций при рассмотрении более узких классов функций. Например, в литературе часто рассматриваются кривые нагрузки и кривые сервиса образованные парой линейных сегментов. Одним из известных результатов является следующая

Теорема. График функции свёртки для двух выпуклых кусочно-линейных функции ÎGT и g е Т может быть построен путём последовательной композиции составляющих эти функции отрезков в порядке увеличения значений их угловых коэффициентов.

Одним из результатов настоящей работы является изложенное в разделе доказательство, в некоторой степени, обратного для неё утверждения:

Теорема 2. Пусть задана пара кусочно-линейных функций: вогнутая функция w Е 7 и выпуклая функция g £ 7 - пересекающихся ровно в двух точках: 0 и t0 = sup{w(t) = g(t)} > 0 . Тогда график их обратной свёртки f = w © g может быть построен из точки (t0, — g(t0)) последовательным соединением отрезков, составляющих графики функций w(t) и g(t) = min(g(t), g(t0)), в порядке уменьшения их угловых коэффициентов.

Эта теорема позволила обобщить два существующих алгоритма оценки времени передачи пакетов на более широкий класс функций описания кривых нагрузки и сервиса. Ранее эти алгоритмы предполагали, что кривые нагрузки и сервиса - кусочно-линейные функции из двух сегментов. Благодаря доказанной теореме те же алгоритмы можно применять и в том случае, когда указанные функций состоят из произвольного количества сегментов.

Показано, что оба указанных алгоритма не в состоянии предоставить достижимые оценки для времени передачи пакетов и дают лишь грубые оценки сверху. Одним из путей получения более точных оценок является отказ от использования свёртки, и описание всей сети в виде системы неравенств, отражающей зависимость объёма переданных через сеть данных от количества данных, поступивших на её входы, во времени. Далее в работе приводится описание способа использования систем линейных неравенств для вычисления достижимой верхней оценки времени передачи пакетов через сеть.

Топология сети обработчиков задана ориентированным ациклическим графом G = {V,E) без кратных дуг, вершины которого пронумерованы натуральными числами V = {1, ...,т}. Вершине с номером v сопоставлен обработчик Sv, который обслуживает совокупность проходящих через него потоков данных в соответствии с вогунтой кусочно-линейной строгой кривой сервиса /?„ Е Т . Обработчики обслуживают каждый отдельный поток по дисциплине FIFO, однако правила мультиплексирования этих потоков между собой, вообще говоря, произвольные - модель построена в ограничениях слепого мультиплексирования.

Каждый путь я длины I = \п\ через граф G однозначно описывается неповторяющейся последовательностью п = {vjJjj-j вершин. Для обозначения -

й вершины маршрута п используется запись тс [/с]. При этом вне зависимости от маршрута п значение выражения тг[0] = 0.

Через граф С пролегают маршруты щ,...,пп передачи данных множества пронумерованных натуральными числами потоков Р = При этом

потоку с номером \ сопоставлена собственная вогнутая кусочно-линейная кривая нагрузки аг £ Т.

Кривые нагрузки потоков и кривые сервиса обработчиков согласованы между собой так, что суммарный объём данных, пребывающих на каждый из обработчиков сети, асимптотически не превышает того объёма, который этот обработчик в состоянии обслужить:

£: г€ тг/

Функция поступления данных потока ^ £ в сеть обозначается записью

Для обозначения функции передачи данных, которая для каждого момента времени Г > 0 возвращает суммарное количество данных потока сумевших преодолеть обработчик с номером V за время [0; с], используется запись

Таким образом, интенсивность передачи данных потока ^ через сеть характеризуется множеством функций ¥1 = \ 0 < к < |гтг|}.

Сценарием работы сети называется всякое множество IIиз £|тГ(| + п функций поступления данных, удовлетворяющее следующим ограничениям:

• Каждая из указанных функций должна принадлежать классу Т\

• В каждый момент времени объём данных, преодолевших произвольный обработчик сети, не превышает объёма данных, которые на него

поступили: V ^,с > 0,1< к < |я,|: ^'^(О > ,м(9

• Функции, непосредственно описывающие поступление потоков в сеть, удовлетворяют ограничениям соответствующих кривых нагрузки;

• Функции, проходящие через один и тот же обработчик, удовлетворяют соответствующим ему кривым сервиса;

Поскольку перечисленные ограничения определяют функции поступления данных неоднозначно, то одна и та же сеть способна обслуживать проходящие через неё потоки по разным сценариям. Таким образом, для построения достижимой верхней оценки задержки передачи заданного потока данных через сеть достаточно рассмотреть множество допустимых сценариев её работы и

выбрать среди них один из тех сценариев, при котором некоторая порция данных этого потока передаётся наибольшее время.

Предлагается описывать семейство допустимых сценариев работы сети системой линейных неравенств. В качестве переменных в построенных линейных системах используются значения отдельных функций сценария в некоторые моменты времени. Сами неравенства получаются из ограничений сценария работы сети. Преимущество указанного подхода заключается в том, что выбор такого сценария работы сети, на котором достигается максимальная задержка передачи данных заданного потока, может быть проведён с помощью линейного программирования.

Так как не все ограничения на сценарий имеют линейную природу, то вычисление верхней оценки для времени передачи данных через сеть сводится к решению нескольких систем линейных неравенств, каждая из которых соответствует некоторому семейству допустимых сценариев работы сети. Наибольшее среди их решений является искомой верхней оценкой.

Хотя использование систем линейных уравнений для моделирования сети обработчиков в предположениях задачи и не является новым, в работе предложен оригинальный алгоритм разбивши всех допустимых сценариев работы сети на семейства, а так же генерации соответствующих им неравенств. Указанный алгоритм является конструктивным доказательством для следующей теоремы;

Теорема 3. Если топология сети обработчиков может быть представлена неориентированным ациклическим графом, то задача построения достижимой верхней оценки передачи данных по маршруту из п обработчиков сводится к решению п-1 системы линейных неравенств и может быть решена за полиномиальное время.

Ранее полиномиальное время решения задачи построения верхней оценки для задержки было получено лишь для сетей с линейной (tandem) топологией.

В конце этой главы приводится описание разработанных программных средств построения верхних оценок для сквозной задержки передачи данных, а так же результаты экспериментальных апробаций указанных средств.

Полученные с помощью разработанных алгоритмов оценки времени передачи данных сравниваются с показателями специально разработанной имитационной модели сети. На основе экспериментальных данных показано, что

время передачи пакетов в имитационной модели сета никогда не превосходят полученных теоретически верхних оценок.

В заключении сформулированы основные результаты диссертационной работы и перечислены некоторые из возможных путей их развития.

В Приложении А приведено описание синтаксиса и семантики некоторых перспективных формальных языков для спецификации политик маршрутизации.

Приложеяне Б содержит описания некоторых перспективных формальных моделей ПКС.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

Полученные автором результаты изложены в следующих работах:

1. Chemeritskiy Е., Smelyansky R., Zakharov V. A formal model and verification problems for software defined networks // Proceedings of the 4-th International Workshop "Program Semantics, Specification and Verification: Theory and Applications". — Yekaterinburg, Russia, 2013. — P. 21-30.

2. Захаров В., Смелянский P., Чемерицкий E. Формальная модель и задачи верификации программно-конфигурируемых сетей // Моделирование и анализ информационных систем. — 2013. — Т. 20, № 6. — С. 33-48.

3. Chemeritskiy Е., Zakharov V. On the network update problem for software defined networks // Proceedings of the 5th Workshop "Program Semantics, Specification and Verification: Theory and Applications". — Издательский дом ГУ ВШЭ Москва, 2014. — Р. 26-37.

4. V. Altukhov, Е. Chemeritskiy, V. Podymov, V. Zakharov Vermont - a toolset for checking SDN packet forwarding policies on-line // Proceedings of the 2014 international science and technology conference "Modern Networking Technologies (MoNeTec)". — SDN & NFV modern networking technologies. — МАКС Пресс Москва, Россия, 2014. — P. 7-12.

5. Altukhov V., Chemeritskiy E. On real-time delay monitoring in software-defined networks // Proceedings of the 2014 international science and technology conference "Modern Networking Technologies (MoNeTec)". — SDN & NFV modern networking technologies. — Макс Пресс Москва, Россия, 2014, —P. 1-6.

6. Smeliansky R., Chemeritsky E. On QoS management in SDN by multipath routing // Proceedings of the 2014 international science and technology conference "Modern Networking Technologies (MoNeTec)". — SDN & NFV

modern networking technologies. — МАКС Пресс Москва, Россия, 2014. — P. 41-46.

7. Chemeritskiy E., Zakharov V. Consistent network update without tagging // Proceedings of the 2014 international science and technology conference "Modern Networking Technologies (MoNeTec)". — SDN & NFV modern networking technologies — МАКС Пресс Москва, Россия, 2014. — P. 47-52.

8. V. Altukhov, E. Chemeritskiy, V. Podymov, V. Zakharov A runtime verification system for software defined networks // Материалы Международной научно-практической конференции: Tools & Methods of Program Analysis, TMPA-2014. — Кострома: КГТУ, 2014. — P. 19-28.

9. Захаров В., Чемерицкий E. О некоторых задачах реконфигурирования программно-конфигурируемых сетей // Моделирование и анализ информационных систем. — 2014. — Т. 21, № 6. — С. 57-69.

10. Chemeritsky Е., Smeliansky R., Zakharov V. A formal model and verification problems for software defined networks // Automatic Control and Computer Sciences. — 2014. — Vol. 48, no. 7. — P. 398-406.

11. В. Алтухов, В. Захаров, В. Подымов, Е. Чемерицкий Vermont - средство верификации программно-конфигурируемых сетей / // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. — 2015. — Т. 212, № 1. — С. 74-87.

Напечатано с готового оригинал-макета

Подписано в печать 16.07.2015 г. Формат 60x90 1/16. Усл.печл. 1,0. Тираж 100 экз. Заказ 175.

Издательство ООО "МАКС Пресс" Лицензия ИД N 00510 от 01.12.99 г. 119992, ГСП-2, Москва, Ленинские горы, МГУ им. М.В. Ломоносова, 2-й учебный корпус, 527 к. Тел. 8(495)939-3890/91. Тел./факс 8(495)939-3891.