Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024) — различия между версиями
Материал из 0x1.tv
StasFomin (обсуждение | вклад) (→Thesis) |
StasFomin (обсуждение | вклад) |
||
| (не показаны 2 промежуточные версии этого же участника) | |||
форме открытых программ достаточно широко, но реализации с удобным графическим интерфейсом иногда плохо
протестированы и имеют небольшой функционал. Поэтому возникла идея собрать воедино множество методов теории
автоматов так, чтобы удовлетворить потребность в наглядности, не теряя в широте охвата преобразований и их
корректности.
Изначально конвертер, включающий эти методы, представлял собой групповую лабораторную работу;
в дальнейшем в проект добавились результаты также нескольких курсовых работ.
</blockquote>
{{VideoSection}}
{{vimeoembed|993361564|800|450}}
{{youtubelink|}}
|U391_Y7RV6k}}
{{SlidesSection}}
[[File:Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf|left|page=-|300px]]
{{----}}
== Thesis ==автоматов так, чтобы удовлетворить потребность в наглядности, не теряя в широте охвата преобразований и их корректности. Изначально конвертер, включающий эти методы, представлял собой групповую лабораторную работу; в дальнейшем в проект добавились результаты также нескольких курсовых работ. Основные требования, предъявляемые к разработке: ;наглядность: — результаты преобразований должны быть представлены в понятной пользователю форме. Для решения этой задачи в качестве базового представления сущностей был выбран язык <tt>LaTeX</tt> и библиотека \textsc{«Tikz}» для отрисовки автоматов. Эти средства наиболее выразительны, и из \LaTeX-формата нетрудно извлечь более простые посредством упрощающих гомоморфизмов. ;расширяемость: — интерфейс должен быть достаточно удобен для пополнения новыми функциями и типами автоматов или других представлений формальных языков. Для решения этой задачи конвертер был спроектирован таким образом, чтобы модули синтаксического разбора, проверки типов и логирования допускали обновления посредством автоматического порождения необходимого кода (исключая «рабский труд» по написанию шаблонного кода). | |||
Текущая версия на 13:13, 7 августа 2024
- Докладчик
- Александр Дельман
Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения.
Актуальные теоретические работы зачастую лишены программных реализаций, или эти реализации удобны в применении только для разработчика (теоретика, написавшего статью). Классическая теория автоматов на уровне элементарного курса представлена в форме открытых программ достаточно широко, но реализации с удобным графическим интерфейсом иногда плохо протестированы и имеют небольшой функционал. Поэтому возникла идея собрать воедино множество методов теории автоматов так, чтобы удовлетворить потребность в наглядности, не теряя в широте охвата преобразований и их корректности.
Изначально конвертер, включающий эти методы, представлял собой групповую лабораторную работу; в дальнейшем в проект добавились результаты также нескольких курсовых работ.
Содержание
Видео
Презентация
Thesis
Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения.
Актуальные теоретические работы зачастую лишены программных реализаций, или эти реализации удобны в применении только для разработчика (теоретика, написавшего статью). Классическая теория автоматов на уровне элементарного курса представлена в форме открытых программ достаточно широко, но реализации с удобным графическим интерфейсом иногда плохо протестированы и имеют небольшой функционал. Поэтому возникла идея собрать воедино множество методов теории автоматов так, чтобы удовлетворить потребность в наглядности, не теряя в широте охвата преобразований и их корректности.
Изначально конвертер, включающий эти методы, представлял собой групповую лабораторную работу; в дальнейшем в проект добавились результаты также нескольких курсовых работ.
Основные требования, предъявляемые к разработке:
- наглядность
- — результаты преобразований должны быть представлены в понятной пользователю форме.
Для решения этой задачи в качестве базового представления сущностей был выбран язык LaTeX и библиотека «Tikz» для отрисовки автоматов. Эти средства наиболее выразительны, и из LaTeX-формата нетрудно извлечь более простые посредством упрощающих гомоморфизмов.
- расширяемость
- — интерфейс должен быть достаточно удобен для пополнения новыми функциями и типами автоматов или других представлений формальных языков. Для решения этой задачи конвертер был спроектирован таким образом, чтобы модули синтаксического разбора, проверки типов и логирования допускали обновления посредством автоматического порождения необходимого кода (исключая «рабский труд» по написанию шаблонного кода).
- связность
- — должна быть возможность демонстрации соотношений между преобразованиями, а также их композициями. Для решения этой задачи было введено понятие цепочки преобразований, а также введены метод Verify (в пользовательском интерфейсе) и метаморфное тестирование[1] (для разработчиков).
Экосистема проекта
В связи с тем, что проект пополнялся не только методами, но и новыми классами автоматов (в частности, «PDA» — стековые автоматы; «MFA» — автоматы с памятью), было решено расширить его экосистему средствами автоматического обновления, позволяющими быстро добавлять в интерфейс новый функционал. В модуль автотестирования помимо юнит-тестов были добавлены метаморфные тесты, проверяющие инвариантность свойств объектов относительно цепочек преобразований. В силу того, что некоторые классы автоматов (в частности, «MFA») имеют неразрешимое отношение эквивалентности, был разработан также фазз-модуль, осуществляющий приблизительную проверку равенства языков соответствующих распознавателей.
Сам конвертер написан на языках C++} (большая часть фронтенда и весь бэкенд) и Refal-5 (форматирующие скрипты для порождения \LaTeX-исходников). В связи с этим, отдельно стоит упомянуть экспериментальный проект Линтера для Refal-5, который служит цели улучшить дисциплину кода, ранее не контролировавшуюся никем, кроме самого разработчика, делающего коммиты, и находится на стадии встраивания в «CI» проекта.
Применение в исследованиях
Хотя изначально конвертер разрабатывался как чисто учебный проект, оказалось, что этот инструмент удобен и для теоретических исследований. В частности, посредством метода Verify удобно перепроверять утверждения на предмет неявных допущений, что показал анализ статьи [2], выявивший несколько неточностей в приведённых формулировках. Кроме того, методы анализа полугрупповых структур показали хорошую скорость и точность при выявлений «REDoS»-ситуаций в академических регулярных выражениях с перекрытиями в подвыражениях[3], для которых методы анализа, использующие самопересечения автоматов [4], работают слишком медленно, а фаззеры[5],[6] — ненадёжно. Последним применением конвертера на данный момент стало исследование бисимуляций в конечных автоматах с памятью посредством аппроксимаций классическими конечными автоматами[7]. Поставленная цель — сделать осязаемыми абстрактные концепции, используемые в современной теории формальных языков, — оказалась полезна не только для сдачи зачётов, но и для испытания новых гипотез.
!.jpg)
Примечания и ссылки
- ↑ 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.
- ↑ C. Allauzen, M. Mohri: A Unified Construction of the Glushkov, Follow, and Antimirov Automata // TR2006-880, Courant Institute of Mathematical Sciences, 2006.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ A. N. Nepeivoda, A. D. Delman, A. S. Terentyeva Bisimulations in Memory Finite Automata // SYRCoSE 2024 Proceedings, 2024.