Методы работы с SMT-решателями

Постановка задачи

При решении некоторых заданий CTF (особенно из категорий Crypto и Reverse) возникает необходимость обратить некоторый алгоритм. В таких заданиях неизвестный флаг подвергается определённому преобразованию, а игроку выдаётся результат этого преобразования и сам алгоритм в виде кода. Очевидно, что если в обратном порядке произвести операции, являющиеся обратными к исходным, то получится искомый флаг. В математическом смысле, процесс решения заданий такого рода сводится к решению уравнения (или их системы).

В качестве примера в данной работе рассмотрим алгоритм шифра Цезаря с ключом равным 3:

flag = 'ravenctf<caw-caw-caw>'

def encrypt(msg):
    "".join(list(map(lambda x : chr(ord(x)+3), msg)))

print(encrypt(flag))

Результатом работы этой программы будет строка 'udyhqfwi?fdz0fdz0fdzA', которая вместе с функцией encrypt будет дана в задании, а переменная flag будет удалена из кода программы:

flag = '???'
# udyhqfwi?fdz0fdz0fdzA

def encrypt(msg)
    ...

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

Принимая исходный символ флага за неизвестную переменную x, можно записать

\(x + 3 = \text{'u'} ,\)

где под 'u' понимается ASCII-код соответствующего символа, т.е. 117. Конечно, это уравнение достаточно простое, чтобы его можно было решить вручную. Однако, в общем случае, уравнение требуется решить программно.

Решение методом грубой силы

Любое уравнение можно попытаться решить простым перебором значений неизвестной переменной. В численной математике подобный метод даже не рассматривается из-за того, что область определения функций в математике чаще всего представляется бесконечным множеством. В нашем примере, однако, мы точно знаем, что каждый символ флага является символом таблицы ASCII, а значит область возможных значений переменной x - [0, 255] (точнее говоря, [32, 126], так как нас не интересуют спецсимволы от 0 до 31 и нелатинские буквы от 127 до 255).

Реализуем bruteforce-решатель для нашего примера на Python:

def bruteforce_solver(known_letter):
    for x in range(32, 127):
        if x + 3 == ord(known_letter):
            return chr(x)
    return "Решение не найдено"

Решим первые три уравнения, чтобы получить первые три символа флага:

>>> bruteforce_solver('u')
'r'
>>> bruteforce_solver('d')
'a'
>>> bruteforce_solver('y')
'v'

Недостаток данного подхода очевиден - могут потребоваться большие вычислительные ресурсы для решения сложных уравнений. Однако, в решении полным перебором есть и неожиданное преимущество. Если внимательно посмотреть на условие в операторе if, то можно заметить, что оно почти полностью повторяет код трансформации символа в функции encode. Иными словами, при решении уравнений методом перебора не нужно находить обратный алгоритм трансформации.

Аналитическое решение

Вторым подходом к проблеме является решение уравнения аналитически “на бумаге”, а затем программирование алгоритма, реализующего найденное аналитическое решение. Под аналитическим решением понимается преобразование исходной формулы в такой вид, в котором неизвестная находится в одной части уравнения, а все известные величины - в другой.

В нашем случае достаточно перенести 3 из левой части в правую:

\(x + 3 = \text{'u'}\)

\(x = \text{'u'} - 3\)

Неизвестной здесь является переменная x, которая обозначает символ исходной строки (флага) до преобразования. В правой части находится константа 3 и известная изменяющаяся переменная, значения которой берутся из результирующей строки. Это аналитическое решение теперь можно записать в виде функции на Python:

def anal_solver(symbol):
    return chr(ord(symbol) - 3)

Можно заметить, что эта функция реализует трансформацию, являющуюся обратной к encrypt. Применив эту функцию таким же образом, каким мы применяли bruteforce_solver, мы получим тот же самый ответ:

>>> anal_solver('u')
'r'
>>> anal_solver('d')
'a'
>>> anal_solver('y')
'v'

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

Применение SMT-решателей

Существует ещё один метод программного решения уравнений и других видов задач на ограничения. SMT-решателем (SMT-солвером, англ. SMT solver) называется программа, принимающая на вход выражение логики первого порядка и определяющая, является ли это выражение выполнимым. Под выполнимостью понимается возможность подобрать такие значения переменных, входящих в выражение, что это выражение станет истинным. Переменные объявляются под квантором существования или всеобщности, после которых следут ограничения, которым должно удовлетворять решение. Например, чтобы найти площадь прямоугольника со сторонами a=6 и b=4, нужно составить следующее выражение:

\(\exists S, a, b:\)

\(S = a*b,\)

\(a = 6,\)

\(b = 4.\)

Результатом работы решателя являются допустимые назначения переменных, фигурироваших под квантором:

\(S = 24,\)

\(a = 6,\)

\(b = 4.\)

Нетрудно заметить, что такой способ передачи данных в решатель позволяет не обращать формулу для того, чтобы найти какую-либо другую переменную. Например, если бы нам была известна площадь S и сторона прямоугольника b, то чтобы найти неизвестную сторону a достаточно было бы лишь немного изменить входное выражение:

\(\exists S, a, b:\)

\(S = a*b,\)

\(S = 24,\)

\(b = 4.\)

Именно эта особенность делает SMT-решатели привлекательным инструментом для решения многих задач CTF.

Современные SMT-решатели принимают входные данные на языке, называемом SMTLib. Этот язык построен на основе S-выражений, поэтому человеку писать на нём некомфортно. Вместо этого для конкретных решателей существуют библиотеки для распространённых языков программирования, называемые привязками (англ. binding), которые позволяют выражать задачи для решателя в виде кода на Python, C# и других языках. Далее будем рассматривать SMT-решатель Z3 и привязки к нему для Python.

Код для решения задачи о прямоугольнике имеет следующий вид:

# импортируем модуль Z3 в глобальную область видимости
from z3 import *

# создаём переменные
# соответствует введению переменных под квантор существования
# используем конструктор Int(), т.к. нас интересуют решения в целых числах
S = Int('S')
a = Int('a')
b = Int('b')

# создаём объект решателя
# в программе можно использовать несколько объектов
# для параллельного решения независимых задач
solver = Solver()

# добавляем ограничения, которым должен удовлетворять результат
# соответсвует выражениям, которые следовали после ':' в
# математической нотации
solver.add(S == a*b)
solver.add(a == 6)
solver.add(b == 4)

# вызов .check() запускает непосредственное решение задачи
if solver.check() == sat:
    # если результат вызова .check() равен значению sat,
    # это означает, что задача выполнима, т.е. для всех переменных
    # были подобраны подходящие значения
    # вызов .model() вернёт их в виде списка
    print(solver.model())
else:
    print("Решение не найдено")

Если задача имеет несколько решений, то можно заставить решатель найти их, добавляя дополнительные ограничения после вызова .model():

from z3 import *

x = Int('x')
s = Solver()

# нужно решить неравенство x > 5
s.add(x > 5)

s.check()
print(s.model()) # выведет x = 6

# добавляем условие, полученное из предыдущего ответа
s.add(x != 6)

s.check()
# решатель вынужден искать другое решение, т.к. мы
# отвергли x = 6
print(s.model()) # выведет x = 7

В заключении, приведём код, который решает первоначальный пример с шифром Цезаря целиком:

from z3 import *

encrypted_flag = 'udyhqfwi?fdz0fdz0fdzA'
decrypted_flag = ''

for e in encrypted_flag:
    d = Int('d')
    s = Solver()

    # уравнение для символа флага
    s.add(d + 3 == ord(e))
    # дополнительные ограничения из таблицы ASCII
    # в методе .add() можно перечислять сразу несколько
    # ограничений в виде отдельных аргументов
    s.add(d >= 32, d < 127)

    s.check()
    # результат вызова .model можно сохранить в переменную,
    # чтобы извлекать из неё отдельные значения модели
    m = s.model()
    # значения, извлечённые из модели нужно конвертировать
    # в соответствующие базовые типы Python
    d_value = m[d].as_long()
    # превращаем код символа в символ
    decrypted_symbol = chr(d_value)
    print("Расшифрованный символ: " + decrypted_symbol)

    decrypted_flag = decrypted_flag + decrypted_symbol

print("Расшифрованный флаг: " + decrypted_flag)

Контрольные вопросы.

Задание на лабораторную работу.

Варианты заданий.

Вариант 1

Вариант 2

Вариант 3

Вариант 4

Вариант 5

Вариант 6

Вариант 7

Вариант 8

Вариант 9

Вариант 10

Вариант 11

Вариант 12

Вариант 13

Вариант 14

Вариант 15