КАРТОЧКА ПРОЕКТА,
ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ

Информация подготовлена на основании данных из Информационно-аналитической системы РНФ, содержательная часть представлена в авторской редакции. Все права принадлежат авторам, использование или перепечатка материалов допустима только с предварительного согласия авторов.

 

ОБЩИЕ СВЕДЕНИЯ


Номер 18-71-00150

НазваниеРазработка эволюционных стратегий поиска декомпозиций трудных вариантов задачи о булевой выполнимости с применением к обращению криптографических функций.

РуководительУльянцев Владимир Игоревич, Кандидат технических наук

Организация финансирования, регионфедеральное государственное автономное образовательное учреждение высшего образования "Национальный исследовательский университет ИТМО", г Санкт-Петербург

Срок выполнения при поддержке РНФ 07.2018 - 06.2020 

КонкурсКонкурс 2018 года по мероприятию «Проведение инициативных исследований молодыми учеными» Президентской программы исследовательских проектов, реализуемых ведущими учеными, в том числе молодыми учеными

Область знания, основной код классификатора 01 - Математика, информатика и науки о системах, 01-201 - Искусственный интеллект и принятие решений

Ключевые словаИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ, КРИПТОАНАЛИЗ, ОБРАЩЕНИЕ КРИПТОГРАФИЧЕСКОЙ ФУНКЦИИ, ЗАДАЧА О БУЛЕВОЙ ВЫПОЛНИМОСТИ (SAT), ЭВОЛЮЦИОННЫЕ АЛГОРИТМЫ, ГЕНЕТИЧЕСКИЕ АЛГОРИТМЫ, SAT-РЕШАТЕЛЬ, SAT-ДЕКОМПОЗИЦИЯ

Код ГРНТИ27.41.41


СтатусУспешно завершен


 

ИНФОРМАЦИЯ ИЗ ЗАЯВКИ


Аннотация
Уровень безопасности систем и протоколов передачи данных критически зависит от того, насколько обоснована стойкость используемых для защиты этих данных криптографических алгоритмов. Ввиду большого разнообразия подходов, используемых для защиты данных, ценными представляются автоматические методы, позволяющие аргументированно сравнивать стойкость различных криптографических алгоритмов. В основе таких методов должна лежать комбинаторная задача с мощной и хорошо развитой алгоритмикой. Ряд последних исследований показывает, что одной из самых многообещающих в этом плане является задача о булевой выполнимости (SAT). В рамках настоящего исследования планируется разработать новые методы поиска декомпозиционных представлений трудных вариантов задачи о булевой выполнимости и применить разработанные алгоритмы к задачам криптоанализа ряда современных шифров. Конкретно, ожидается, что будут построены новые алгоритмы, основанные на эволюционных принципах, которые позволят находить декомпозиционные представления SAT-задач (т.н. «SAT Partitionings») с лучшей оценкой трудоемкости решения, чем у известных методов. Подчеркнем, что эволюционные алгоритмы будут использоваться на этапе декомпозиции трудных вариантов (экземпляров) задачи SAT, но не при решении самих SAT-формул. Предполагается, что разработанные алгоритмы позволят для ряда шифров построить новые атаки из класса «угадывай и определяй» (guess-and-determine), которые окажутся эффективнее известных. Предполагается разработка новых стратегий параметризации SAT-решателей для их использования в задачах криптоанализа (SAT-based cryptanalysis). В этом направлении также планируется детальный анализ возможностей применения эволюционных стратегий. Актуальность настоящего исследования обосновывается тем, что методы криптоанализа являются важной составной частью процессов разработки новых систем шифрования. Современные алгоритмы решения SAT в последние годы весьма успешно применяются в криптоанализе, что позволяет рассматривать их как основу для построения целого ряда атак на известные и разрабатываемые криптографические примитивы и шифры. Тем самым такие алгоритмы могут выполнять функции экспертных систем, выдавая оценки стойкости исследуемых криптографических конструкций. В дальнейшем наиболее стойкие такие конструкции могут использоваться при разработке реальных шифров. Научная новизна настоящего исследования состоит в разработке основанных на новых принципах методов поиска декомпозиционных представлений трудных вариантов задачи SAT. Также будут предложены новые методы подбора оптимальных параметров запуска SAT-решателей для рассматриваемого класса SAT-формул. Предполагается, что разработанные методы позволят построить новые криптографические атаки, более эффективные, чем известные. Также предполагается использовать разработанные методы для аргументированного сравнения между собой различных криптографических систем.

Ожидаемые результаты
Ожидается, что в ходе выполнения проекта будут разработаны и программно реализованы новые методы построения декомпозиционных представлений булевых формул в контексте решения задачи о булевой выполнимости (SAT). Применительно к задачам криптоанализа каждая такая декомпозиция соответствует некоторой криптографической атаке, относящейся к классу “угадывай и определяй” (guess-and-determine). Новизна разрабатываемых алгоритмов заключается в использовании эволюционных стратегий для оценивания эффективности конкретной декомпозиции (и, как следствие, трудоемкости соответствующей guess-and-determine атаки) через оптимизацию специальных оценочных функций black-box типа. Относительно недавние работы по данной тематике демонстрируют, что использование SAT в связке с black-box оптимизацией позволяет для ряда шифров построить рекордные или близкие к рекордным guess-and-determine атаки. Предполагается, что использование новых эволюционных стратегий позволит существенно улучшить эти результаты. Представляется, что созданная в рамках выполнения проекта программная среда, в которой возможно тестирование стойкости различных криптографических примитивов к guess-and-determine атакам, будет востребована при разработке новых скоростных криптографических алгоритмов. Разработанные и реализованные алгоритмы построения guess-and-determine атак предполагается протестировать на ряде криптографических генераторов ключевого потока (Bivium, Toy-Trivium, Trivium, Grain и др.) в параллельных и распределенных вычислительных средах.


 

ОТЧЁТНЫЕ МАТЕРИАЛЫ


Аннотация результатов, полученных в 2018 году
В современной информационной безопасности криптографические методы играют одну из центральных ролей. Расширение сферы применения методов защиты информации и появление новых угроз приводит к росту множества криптографических конструкций. Зачастую это делает нетривиальной проблему выбора того или иного шифра для решения конкретной задачи на конкретном типе устройств и платформ. В силу сказанного актуальной является проблема использования интеллектуальных методов, позволяющих оценивать стойкость потоковых шифров к тем или иным видам криптографических атак, сравнивать стойкость различных шифров и в итоге выбирать наилучший шифр в применении к конкретной ситуации. Настоящий проект направлен на разработку нового подхода к оценке стойкости заданного алгоритма потокового шифрования. Проект развивает (при активной совместной коллаборации) результаты исследований научной группы, возглавляемой Семеновым А.А. в ИДСТУ СО РАН. В последних работах указанного коллектива задачи построения одного класса атак были сведены к проблеме минимизации специальных оценочных функций Black-Box типа. Более точно, функции, введенные в [Semenov et al. 2016, 2018], позволяют осуществлять сравнительный анализ стойкости различных шифров к алгебраическим атакам, относящимся к классу guess-and-determine и использующим представление задачи в виде булевой формулы SAT. В большинстве случаев, поиск декомпозиционного множества (guessed bits set) осуществляется вручную посредством анализа особенностей рассматриваемого шифра и соответствующей шифру SAT-формулы. Ранее в упомянутых работах был предложен подход, в рамках которого задача поиска декомпозиции ставится как задача оптимизации специальной псевдобулевой функции Black-Box типа, значения которой стохастически оценивают трудоемкость соответствующей guess-and-determine attack. Для оптимизации авторы использовали алгоритмы поиска с запретами (Tabu Search) и имитации отжига (Simulated Annealing). В настоящем проекте впервые для поиска декомпозиционного множества разрабатываются и применяются эволюционные алгоритмы. В рамках первого этапа выполнения проекта были получены следующие результаты: 1. Разработаны новые эволюционные алгоритмы (ЭА) оптимизации оценочных функций black-box типа, оценивающих эффективность SAT-декомпозиций в задачах SAT-based криптоанализа. В качестве стратегий направленного поиска после ряда предварительных исследований выбраны (1+1)-ЭА и генетический алгоритм (ГА) с размером популяции 10. Отдельного внимания заслуживает предложенная модификация функции приспособленности (ФП), так называемая адаптивная стратегия. При начальных этапах запуска алгоритма используется меньший размер выборки Монте-Карло (например, M=10), используемый для вычисления ФП. Это ведет к потере точности функции, но при этом существенно ускоряется работа алгоритма на начальных этапах. При приближении к локальному оптимуму для повышения точности вычисления ФП используется стандартный для задачи размер выборки (например, M=1000). 2. Разработанные алгоритмы реализованы в виде программных приложений, эффективно работающих в параллельных и распределенных вычислительных средах. Исходные коды и средства запуска расположены в открытом репозитории (https://github.com/lytr777/CryptoEv). Любой желающий имеет возможность ознакомиться с деталями реализации и инструкциями запусков. Вычисления в распределенных системах реализованы с использованием программного интерфейса MPI. Реализация была успешно апробирована на вычислительных кластерах Университета ИТМО и Иркутском вычислительном кластере «Академик В.М. Матросов». 3. Был проведен ряд экспериментальных исследований по использованию разработанных и реализованных алгоритмов для построения guess-and-determine атак на ряд поточных шифров. С детальными результатами экспериментальных исследований можно ознакомиться в опубликованной работе “Evolutionary Computation Techniques for Constructing SAT-Based Attacks in Algebraic Cryptanalysis”. Для экспериментов было выбрано шесть алгоритмов потокового шифрования. Для четырех из них были построены новые декомпозиционные множества с лучшими оценками времени SAT-атаки, чем у построенных предложенными ранее алгоритмами. Таким образом, была показана применимость на практике разработанных и реализованных алгоритмов. По результатам работ была опубликована статья (https://link.springer.com/chapter/10.1007/978-3-030-16692-2_16) в трудах конференции EvoStar 2019, являющейся одной из самых признанных в области эволюционных вычислений. Были сделаны устный и постерные доклады в Лейпциге, Германия (постер и презентацию можно найти на личной странице руководителя проекта http://rain.ifmo.ru/~ulyantsev/papers.html).

 

Публикации

1. Павленко А.Л., Семенов А.А., Ульянцев В.И. Evolutionary Computation Techniques for Constructing SAT-Based Attacks in Algebraic Cryptanalysis Applications of Evolutionary Computation. EvoApplications 2019. Lecture Notes in Computer Science, Vol. 11454, P. 237-253 (год публикации - 2019).


Аннотация результатов, полученных в 2019 году
Второй и заключительный этап проекта продолжает исследования, направленные на разработку новых методов для анализа устойчивости алгоритмов потокового шифрования, основанных на применении эволюционных алгоритмов и SAT-решателей. 1. Были разработаны усовершенствования предложенных в первом этапе эволюционных алгоритмов оптимизации оценочных Монте-Карловских функций black-box типа, оценивающих эффективность SAT-декомпозиций в задачах SAT-based криптоанализа. Основное усовершенствование заключается в модернизации функции приспособленности (ФП) за счет использования статистических тестов. Во время работы алгоритма оптимизации проверяется множество SAT-декомпозиций, эффективность которых хуже текущего решения. Для таких декомпозиций можно прервать вычисления на более ранних стадиях вычисления ФП, которая в настоящем проекте вычисляется итеративно и требует большого числа вычислительных ресурсов. Для решения о прерывании текущая выборка результатов запусков SAT-решателей оценивается на каждой итерации при помощи критерия Уилкоксона. 2. Был реализован программный фреймворк EvoGuess (https://github.com/ctlab/EvoGuess) для оценки стойкости алгоритмов потокового шифрования к SAT-based атакам. Данный фреймворк состоит из четырех модулей и включает в себя разработанные ранее методы и их улучшения. Включена возможность использования как параметризуемых, так и непараметризуемых SAT-решателей ROKK, Lingeling, Treengeling, MiniSat, CryptoMiniSAT, PaInleSS, Glucose, Maple, Minicard. Реализованный фреймворк находится в открытом доступе, его можно использовать как для криптоанализа алгоритмов шифрования, так и для реализации аналогичных исследовательских проектов, подразумевающих параллельное решение множества SAT-формул в процессе работы алгоритма оптимизации. 3. С реализованным фреймворком EvoGuess были проведены экспериментальные исследования. Подтверждена целесообразность использования статистических тестов и параметризованных SAT-решателей в задачах SAT-based криптоанализа. В данной серии экспериментов исследовались алгоритмы потокового шифрования A5/1, Bivium, Trivium-64, Trivium-96 на пяти идентичных узлах Иркутского вычислительного кластера «Академик В.М. Матросов». Полученные результаты показали, что разработанные улучшения позволили с использованием тех же ресурсов рассмотреть в разы большее число потенциальных декомпозиционных множеств: в 4.31 раза для A5/1; в 1.48 раза для Bivium; в 2.56 раза для Trivium-64 и в 1.92 раза для Trivium-96. Были построены новые декомпозиционные множества с улучшенными оценками. По результатам второго этапа работ была опубликована статья (doi.org/10.1145/3321707.3321847) в трудах конференции GECCO 2019 (ранг A), являющейся самой известной в области эволюционных вычислений. Статья с описанием фреймворка (doi.org/10.23919/MIPRO.2019.8757214) была опубликована в трудах конференции MIPRO. Были сделаны устные доклады в Праге, Чехия; Опатии, Хорватия; а также на Конгрессе Молодых Ученых в Санкт-Петербурге (презентации доступны на личной странице руководителя проекта http://rain.ifmo.ru/~ulyantsev/papers.html).

 

Публикации

1. - Ученые Университета ИТМО представили рекордное количество работ на конференции по эволюционным вычислениям GECCO-2019 в Праге ITMO.NEWS, - (год публикации - ).

2. Павленко А., Буздалов М., Ульянцев В. Fitness Comparison by Statistical Testing in Construction of SAT-Based Guess-and-Determine Cryptographic Attacks GECCO 2019 - Proceedings of the 2019 Genetic and Evolutionary Computation Conference, ACM, P. 312-320 (год публикации - 2019).

3. Павленко А., Семенов А., Ульянцев В., Заикин О. Parallel framework for evolutionary black-box optimization with application to algebraic cryptanalysis 2019 42nd International Convention on Information and Communication Technology, Electronics and Microelectronics, MIPRO 2019 - Proceedings, IEEE, P. 1144-1149 (год публикации - 2019).


Возможность практического использования результатов
Результаты проекта могут быть использованы следующим образом: 1. Совершенствование технологий проверки и стандартизации каналов передачи данных в части применяемых алгоритмов потокового шифрования (Приоритет 20д НТР РФ). 2. Упрощение задачи выбора того или иного шифра при создании программного обеспечения для новых устройств, платформ и протоколов. 3. Использование реализованного фреймворка для реализации аналогичных исследовательских проектов, подразумевающих параллельное решение множества SAT-формул в процессе работы алгоритма оптимизации (Приоритет 20а НТР РФ). 4. Использование разработанных техник ускорения в реализации методов оптимизации, вычисляющих функцию приспособленности при помощи метода Монте-Карло. 5. Использование результатов в образовательном процессе Университета ИТМО (или любого другого вуза) - в курсовых проектах и при чтении дисциплин “Эволюционные алгоритмы” и “Теория информации и методы кодирования”.