Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024)

Материал из 0x1.tv

Докладчик
Александр Дельман

Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения.

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

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

Видео

on youtube

Презентация

Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf

Thesis

Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения.

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

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

Основные требования, предъявляемые к разработке:

наглядность
— результаты преобразований должны быть представлены в понятной пользователю форме.

Для решения этой задачи в качестве базового представления сущностей был выбран язык LaTeX и библиотека «Tikz» для отрисовки автоматов. Эти средства наиболее выразительны, и из LaTeX-формата нетрудно извлечь более простые посредством упрощающих гомоморфизмов.

расширяемость
— интерфейс должен быть достаточно удобен для пополнения новыми функциями и типами автоматов или других представлений формальных языков. Для решения этой задачи конвертер был спроектирован таким образом, чтобы модули синтаксического разбора, проверки типов и логирования допускали обновления посредством автоматического порождения необходимого кода (исключая «рабский труд» по написанию шаблонного кода).
связность
— должна быть возможность демонстрации соотношений между преобразованиями, а также их композициями. Для решения этой задачи было введено понятие цепочки преобразований, а также введены метод Verify (в пользовательском интерфейсе) и метаморфное тестирование[1] (для разработчиков).

Экосистема проекта

В связи с тем, что проект пополнялся не только методами, но и новыми классами автоматов (в частности, «PDA» — стековые автоматы; «MFA» — автоматы с памятью), было решено расширить его экосистему средствами автоматического обновления, позволяющими быстро добавлять в интерфейс новый функционал. В модуль автотестирования помимо юнит-тестов были добавлены метаморфные тесты, проверяющие инвариантность свойств объектов относительно цепочек преобразований. В силу того, что некоторые классы автоматов (в частности, «MFA») имеют неразрешимое отношение эквивалентности, был разработан также фазз-модуль, осуществляющий приблизительную проверку равенства языков соответствующих распознавателей.

Сам конвертер написан на языках C++} (большая часть фронтенда и весь бэкенд) и Refal-5 (форматирующие скрипты для порождения \LaTeX-исходников). В связи с этим, отдельно стоит упомянуть экспериментальный проект Линтера для Refal-5, который служит цели улучшить дисциплину кода, ранее не контролировавшуюся никем, кроме самого разработчика, делающего коммиты, и находится на стадии встраивания в «CI» проекта.

Применение в исследованиях

Хотя изначально конвертер разрабатывался как чисто учебный проект, оказалось, что этот инструмент удобен и для теоретических исследований. В частности, посредством метода Verify удобно перепроверять утверждения на предмет неявных допущений, что показал анализ статьи [2], выявивший несколько неточностей в приведённых формулировках. Кроме того, методы анализа полугрупповых структур показали хорошую скорость и точность при выявлений «REDoS»-ситуаций в академических регулярных выражениях с перекрытиями в подвыражениях[3], для которых методы анализа, использующие самопересечения автоматов [4], работают слишком медленно, а фаззеры[5],[6] — ненадёжно. Последним применением конвертера на данный момент стало исследование бисимуляций в конечных автоматах с памятью посредством аппроксимаций классическими конечными автоматами[7]. Поставленная цель — сделать осязаемыми абстрактные концепции, используемые в современной теории формальных языков, — оказалась полезна не только для сдачи зачётов, но и для испытания новых гипотез.

Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024)!.jpg

Примечания и ссылки

  1. T. Y. Chen, S. C. Cheung, S. M. Yiu: Metamorphic testing: A new approach for generating next test cases // TR HKUST-CS98-01, Department of Computer Science, The Hong Kong University of Science and Technology, Hong Kong, 1998.
  2. C. Allauzen, M. Mohri: A Unified Construction of the Glushkov, Follow, and Antimirov Automata // TR2006-880, Courant Institute of Mathematical Sciences, 2006.
  3. A. N. Nepeivoda, Yu. A. Belikova, K. K. Shevchenko, M. R. Teriukha, D. P. Knyazihin, A. D. Delman, A. S. Terentyeva REDoS detection in ``Domino regular expressions by Ambiguity Analysis // Труды ИСП РАН 35(3), 109—124, 2023.
  4. N. Weideman, B. van der Merwe, M. Berglund, B. W. Watson:{Analyzing Matching Time Behavior of Backtracking Regular Expression Matchers by Using Ambiguity of {NFA}} //Proc. of Implementation and Application of Automata - 21st International Conference, {Lecture Notes in Computer Science}, 9705, p.322—334, 2016.
  5. Y. Shen, Y. Jiang, C. Xu, P. Yu, X. Ma, J. Lu: {Re{S}cue: Crafting Regular Expression DoS Attacks} // Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 225—235, 2018.
  6. Y. Liu, M. Zhang, W. Meng: {Revealer: Detecting and Exploiting Regular Expression Denial-of-Service Vulnerabilities} // Proceedings of the 2021 IEEE Symposium on Security and Privacy (SP), 1468—1484, 2021.
  7. A. N. Nepeivoda, A. D. Delman, A. S. Terentyeva Bisimulations in Memory Finite Automata // SYRCoSE 2024 Proceedings, 2024.