Author: Семёнов Александр Анатольевич
В докладе предполагается рассмотреть общую проблему обращения эффективно вычислимых дискретных функций (то есть функций, преобразующих двоичные слова в двоичные слова).
Проблема обращения заключается в том, чтобы по известному образу и известному описанию функции (в нашем случае таким описанием является алгоритм) найти неизвестный прообраз. Большое число практически важных задач, в том числе различные задачи криптоанализа, можно рассматривать как частные случаи проблемы обращения эффективно вычислимых дискретных функций. Построение «практически эффективных» вычислительных методов для решения задач обращения – крайне важная и актуальная проблема. «Практическая эффективность» того или иного метода/алгоритма должна быть убедительно аргументирована. В этом плане задачи криптоанализа могут выступать в роли таких аргументов – если метод успешно справляется с криптографическими тестами, он, как правило, эффективен и на задачах, вычислительная трудность в которые не закладывалась искусственно.
В докладе будут рассмотрены механизмы сведения задач обращения дискретных функций к системам булевых уравнений. Для решения последних используются SAT-решатели, базирующиеся на алгоритме DPLL, а также двоичные диаграммы решений (BDD). Будут представлены результаты по решению (с применением SAT- и BDD-решателей) задач криптоанализа некоторых систем шифрования в распределенных вычислительных средах. Будут приведены примеры использования SAT- и BDD-подходов в биоинформатике (в исследовании дискретных моделей генных сетей).
Посмотреть презентацию
Посмотреть видео лекции
Минимальные требования к знаниям слушателей:
- стандартный университетский курс дискретной математики;
- начальные главы математической логики (в объеме исчисления высказываний);
- представления о вычислительной сложности алгоритмов.
Рекомендуется к прочтению по BDD:
- Meinel Ch., Theobald T. Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications. Springer-Verlag, Berlin, Heidelberg, New York, 1998 (доступна в Интернете);
- Ю.Г. Карпов Model Checking. Верификация параллельных и распределенных программных систем. "БХВ-Петербург", 2010 (BDD не является основной темой данной книги).