Система трансформації подій інтерфейсу користувача у формальні логічні специфікації для автоматизованої верифікації

Abstract

Об’єктом дослідження є взаємодія користувача з графічним інтерфейсом і вимоги безпеки авторизації. Предметом дослідження – автоматизоване перетворення UI-подій на темпоральні специфікації та їх формальна верифікація. Метою роботи є розробка системи, що будує формальну модель поведінки за спостережуваними подіями інтерфейсу, автоматично генерує LTL/CTL/TLA+-властивості та перевіряє їх засобами model checking з поясненням порушень. Методи дослідження – темпоральні логіки, перевірка моделей, шаблони специфікацій, каузальні графи трейсів, гібридна нормалізація намірів, Python (PySide6, Pydantic, NetworkX, PyTorch), експериментальна верифікація. У результаті створено систему uiformal і демонстрацію LogisTek App, Monitor для авторизації з PBKDF2, TOTP і блокуванням облікового запису. Система виявляє обхід 2FA, прямий доступ і порушення властивостей відгуку форми. На 7 сценаріях підтверджено коректність верифікації; час конвеєра – 0,5–7,7 мс; реалізацію перевірено 23 тестами. Система автоматично виявляє небезпечні сценарії доступу – обхід двофакторної автентифікації, прямий доступ до захищених розділів, порушення властивостей відгуку форми – формулюючи їх як порушення темпоральних властивостей безпеки.