• Main Navigation
  • Main Content
  • Sidebar

Электронные библиотеки

  • Главная
  • О нас
    • О журнале
    • Цели и задачи
    • Тематика
    • Главный редактор
    • Редакция
    • Отправка материалов
    • Заявление об открытом доступе
    • Заявление о конфиденциальности
    • Контакты
  • Текущий выпуск
  • Архивы
  • Регистрация
  • Вход
  • Поиск
Издается с 1998 года
ISSN 1562-5419
16+
Language
  • Русский
  • English

Найти

Расширенные фильтры

Результаты поиска

Средства интерактивного взаимодействия с пользователем в системе SAPFOR

Никита Андреевич Катаев
157-183
Аннотация:

Автоматизация параллельного программирования затрагивает различные этапы в разработке параллельной программы, начиная от профилирования исходной программы, ее преобразования и приведения к виду, допускающему эффективное распараллеливание, и заканчивая построением параллельной версии программы и ее последующей оптимизацией. Немалое значение имеет выбор целевой модели параллельного программирования, с одной стороны, позволяющей задействовать разнообразие существующих на данный момент аппаратных ресурсов, а с другой, упрощающей разработку автоматизированных средств и позволяющей пользователю изучить решения, принимаемые системой автоматизированного распараллеливания. Система SAPFOR (System FOR Automated Parallelization) объединяет различные подходы, направленные на автоматизацию программирования, и позволяет пользователю принимать активное участие в процесс распараллеливания программ. Кроме того, распараллеливание выполняется в модели DVMH, позволяющей разрабатывать эффективные параллельные программы для гетерогенных вычислительных кластеров.


В настоящей статье рассмотрен подход к автоматизированному распараллеливанию программ, реализованный в системе SAPFOR. Отдельное внимание уделено архитектуре системы и реализации подсистемы интерактивного взаимодействия с пользователем. Рассмотрено применение интерактивной оболочки в процессе распараллеливания и приведены результаты распараллеливания некоторых программ из набора NAS Parallel Benchmarks 3.3.1 c ручным распараллеливанием, выполненным с помощью OpenCL.

Ключевые слова: анализ программ, преобразование программ, автоматизация распараллеливания, графический интерфейс пользователя, SAPFOR, DVM, LLVM.

Определение зависимостей по данным средствами динамического анализа системы SAPFOR

Никита Андреевич Катаев, Александр Андреевич Смирнов, Андрей Дмитриевич Жуков
473-493
Аннотация: Использование указателей и косвенной адресации в программе, а также сложная структура графа потока управления являются одними из основных препятствий при выполнении статического анализа программ. Обнаруженные в результате такого анализа свойства программы слишком консервативно описывают ее поведение и часто оказываются недостаточными для принятия решений о возможности ее параллельного выполнения. Использование динамического анализа программ позволяет расширить возможности средств автоматизации распараллеливания. В системе SAPFOR (System FOR Automated Parallelization) реализован инструмент динамического анализа, опирающийся на инструментацию программ в представлении LLVM, что позволяет исследовать программы на языках C и Fortran. Чтобы снизить накладные расходы на время выполнения инструментированной программы, сохранив при этом полноту проводимого анализа, используются возможности статического анализа, реализованного в SAPFOR. В процессе динамического анализа часть обращений к памяти, информация о которых была получена в процессе статического анализа, может быть проигнорирована. Разработанный инструмент был протестирован на тестах производительности из пакета NAS Parallel Benchmarks для языков C и Fortran. В процессе динамического анализа кроме традиционных видов зависимостей (flow, anit, output) также определяются переменные, зависимость по которым может быть устранена за счет приватизации или конвейерного выполнения циклов. Совместно с возможностями DVM и OpenMP это существенно облегчает, в том числе, и ручное распараллеливание, облегчая задание соответствующих директив компилятора.
Ключевые слова: анализ программ, динамический анализ, автоматизация распараллеливания, SAPFOR, DVM, LLVM.

О вопросе измерения вклада программистских решений в производительность программ

Лидия Васильевна Городняя, Татьяна Анатольевна Андреева
738-759
Аннотация:

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

Ключевые слова: измерение качества программ, продуктивность программирования,, производительность программ, программистские решения, функциональное программирование.

Добавление статической типизации в язык функционально-потокового параллельного программирования

Александр Иванович Легалов, Игорь Александрович Легалов, Иван Васильевич Матковский
788-807
Аннотация: Предложено добавить статическую систему типов в функционально-потоковую модель параллельных вычислений и разработанный на ее основе язык функционально-потокового параллельного программирования. Использование статической типизации повышает возможность трансформации функционально-потоковых параллельных программ в программы, выполняемые на современных параллельных вычислительных системах. Предложены языковые конструкции. Описаны их синтаксис и семантика. Отмечена необходимость использования принципа единственного присваивания при формировании хранилищ данных конкретного типа. Рассмотрены особенности инструментальной поддержки предлагаемого подхода.
Ключевые слова: парадигмы программирования, параллельное программирование, функционально-потоковое параллельное программирование, статическая типизация, модели параллельных вычислений.

Систематизации парадигм программирования по приоритетам принятия решений

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

Восстановление многомерной формы обращений к линеаризованным массивам в системе SAPFOR

Никита Андреевич Катаев, Владислав Николаевич Василькин
770-787
Аннотация: Система автоматизированного распараллеливания SAPFOR (System FOR Automated Parallelization) включает инструменты для анализа и преобразования программ, основной ее целью является снижение сложности распараллеливания программ. Система SAPFOR ориентирована на исследования многоязыковых вычислительных комплексов, разрабатываемых на языках программирования Фортран и Си. Для анализа программ в этой системе используется низкоуровневое их представление в виде LLVM IR, которое позволяет проводить различные оптимизации с целью повышения качества анализа программ. При этом оно теряет некоторые особенности программы, отражаемые ее представлением на языке высокого уровня. Одной из таких особенностей является многомерная структура используемых массивов. Анализ зависимостей по данным является одним из ключевых при исследовании возможности параллельного выполнения программ. При этом такой анализ относится к классу NP-трудных задач. Знание многомерной структуры массивов позволяет во многих случаях учесть структуру индексных выражений в обращениях к массивам и снизить сложность проводимого анализа. Кроме того, использование многомерных массивов позволяет повысить уровень параллелизма в программе за счет использования многомерных решеток процессоров и распараллеливания гнезд циклов, а не отдельных циклов в гнезде. Данная возможность естественным образом поддерживается в DVM-системе. В настоящей работе рассмотрен подход, применяемый в системе SAPFOR для восстановления формы многомерных массивов и обращений к ним по их линеаризованному представлению в LLVM IR. Предложенный подход был успешно протестирован на различных приложениях, включая тесты производительности из набора NAS Parallel Benchmarks.
Ключевые слова: анализ программ, автоматизация распараллеливания, SAPFOR, DVM, LLVM.

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

Лидия Васильевна Городняя
1090-1116
Аннотация:

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

Ключевые слова: функциональное программирование, парадигмальная декомпозиция, параллельные вычисления, система программирования, мультипарадигмальность.

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

Лидия Васильевна Городняя
472-493
Аннотация: Цель статьи – выбор представления результатов сравнения языков программирования, удобного для оценки выразительной силы языков и трудоёмкости реализации систем программирования. Формы такого представления должны быть приспособлены к обоснованию практичных критериев декомпозиции программ, что можно рассматривать как подход к решению проблемы факторизации весьма усложнённых определений языков программирования. Актуальность выбора лаконичных и быстро воспринимаемых форм полезен для работы в стремительно развивающемся пространстве новых проблемно-ориентирован-ных языков программирования. Попутно можно показывать дистанцию в понятийной сложности между программированием и разработкой систем программирования.
Ключевые слова: системы программирования, декомпозиция программ, реализационная прагматика, парадигмы программирования, критерии декомпозиции, семантические системы, определение языков программирования.

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

Светлана Михайловна Гарина, Татьяна Викторовна Модянова
567-578
Аннотация: Экспертиза в научно-технической сфере имеет более чем трехсотлетнюю историю и за это время во внешних своих формах претерпела существенные изменения. Компьютерные технологии повлияли на процессы организации экспертизы особенно сильно. В статье описана процедура организации экспертизы в конкурсах на получение финансирования в рамках федеральной целевой программы (ФЦП) «Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2014–2020 годы». Разработанные специализированные информационные системы и сервисы, использующие новые технологические средства поиска и обработки данных, дают возможность эксперту всесторонне и глубоко оценить объект экспертизы. Информационная поддержка охватывает все стороны организации экспертизы и деятельности экспертов. Процедура организации экспертизы, используемая в ФГБНУ «Дирекция научно технических программ», и ее информационно-аналитическое сопровождение обеспечивают функционирование современной системы независимой научно-технической экспертизы, позволяют повысить качество оценки проектов и одновременно с этим снизить трудоемкость процесса организации экспертизы и, как следствие, организовывать экспертизу в больших объемах, в сжатые сроки и с минимальными издержками.
Ключевые слова: научно-техническая экспертиза, организация экспертизы, информационное обеспечение, конкурсный отбор, критерии оценки, экспертная оценка, эксперт, информационная система, информационный сервис.

Отладка параллельных программ в DVM-системе

Владимир Александрович Бахтин, Дмитрий Александрович Захаров, Александр Александрович Ермичев, Виктор Алексеевич Крюков
866-886
Аннотация: DVM-система предназначена для разработки параллельных программ научно-технических расчетов на языках C-DVMH и Fortran-DVMH. Эти языки используют единую DVMH-модель параллельного программирования и являются расширением стандартных языков Си и Фортран спецификациями параллелизма, оформленными в виде директив для компилятора. DVMH-модель позволяет создавать эффективные параллельные программы для гетерогенных вычислительных кластеров, в узлах которых в качестве вычислительных устройств наряду с универсальными многоядерными процессорами могут использоваться ускорители, графические процессоры или сопроцессоры Intel Xeon Phi. В статье описыны методика отладки параллельных программ в DVM-системе, а также новые возможности DVM-отладчика.
Ключевые слова: автоматизация разработки параллельных программ, автоматизация отладки параллельных программ, динамический контроль, сравнительная отладка, DVM-система, ускоритель, ГПУ, Фортран, Си.

Веб-среда анализа и преобразований программ в Оптимизирующей распараллеливающей системе

Антон Павлович Баглий
576-593
Аннотация: Описан опыт проектирования различных вариантов веб-среды разработки (IDE) для Оптимизирующей распараллеливающей системы и компилятора на реконфигурируемую архитектуру на основе существующих инструментов, таких, как Jupyter Notebook и Eclise Che. Сформированы требования к инструментам в составе Открытой распараллеливающей системы для поддержки их интеграции в веб-среду разработки, доступную в интернете. Описан процесс создания переносимого окружения для разработки модулей компилятора, демонстрации его работы и обучения навыкам разработки параллельных программ. Приведены примеры использования разработанных преобразований программ, используемых при оптимизации программ для ПЛИС в разработанной веб-среде, и описаны способы визуализации результатов выполнения преобразований и анализа при использовании Jupyter Notebook. Проведенная работа демонстрирует возможность организации удаленного доступа к библиотеке разрабатываемых инструментов оптимизации программ в виде, удобном прикладным разработчикам.
Ключевые слова: интегрированная среда, распараллеливающий компилятор, преобразования программ, ПЛИС, контейнеризация, интерактивная тетрадь, облачные вычисления.

Использование DVM-системы при разработке программы для расчетов задачи радиационной магнитной газодинамики и исследования динамики плазмы в канале КСПУ

Владимир Александрович Бахтин, Дмитрий Александрович Захаров, Андрей Николаевич Козлов, Вениамин Сергеевич Коновалов
594-614
Аннотация: DVM-система предназначена для разработки параллельных программ научно-технических расчетов на языках C-DVMH и Fortran-DVMH. Эти языки используют единую DVMH-модель параллельного программирования и являются расширением стандартных языков Си и Фортран спецификациями параллелизма, оформленными в виде директив для компилятора. DVMH-модель позволяет создавать эффективные параллельные программы для гетерогенных вычислительных кластеров, в узлах которых в качестве вычислительных устройств наряду с универсальными многоядерными процессорами могут использоваться ускорители, графические процессоры или сопроцессоры Intel Xeon Phi. В статье описан опыт успешного применения DVM-системы для разработки параллельного программного кода для расчетов задачи радиационной магнитной газодинамики и исследования динамики плазмы в канале КСПУ.
Ключевые слова: автоматизация разработки параллельных программ, DVM-система, плазменный ускоритель, радиационная магнитная газодинамика.

О разделимости входо-выходных полуавтоматов с недетерминированным поведением

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

Резервы синтаксического конструирования систем программирования

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

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

Лидия Васильевна Городняя
830-856
Аннотация:

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


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

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

Развитие DVM-системы

Валерий Федорович Алексахин, Владимир Александрович Бахтин, Ольга Федоровна Жукова, Дмитрий Александрович Захаров, Виктор Алексеевич Крюков, Наталия Викторовна Поддерюгина, Ольга Антониевна Савицкая
247-270
Аннотация: DVM-система предназначена для разработки параллельных программ научно-технических расчетов на языках C-DVMH и Fortran-DVMH. Эти языки используют единую DVMH-модель параллельного программирования и являются расширением стандартных языков Си и Фортран спецификациями параллелизма, оформленными в виде директив для компилятора. DVMH-модель позволяет создавать эффективные параллельные программы для гетерогенных вычислительных кластеров, в узлах которых в качестве вычислительных устройств наряду с универсальными многоядерными процессорами могут использоваться ускорители, графические процессоры или сопроцессоры Intel Xeon Phi. В статье представлены новые возможности DVM-системы, которые были разработаны в последнее время.
Ключевые слова: автоматизация разработки параллельных программ, DVM-система, ускоритель, ГПУ, Фортран, Си, нерегулярная сетка, неструктурированная сетка.

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

Татьяна Петровна Баранова, Александр Борисович Бугеря, Кирилл Николаевич Ефимкин
42-56
Аннотация:

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

Ключевые слова: параллельное программирование, автоматизация программирования, балансировка вычислительной нагрузки, гибридные архитектуры, язык НОРМА, автоматическая генерация программ .

Гибридная система программирования для учебных исполнителей на Python

Миля Вячеславовна Райко
398-414
Аннотация:

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

Ключевые слова: формальный исполнитель, визуализация, программирование, пиктограммный интерфейс, Python.

Weazet – платформа для соревнований и практики начинающих программистов

Юрий Иосифович Воротницкий, Михаил Георгиевич Зеков
304-311
Аннотация:

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

Ключевые слова: алгоритмизация, программирование, геймификация, дополнительное образование.

Организация вычислений и работы с памятью в учебном языке программирования CИНХРО

Лидия Васильевна Городняя
566-599
Аннотация:

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

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

О формировании профессиональных компетенций будущих техников-программистов в процессе обучения программированию

Фануза Мунировна Саляхова, Зульфия Равильевна Халитова
694-701
Аннотация: Описан опыт формирования профессиональных компетенций будущих техников-программистов при обучении программированию.
Ключевые слова: профессиональные компетенции, структурное и объектно-ориентированное программирование, система программирования Lazarus.

Автоматизация распараллеливания программ для многоядерных процессоров с распределенной локальной памятью

Антон Павлович Баглий, Никита Максимович Кривошеев, Борис Яковлевич Штейнберг
135-153
Аннотация:

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

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

Сравнительный анализ производительности механизмов метапрограммирования в языке Java

Азат Фердинандович Галиуллин, Ирина Сергеевна Шахова
985-996
Аннотация: Использование определенных механизмов метапрограммирования при разработке программных библиотек на языке Java может негативно сказываться на времени сборки и работе конечного программного продукта, в котором они используются. Для того, чтобы нивелировать воздействие различных подходов, необходимо предложить комплексное решение, позволяющее регулировать их использование в зависимости от особенностей контекста, что, в свою очередь, требует проведения предварительного анализа. В данной статье рассмотрены существующие в языке Java механизмы метапрограммирования и представлены результаты сравнения влияния данных подходов на время сборки Android-приложений.
Ключевые слова: annotation processing, Reflection, обработка аннотаций, рефлексия, кодогенерация, производительность, Android, Java.

Опыт верификации реализаций клиента протокола TLS 1.3

Алексей Вячеславович Никешин, Виктор Зиновьевич Шнитман
104-121
Аннотация:

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


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

Ключевые слова: безопасность, TLS, TLSv1.3, протоколы, тестирование, оценка устойчивости, интернет, стандарты, формальные методы спецификации.

Опыт верификации реализаций протокола TLS 1.3

Алексей Вячеславович Никешин, Виктор Зиновьевич Шнитман
902-922
Аннотация:

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


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


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

Ключевые слова: безопасность, TSL, TSLv1.3, протоколы, тестирование, оценка устойчивости, Интернет, стандарты, формальные методы спецификации.
1 - 25 из 97 результатов 1 2 3 4 > >> 
Информация
  • Для читателей
  • Для авторов
  • Для библиотек
Отправить материал
Текущий выпуск
  • Логотип Atom
  • Логотип RSS2
  • Логотип RSS1

Электронные библиотеки

ISSN 1562-5419

Информация

  • О журнале
  • Цели и задачи
  • Тематика
  • Руководство для авторов
  • Отправка материалов
  • Заявление о конфиденциальности
  • Контакты
  • eLIBRARY.RU
  • dblp computer science bibliography

Отправить статью

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

Отправить материал
Больше информации об этой издательской системе, платформе и рабочем процессе от OJS/PKP.

© 2015-2025 Казанский (Приволжский) федеральный университет; Институт развития информационного общества