R-Verify - отечественная программная платформа автоматизированной верификации программного обеспечения на основе встроенной трассировки выполнения. Продукт обеспечивает формирование структурированной трассы исполнения, фиксацию состояний и событий, сопоставление фактического поведения с заданными целями, сценариями и свойствами корректности. MVP предусматривает модуль трассировки, механизм описания целей и намерений выполнения, анализатор трасс и классификацию выявленных отклонений. В рамках НИР планируется разработать математическую и программную модель P-Verify, реализовать прототип инструментов трассировки и анализа, определить формальные свойства проверяемого поведения и провести апробацию на реальных программных сценариях, включая инфраструктурные системы. Результатом станет работоспособный отечественный MVP, демонстрирующий автоматизированное выявление отклонений поведения программ и формирование воспроизводимого отчета о результатах проверки.

Решаемая проблема

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

Цели реализации проекта

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

Создание отечественной платформы для разработчиков, QA-инженеров, DevOps - команд и специалистов по информационной безопасности. Продукт позволит автоматически получать и анализировать трассы выполнения программ, выявлять отклонения от заданного поведения и формировать отчеты о верификации.

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

Команда

Синцова Ксения — Руководитель проекта, кандидат математических наук, доцент НИЯУ МИФИ. Специалист в области математического моделирования, формальной верификации, теории множеств и применения формальных методов в кибербезопасности. Отвечает за научно-методическую основу R-Verify, разработку математической модели и методов верификации.

Шилов Игорь — Главный разработчик/Архитектор, специалист в области информационных технологий и программно-сетевой инфраструктуры. Имеет опыт работы с Linux/Unix, FreeBSD, Asterisk, сетевым оборудованием, серверным администрированием и тестированием. Отвечает за архитектуру и программную реализацию MVP, интеграцию, тестирование и практическую апробацию продукта.

При необходимости для ускорения разработки MVP возможно привлечение дополнительных разработчиков.

На страницу проекта