Symbolic execution. Первое знакомство с angr
1. Введение
В современном мире кибербезопасности, где угрозы становятся все более изощренными и сложными, традиционные методы анализа уязвимостей часто оказываются недостаточными. Поиск и устранение уязвимостей – это непрерывный процесс, требующий постоянного совершенствования инструментов и техник. В этой статье мы познакомимся с одним из самых мощных и перспективных подходов – символьным исполнением (символическое выполнение, symbolic execution), и рассмотрим, как его можно эффективно использовать с помощью библиотеки angr.
Традиционно, анализ безопасности опирается на два основных подхода: статический и динамический анализ. Статический анализ, такой как сканирование кода на предмет известных шаблонов уязвимостей, имеет ряд ограничений. Он часто выдает большое количество ложных срабатываний, особенно в сложных проектах, и не может определить, какие участки кода действительно будут выполнены при конкретных входных данных. При этом необходимо иметь доступ к исходному коду приложения (white-box), что не всегда возможно при независимом исследовании приложения.
С точки зрения reverse-engineering (black/gray -box тестирования), применяется дизассемблирование и декомпиляция, с дальнейшим ручным анализом. В этом случае полный анализ приложения требует огромного количества времени и экспертизы, а зачастую практически невозможен из-за размеров современных программ. И даже при таком подходе нет никакой гарантии результата.
Динамический анализ, с другой стороны, предполагает выполнение программы с конкретными входными данными и мониторинг ее поведения. Этот подход позволяет обнаружить уязвимости, которые проявляются только во время выполнения, но он требует тщательного выбора входных данных для обеспечения достаточного покрытия кода. Поиск входных данных, которые активируют "глубокие" или редко используемые участки кода, может быть чрезвычайно сложной задачей, особенно для больших и сложных программ. Кроме того, динамический анализ не гарантирует, что все возможные пути выполнения будут исследованы. Если входные данные не приведут к выполнению уязвимого участка кода, он останется незамеченным. Более того, уязвимые состояния часто связаны с пограничными значениями переменных, вследствие этого, достижение уязвимого участка программы не всегда означает обнаружение уязвимости.
Рассмотрим простой пример:
#include <stdio.h> int main(int argc, char *argv[]){ char name[10]; scanf("%s", name); // buffer overflow printf("Hello, %s\n", name); return 0; }
Классическое переполнение буфера - программа, которая принимает строку в качестве входных данных и копирует ее в буфер фиксированного размера. Статический анализатор может обнаружить эту уязвимость, но определить конкретные входные данные для ее эксплуатации - нет. Динамический анализ потребует представления строки, которая превышает размер буфера, чтобы вызвать переполнение. Если же мы представим строку меньшего размера, уязвимость останется незамеченной.
2. Symbolic execution.
Символьное исполнение предлагает элегантное решение этих проблем. Вместо анализа программы с конкретными входными данными мы можем использовать символьные переменные, такие как "x", которые представляют любое возможное значение. Проходя по ветвям исполнения программы строится предикат пути - логическое выражение, которое описывает ограничения входных данных. Таким образом, символическое выполнение позволяет потенциально обеспечивать очень высокое покрытие путей выполнения, недостижимое другими методами, хотя для очень больших программ полное покрытие может быть ограничено проблемой “взрыва состояний” (state explosion), когда количество возможных путей растет экспоненциально, делая полный анализ вычислительно затратным.
Усложним предыдущий пример, теперь программа не просто спрашивает имя и здоровается, а на основе вашего баланса и возраста вычисляет коэффициент, и в определенном случае предлагает сохранить данные, где и находится уязвимость переполнения буфера.
Движок символьного исполнения разделит эту программу на три пути, и для каждого из них будут сформированы соответствующие ограничения (предикаты). Это позволяет нам находить условия, которые "активируют" определенные участки кода, даже если они редко выполняются.
Теперь мы можем представить программу как “дерево выполнения” где каждый узел будет соответствовать конкретному символьному состоянию, а ветви - это различные пути, обусловленные условными переходами. Чтобы полностью понять, как это работает, давайте разберем ключевые концепции, лежащие в основе этого подхода, а именно: SMT-решатель, символьные переменные, и символьное состояние.
Satisfiability Modulo Theories (SMT, Задача выполнимости формул в теориях) - это задача разрешимости для логических формул с учетом лежащих в их основе теорий, например, теории целых и вещественных чисел, списков, битовых векторов и т.п.
В нашем случае будет использоваться теория битовых векторов. Вычисления с ними во многом аналогичны операциям с целыми числами, но с одним ключевым отличием: хранимое значение ограничено размером вектора. Если результат операции не помещается в отведенное количество бит, его старшая часть, выходящая за пределы вектора, отбрасывается. С математической точки зрения, это означает, что все арифметические операции выполняются по модулю 2^N, где N — размер вектора в битах.
Например, для переменной размером 1 байт (N=8), вычисления производятся по модулю 2^8 = 256. Диапазон ее значений — от 0 до 255. Если к максимальному значению 255 прибавить 1, результатом будет (255 + 1) mod 256 = 0. Этот принцип работает для векторов любого размера, будь то стандартный word (N=16, модуль 65536) или нестандартный вектор в 3 бита (N=3, модуль 8).
Для решения практических задач используются SMT-решатели. Наиболее известный из них - Z3, разработанный командой Microsoft Research, именно он используется для решения логических выражений в фреймворке angr.
Символьная переменная - это переменная, которая обозначает неизвестное значение, однако может использоваться в вычислениях. В каком-то смысле она ближе к понятию “переменная” из математики, чем к программированию.
В процессе символьного исполнения из этих переменных строятся символьные выражения. Например, чтобы дойти до узла 3 (рис. 2) необходимо, чтобы balance был > 0 и age >= 18, а далее, чтобы дойти до узла 6, добавляется условие, что отношение баланса к возрасту должно быть не меньше 1000.
Получившееся выражение передается в SMT-решатель, он позволяет ответить на вопросы: является ли этот участок кода вообще достижимым? Можем ли мы найти конкретное значение для переменных, чтобы попасть в эту ветвь?
Результат может быть SAT и UNSAT:
SAT (Satisfable): означает, что решение существует, и его можно вычислить
UNSAT (Unsatisfable): означает: ”нет, не существует такого значения, которое удовлетворяло бы всем условиям одновременно”. Т.е. данный путь выполнения в программе недостижим.
Символьное состояние программы - это совокупность значений переменных, регистров и ячеек памяти при символьном исполнении программы. Главным отличием от “традиционного” состояния является то, что помимо конкретных значений, в регистрах и ячейках памяти могут содержаться логические выражения.
3. Angr
Теперь, когда мы разобрались с теоретическими основами символьного исполнения, самое время познакомиться с инструментом, который воплощает эти идеи в жизнь. angr – это мощный и гибкий фреймворк для анализа бинарных файлов, написанный на Python. Он предоставляет богатый набор инструментов для автоматизации задач обратной разработки (reverse-engineering) и поиска уязвимостей (vulnerability research), и в его основе лежит именно движок символьного исполнения.
Angr позволяет нам программно исследовать бинарные файлы, не запуская их в традиционном смысле. Он абстрагирует сложные детали архитектуры процессора и операционной системы, позволяя нам сосредоточиться на логике программы.
3.1. Установка angr
Существует несколько способов установки angr на свою систему, они описаны здесь. Наиболее простым, является установка через pip.
# pip install angr
Проверить успешность установки можно в самой командной строке python:
>>> import angr >>> angr.__version__ '9.2.100'
3.2. Ключевые компоненты angr
После того, как окружение подготовлено, мы можем переходить к практике. Работа с angr строится вокруг нескольких основных объектов, которые соответствуют концепциям, рассмотренным нами ранее.
Первый ключевой компонент angr - это Project, он является главным объектом во всем исследовании. Объект Project создается путем загрузки бинарного файла. В момент загрузки angr анализирует файл, определяет его архитектуру (x86, ARM и т.д.), формат (ELF, PE), точку входа программы, и отображает бинарный код в виртуальное адресное пространство.
import angr # Загружаем файл в проект project = angr.Project('./sample1')
Следующий ключевой компонент — это состояние (State). В angr состояние (узел в нашем "дереве выполнения"), или SimState представляет собой полный снимок состояния программы в один конкретный момент времени. Это включает в себя все: значения в регистрах, содержимое памяти и даже состояние файловой системы (например, данные, которые были прочитаны из стандартного ввода).
Напомню, что главным отличием SimState от традиционного состояния программы является то, что оно может оперировать символьными переменными. Чтобы начать анализ, нам нужно создать начальное состояние.
Наиболее простой способ создать начальное состояние - это использовать точку входа в программу.
initial_state = project.factory.entry_state()
Если необходимо исследовать конкретную функцию, либо начинать исследование не из entry point, то желательно использовать другой метод:
initial_state = project.factory.call_state(address=0x1189) # Где 0x1189 - адрес функции
Теперь, когда у нас есть начальное состояние, нам нужен способ исследовать, как это состояние будет меняться при выполнении программы. Для этого используется Simulation Manager. Он берет начальное состояние (или несколько состояний) и начинает пошагово выполнять программу. Когда angr встречает условный переход (например, if-else), Simulation Manager "разветвляет" текущее состояние на два новых: одно для ветви if, другое для else, добавляя соответствующие ограничения к каждому.
Он управляет всеми активными путями выполнения, отслеживая их в специальных "хранилищах" (stashes):
- active - состояния, которые готовы к дальнейшему исследованию.
- deadended - состояния, которые не могут дальше выполняться по различным причинам (закончился код, ошибка и т.д.)
- found - состояния, которые достигли искомого адреса.
- avoided - состояния, которые достигли адреса, которого мы хотим избежать (если понимаем, что исполнение пошло не в ту сторону).
- и другие, для более сложных сценариев.
# Создаем Simulation Manager с начальным состоянием simgr = project.factory.simulation_manager(initial_state)
Этих объектов, в целом, достаточно для того, чтобы запустить анализируемую программу, но не хватает важнейшего компонента символьного исполнения - символьных переменных.
3.3 Claripy
Для работы с символьными переменными в angr используется модуль claripy, который объединяет “под капотом” несколько технологий, в том числе и Z3 SMT-solver.
# Импортируем модуль import claripy # Объявление символьных переменных a = claripy.BVV(3, 32) # Символьная константа 3, размером 32 бита b = claripy.BVS('var_b', 32) # Симв. переменная var_b, размером 32 бита s = claripy.Solver() # Главный объект - SMT-решатель s.add(b > a) # Добавляем логическое условие в решатель print(s.eval(b, 1)[0]) # Находим значение переменной
Вы могли заметить небольшую, но фундаментальную разницу между переменными a и b. Переменная a является объектом BVV (Bit-Vector Value), а переменная b - BVS (Bit-Vector Symbolic Variable).
- BVV - константа, представляет собой известное значение определенного размера.
- BVS - символьная переменная.
Они критически необходимы для SMT-решателя: BVS - как искомое значение, BVV - как часть условий.
Так как у нас уже есть весь список логических ограничений (рисунок 2), определяющих поток к искомой ветке кода, а именно:
((balance > 0) And (age >= 18)) And (balance / age >= 1000)
Мы можем решить это самостоятельно с помощью claripy:
# Объявляем решатель s = claripy.Solver() # Объявляем переменные balance = claripy.BVS("balance", 31) age = claripy.BVS("age", 31) # Добавляем условия s.add(balance > 0) s.add(age >= 18) s.add(balance/age >= 1000) # Находим результат print(f"balance: {s.eval(balance,1)[0]}") print(f"age: {s.eval(age,1)[0]}")
Каждый раз при запуске этого скрипта мы будем получать различные значения, удовлетворяющие условиям. Обратите внимание, что размер переменной 31 бит, хотя integer - 32 бита, почему так? Это связано с тем, что integer является знаковым типом, и что самый старший бит обозначает знак: 0 - положительное число, 1 - отрицательное. А само значение занимает младшие 31 бит.
1. balance: 1149100004 age: 25 2. balance: 1878988608 age: 112 3. balance: 999157188 age: 132115
Все эти значения будут соответствовать ограничениям и приводить поток выполнения к уязвимому коду. Мы также можем найти минимальное и максимальное значение искомых переменных, с помощью методов min() и max() соответственно.
min: balance: 18000 age: 18 max: balance: 2147483647 age: 2147483
3.4 Финальный этап
Теперь мы можем приступить непосредственно к разработке скрипта для анализа программы из нашего примера.
import angr import claripy # Необходим для объявления символьных переменных # Создаем проект project = angr.Project("./sample1")
Перед созданием начального состояния нам необходимо объявить символьные переменные, обозначающие введенные данные. Так как в нашу программу все данные вводятся через стандартный ввод (stdin) мы создадим одну символьную переменную для всего ввода.
# Объявляем символьный stdin symbolic_stdin = claripy.BVS("stdin", 10 * 8) # размер 10 байт # Создаем начальное состояние в точке входа, передавая наши символьные данные в качестве stdin initial_state = project.factory.entry_state(stdin=symbolic_stdin) # Создаем Simulation Manager simgr = project.factory.simulation_manager(initial_state)
Для поиска пути к определенному адресу в Simulation Manager предусмотрен метод explore(), которому в качестве аргумента “find” необходимо указать искомый адрес.
Для наглядности ниже представлен исходный код анализируемой программы.
#include <stdio.h> int main(){ char name[10]; int balance = 0; int age = 0; scanf("%d", &balance); scanf("%d", &age); if ((balance <= 0) || (age < 18)){ return 1; } else if ((balance / age) < 1000) { printf("You're poor\n"); return 1; } printf("Nice! Save your data!\n"); scanf("%s", name); return 0; }
Как уже было сказано ранее, уязвимость переполнения буфера возникает из-за записи строки в буфер без проверки размера, но для того, чтобы ее реализовать, необходимо попасть в ту часть кода, где происходит запись в этот буфер. Ниже представлен граф анализируемой функции в ida pro (рисунок 3). В случае с символьным анализом нас не интересует весь код программы, нам нужно только найти уязвимый блок и определить его адрес (рисунок 4):
В нашем случае искомый адрес - 0x1224, однако нужно помнить, что это адрес относительно начала файла, при загрузке в память он будет загружен по какому-то базовому адресу, этот адрес можно получить “на лету”, и соответственно просто прибавить к искомому адресу.
# Определяем базовый адрес
base_addr = project.loader.main_object.mapped_base
# Вычисляем адрес уязвимого блока
find_addr = 0x1224 + base_addr
# Запускаем поиск
simgr.explore(find=find_addr)
Angr самостоятельно остановится как только найдет первый путь, удовлетворяющий условиям, либо полностью выполнятся все пути. Если необходимый путь нашелся, то это символьное состояние помещается в “хранилище” found.
if simgr.found: # Получаем первый найденный путь/состояние. found_state = simgr.found[0]
А теперь передаем в smt-решатель символьную переменную и просим найти конкретное решение для символьного stdin, которое будет удовлетворять всем ограничениям, собранным на этом пути.
# Находим значение символьного stdin. cast_to=bytes преобразует результат в байтовую строку. solution_stdin = found_state.solver.eval(symbolic_stdin, cast_to=bytes)
Итоговый скрипт:
import angr import claripy # Необходим для объявления символьных переменных # Создание проекта project = angr.Project("./sample1") # Объявляем символьный stdin symbolic_stdin = claripy.BVS("stdin", 10 * 8) # размер 10 байт # Создаем начальное состояние в точке входа, передавая наши символьные данные в качестве stdin initial_state = project.factory.entry_state(stdin=symbolic_stdin) # Создаем Simulation Manager simgr = project.factory.simulation_manager(initial_state) # Определяем базовый адрес base_addr = project.loader.main_object.mapped_base # Вычисляем адрес уязвимого блока find_addr = 0x1224 + base_addr # Запускаем поиск simgr.explore(find=find_addr) if simgr.found: # Получаем первый найденный путь/состояние. found_state = simgr.found[0] # Находим значение символьного stdin. cast_to=bytes преобразует результат в байтовую строку. solution_stdin = found_state.solver.eval(symbolic_stdin, cast_to=bytes) print(solution_stdin)
В результате выполнения скрипта мы получили ответ “8392084+20”. Символ “+” в данном случае ничего не меняет. программой будут считаны последовательно 2 числа: 8392084 и 20, что соответствует условиям и ведет нас в уязвимую часть кода.
4. Заключение
В этой статье мы прошли путь от теоретических основ символьного исполнения до его практического применения с помощью фреймворка angr. Мы увидели, как этот подход позволяет автоматически находить входные данные, которые ведут программу по определенному, нужному нам пути выполнения, тем самым эффективно преодолевая ключевые ограничения традиционного статического и динамического анализа.
Рассмотренный пример - это лишь отправная точка. Техника символьного исполнения незаменима при автоматическом создании эксплойтов (AEG), реверс-инжиниринге проприетарных протоколов и верификации корректности программ.
Безусловно, символьное исполнение имеет свои ограничения. Основной проблемой является "взрыв состояний" (state explosion). Кроме того, точное моделирование взаимодействия с внешним миром (системой, сетью) остается сложной задачей.
Несмотря на эти трудности, символьное исполнение остается одним из самых передовых и эффективных инструментов в арсенале исследователя безопасности и реверс-инженера. Освоение angr дает возможность автоматизации сложных задач анализа, которые ранее требовали многих часов ручной работы.
