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

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

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

В статье рассмотрены особенности применения технологий разработки программных систем на основе модельно-ориентированного подхода: Model Driven Software Development (MDSD), Model Driven Architecture (MDA) и Model Driven Development (MDD). Описаны преимущества использования подходов в промышленности. Основной акцент сделан на проектирование систем, автоматическую генерацию кода больших систем, верификацию, доказательство свойств систем и уменьшение плотности ошибок. Приведены недостатки использования данного подхода, одним из которых является различная степень детальности модели и реальной реализованной системы на языке программирования. В работе предлагается подход, характерный для систем, имеющих многоуровневое представление, связанное с детализацией функциональности приложения до уровня, на котором осуществляется прямая генерация корректного кода. Подход позволяет детализировать модель до уровня реального кода системы, при этом сохранить проверенную семантику модели и обеспечить проверку всей детальной модели. Детализация проводится как по потоку управления, так и по потоку данных. Представлены шаги по преобразованию абстрактных структур данных (в том числе транзакций, сигналов и их параметров) в структуры данных, используемых в реализации систем. Приведена грамматика языка задания правил преобразования структур данных абстрактной модели в детальные структуры данных реальной системы и общая схема преобразования. Приведены результаты применения предложенного метода в промышленной технологии.

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

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

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

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

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

Верификация С-программ является актуальной проблемой современного программирования. Для применения известных методов дедуктивной верификации необходимо аннотировать циклы посредством инвариантов, что во многих случаях является трудной задачей. В этой статье мы рассматриваем язык C-light, который является выразительным подмножеством языка C, соответствующего стандарту ISO. Для верификации C-light программ нами были предложены двухуровневый подход [19, 20] и метод смешанной аксиоматической семантики [1, 3, 11]. На первой стадии этого подхода исходная C-light программа транслируется [17] в программу на языке C-kernel [19], который является подмножеством языка C-light. Теорема о корректности этой трансляции была доказана в [10, 11]. По сравнению с C-light в языке C-kernel меньше операторов, что позволяет уменьшить число правил вывода при разработке аксиоматической семантики. На второй стадии этого подхода для программ на языке C-kernel порождаются условия корректности по правилам смешанной аксиоматической семантики [10, 11], которая может содержать несколько правил вывода для одной и той же программной конструкции. В таких случаях правила вывода применяются однозначно в зависимости от контекста. Заметим, что во многих случаях использование смешанной аксиоматической семантики позволяет упростить условия корректности. В этой статье представлено расширение данного подхода, которое включает наш метод верификации для финитной итерации над неизменяемыми структурами данных без выхода из тела цикла в C-light программах. Данный метод содержит новое правило вывода для таких финитных итераций без инвариантов. Это правило было реализовано в генераторе условий корректности. На стадии доказательства используется SMT-решатель Z3 [12]. Рассмотрен пример, иллюстрирующий применение данного подхода.

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

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

В настоящее время наблюдается огромный практический интерес к параллельному программированию. Этот интерес обусловлен доступностью супер-ЭВМ, компьютерных кластеров и мощных графических процессоров для массового использования в вычислительной математике и компьютерном моделировании. Кроме того, такие технологии параллельного программирования, как MPI, OpenMP и CUDA, позволяют использовать безопасным образом опыт программирования на классических языках Си и FORTRAN для ускорения вычислений, избегая конфликтов (“гонок”) из-за ресурсов. Однако такой прогресс параллельного программирования не означает, что конкуренция из-за ресурсов не может возникать в параллельных общего вида, в так называемых распределенных системах в частности. Поэтому остается актуальным изучение и преподавание формальных моделей параллелизма и средств верификации поведенческих свойств параллельных (распределенных) систем. В статье представлен опыт преподавания специального курса по формальным моделям параллелизма для магистрантов и аспирантов, специализирующихся в области высокопроизводительных вычислений. Сначала в статье дан обзор курса в целом, предварительных знаний, необходимых для этого курса, целей и задач курса, представлен план лекций и список рекомендованной литературы. Затем представлен пример одной поучительной головоломки (на достижимость в пространстве состояний) и ее формализации средствами семантических, синтаксических и логических моделей, как-то: сетями Петри, средствами исчисления параллельных взаимодействующих процессов (CCS) и темпоральной логики CTL. Эта головоломка — хороший пример для того, чтобы показать специфику и пользу каждого из рассмотренных формализмов.

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

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

В статье мы обсуждаем концепцию схемы Лакса–Дарбу и иллюстрируем ее на хорошо известных примерах, ассоциированных с нелинейным уравнением Шрёдингера. Мы изучаем связи, возникшие благодаря преобразованиям Дарбу, между иерархиями нелинейного уравнения Шрёдингера, модели Гейзенберга, модели главного кирального поля, а также дифференциально-разностными системами (такими как цепочка Тоды и дифференциально-разностная цепочка Гейзенберга) и конечно-разностными интегрируемыми системами. Мы показываем, что существует формальное преобразование, которое одновременно диагонализует все элементы схемы Лакса–Дарбу. Это приводит нас к производящим функциям локальных законов сохранения для всех интегрируемых систем, полученных в рамках данной схемы Лакса–Дарбу. Обсуждаются связи между законами сохранения систем, принадлежащих заданной схеме Лакса–Дарбу.

Информационные системы (ИС) оставляют многочисленные следы и журналы событий своей работы. В контексте сервисно-ориентированной архитектуры (СОА) информационной системы такие журналы содержат детальную информацию о последовательностях вызовов процессов и сервисов. Современные инструменты мониторинга приложений и отслеживания ошибок их исполнения предоставляют довольно простые средства поиска и фильтрации журналов событий. Тем не менее, “интеллектуальный” анализ таких журналов событий является крайне полезным, так как может предоставить ценную информацию об архитектуре системы, взаимодействии между бизнес-доменами и сервисами. В работе рассматриваются журналы событий (представляющие данные о системных исполнениях) большой информационной системы поддержки бронирования, на основании данных которых производится обнаружение нарушений архитектурных принципов взаимодействия компонентов и общих антипаттернов СОА. Для анализа этих журналов применяются проверенные подходы дисциплины извлечения и анализа процессов (process mining). Process mining применяется для автоматического синтеза моделей процессов, анализа этих процессов и их улучшения на основе информации о поведении ИС, записанной в виде журналов событий. На базе нескольких конкретных примеров демонстрируется успешное применения подходов process mining для анализа системных исполнений и приводится обоснование необходимости дальнейших исследований в данной области.

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

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

Традиционная архитектура сети передачи данных является негибкой и сложной. Данное обстоятельство привело к появлению парадигмы программно-конфигурируемой сети (ПКС), в которой уровень управления сетью отделен от уровня передачи данных. Это стало возможно за счет переноса плоскости управления с коммутационного оборудования в программные модули, которые работают на выделенном сервере, называемом контроллером (или сетевой операционной системой), или в сетевые приложения, которые работают с этим контроллером. Способы представления, хранения и интерфейсы взаимодействия с элементами сетевой топологии, доступные пользователям контроллера ПКС, являются одними из наиболее важных аспектов сетевых операционных систем. Данное обстоятельство обусловлено тем, что функционирование некоторых ключевых модулей контроллера в существенной степени основано на внутреннем представлении сетевой топологии. Такими модулями, к примеру, являются модуль firewall, модуль маршрутизации и т.д. В данной статье рассмотрены применяемые способы представления и хранения сетевой топологии, а также интерфейсы взаимодействия с соответствующими модулями контроллера Floodlight. Предложен и разработан альтернативный алгоритм обмена сообщениями об изменении сетевой топологии между контроллером и сетевыми приложениями, позволяющий реализовать оповещение на основе подписки на соответствующие события. Разработан API для модуля взаимодействия с прикладными программами контроллера программно-конфигурируемой сети. На основе данного алгоритма и API разработан модуль Topology Tracker, способный в активном режиме сообщать сетевым приложениям о произошедших изменениях в топологии сети и хранящий ее компактное представление для ускорения процесса взаимодействия.