VERMONT – средство верификации программно-конфигурируемых сетей

Представлено программно-инструментальное средство VERMONT (VERifying MONiTor) для верификации в оперативном режиме программно-конфигурируемых сетей (ПКС) относительно формально специфицированных политик маршрутизации пакетов (ПМП). VERMONT может быть установлен в сети между контроллером и коммутаторами для наблюдения за сетью путем перехвата сообщений и команд, которыми обмениваются контроллер и коммутаторы, построения модели сети и проверки того, в какой мере изменения, происходящие в сети в результате выполнения команд реконфигурирования, подключения и отключения каналов связи и коммутационных устройств, согласуются с заданными требованиями ПМП. Перед тем как отправить команду реконфигурирования таблиц коммутации, VERMONT моделирует результат ее выполнения и проверяет выполнимость требований ПМП для модифицированной модели ПКС. Если VERMONT обнаруживает нарушение какого-либо требования ПМП, он блокирует пересылку команды и оповещает об этом системного администратора.
Описана математическая модель ПКС и формальный язык спецификации ПМП, используемые в нашей системе верификации. Рассказано об устройстве и алгоритмических принципах функционирования системы VERMONT. Представлены результаты экспериментов по применению разработанной системы для верификации некоторых ПКС, а также проведен сравнительный анализ системы VERMONT и других систем верификации ПКС.