Формальная верификация реализации хэш-функции «Стрибог» с «Группой Астра»
Язык статьиРусский
Аннотация
Обеспечение доверия к реализациям криптостойких алгоритмов является актуальной задачей современного программирования. К правильности работы таких программных систем предъявляются повышенные требования, поэтому для доказательства корректности таких программ относительно спецификаций применяют дедуктивную верификацию. В данной статье описана работа в прогрессе по доказательству корректности реализации хэш-функции «Стрибог» из ядра Linux относительно ГОСТ Р 34.11-2012. Данная работа стартовала на проекте «Формальная верификация реализации хэш-функции «Стрибог» с «Группой Астра»» на Большой Математической Мастерской 2025 года. В качестве результатов работы мы презентуем формализацию ГОСТ Р 34.11-2012 в системе интерактивного доказательства Rocq. Данная формализация является функциональной спецификацией любой реализации хэш-функции «Стрибог». Также мы презентуем задание спецификаций для базовых функций реализации хэш-функции «Стрибог» из ядра Linux и методы упрощения доказательства таких функций с помощью задания набора лемм о связи структур данных из функциональной спецификации и из данной реализации.
Ключевые слова
УДК004.052.42
Номер
№ 28,
Страницы25-52
Файл
verification_project_paper.pdf
(1.58 МБ)
Библиографическая ссылка
Кондратьев Д.А., Бояндин Л.К., Гончар Г.Е., Марченко В.В., Обухова А.А., Разбитнова Ю.Ю., Хованская А.С., Янбулатов Д.Р. Формальная верификация реализации хэш-функции «Стрибог» с «Группой Астра» // Системная информатика, 2025. – № 28. – С. 25-52. – DOI: https://doi.org/.