Аннотация:

Рассмотрена проблема визуального представления темпоральных и вероятностных элементов в инструментах формального моделирования игровых механик. На основе анализа существующих систем визуального моделирования – Machinations, сетей Петри, диаграмм состояний UML и UPPAAL – выявлены их ключевые ограничения при описании сложных игровых сценариев. Предложен подход к визуализации темпоральных операторов и вероятностных конструкций в инструменте Tula, разработанном авторами. Описан набор визуальных примитивов, обеспечивающих двунаправленное соответствие между визуальным представлением и формальной спецификацией на языке геймплея. Приведены примеры визуального моделирования типовых игровых сценариев с элементами временных задержек, условных вероятностей и многопользовательских взаимодействий. Показана возможность автоматической трансформации визуальных моделей в формальные спецификации, пригодные для верификации средствами PRISM и UPPAAL. Проведён сравнительный анализ выразительных возможностей Tula и систем-предшественников, показавший, что Tula является единственной из рассмотренных систем, одновременно обеспечивающей формальную верифицируемую семантику, встроенную поддержку темпоральных операторов (X, G, F, U) и произвольных вероятностных распределений, а также визуальную нотацию, организованную вокруг ресурсных потоков и игровых событий. Предложенный в Tula принцип двухуровневой спецификации с двунаправленной трансформацией замыкает цикл «дизайн → формализация → верификация → корректировка», снижая порог входа в формальные методы для практиков без потери верификационной полноты. Это позволяет рассматривать Tula как промежуточный слой между итеративным геймдизайном и промышленными верификаторами.

Аннотация:

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

В работе использован новый тестовый набор для верификации реализаций клиента протокола TLS 1.3 на соответствие спецификациям интернет, разработанный на основе спецификации RFC 8446 с использованием технологии UniTESK и методов мутационного тестирования. Для тестирования реализаций на соответствие формальным спецификациям применена технология UniTESK, предоставляющая средства автоматизации тестирования на основе использования конечных автоматов. Состояния тестируемой системы задают состояния автомата, а тестовые воздействия – переходы этого автомата. При выполнении перехода заданное воздействие передается на тестируемую реализацию, после чего регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Мутационные методы тестирования используются для обнаружения нестандартного поведения тестируемой системы (завершение из-за фатальной ошибки, «подвисание», ошибки доступа к памяти) с помощью передачи некорректных данных, такие ситуации часто остаются за рамками требований спецификаций. В сообщения, сформированные на основе разработанной модели протокола, вносятся какие-либо изменения. Модель протокола дает возможность вносить изменения в поток данных на любом этапе сетевого обмена, что позволяет тестовому сценарию проходить через все значимые состояния протокола и в каждом таком состоянии проводить тестирование реализации в соответствие с заданной программой. Представленный подход доказал свою эффективность в нескольких наших проектах при тестировании сетевых протоколов, обеспечив обнаружение различных отклонений от спецификации и других ошибок. Текущая работа является частью проекта верификации протокола TLS 1.3 и охватывает реализации клиентской части протокола.

Аннотация:

Представлен опыт верификации реализаций сервера криптографического протокола TLS версии 1.3. TLS – широко распространенный криптографический протокол, предназначенный для создания защищенных каналов передачи данных и обеспечивающий необходимую для этого функциональность: конфиденциальность передаваемых данных, целостность данных, аутентификацию сторон. Новая версия протокола TLS 1.3 была представлена в августе 2018 года и имеет ряд существенных отличий по сравнению с предыдущей версией 1.2. Ряд разработчиков протокола TLS уже включил поддержку последней версии в свои реализации. Данные обстоятельства делают актуальным проведение исследований в области верификации и безопасности реализаций новой версии протокола TLS. В работе использован новый тестовый набор для верификации реализаций протокола TLS 1.3 на соответствие спецификациям интернета, разработанный на основе спецификации RFC 8446 с использованием технологии UniTESK и методов мутационного тестирования. Текущая работа является частью проекта верификации протокола TLS 1.3 и охватывает часть дополнительной функциональности и необязательных расширений протокола.

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

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

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