Автоматизация реверс-инжиниринга с помощью Angr

Источник: https://github.com/AnaktaCTF/CTF/blob/main — Reverse/AutomatingReverseEngineeringwithAngr.md

В мире соревнований Capture The Flag методика ручного анализа исполняемых файлов нередко становится узким местом: исследователю приходится вручную читать дизассемблированный код, сопоставлять его с ожидаемым поведением и, зачастую, часами перебирать гипотезы и тестировать их на практике. Но в последние годы важным подспорьем в этой задаче стал фреймворк Angr — гибкая платформа для статического и динамического анализа исполняемых файлов, позволяющая автоматизировать многие рутинные этапы и сосредоточиться на самом интересном: стратегии обхода защит и извлечении скрытых данных. В этой статье мы подробно разберём, как шаг за шагом построить надёжный, расширяемый и настраиваемый скрипт для автоматизации реверс-инжиниринга заданий CTF-соревнований, опираясь на возможности Angr и SMT-решателя Z3.

Глубокое знакомство с Angr и символическим выполнением

Перед тем как приступить к практике, важно понять, почему Angr так мощно помогает в CTF: дело в символическом выполнении. В классическом отладчике вы задаёте конкретные входные данные и видите, как программа ведёт себя в одном единственном сценарии. Символическое выполнение же позволяет представить неизвестные данные (ввод пользователя, сетевой трафик, содержимое файла) в виде символических переменных. Программа интерпретируется условно-компилятором (IR), и при каждом условном переходе ветвления сохраняются ограничения, наложенные на эти переменные.

Главная заслуга Angr — объединить несколько ключевых компонентов в едином Python-интерфейсе:

Capstone и PyVEX для преобразования «сырых» машинных команд в промежуточное представление;
Claripy для работы с символическими выражениями и построения SMT-формул;
SimulationManager для управления множеством «симуляционных» путей и фильтрации тех, что нас не интересуют;
интеграция со внешними SMT-решателями (чаще всего Z3), позволяющая проверять выполнимость формул и извлекать конкретные модели (значения символов).

Такой подход особенно эффективен против CTF-задач, где присутствуют сложные проверки целостности, хеш-функции и ветвления, рассчитанные на запутывание анализатора. По сути, Angr даёт вам возможность «спросить» у программы: «Что ты выведешь, если я введу такие-то данные?» и получить ответ без численных попыток грубой силы.

Подготовка окружения и установка зависимостей

Начнём с настройки чистого рабочего пространства на Linux или macOS. Рекомендуется изолировать проект в виртуальном окружении, чтобы не смешивать версии библиотек между различными задачами.

# 1. Создаём виртуальное окружение
python3 -m venv venv

# 2. Активируем его
source venv/bin/activate

# 3. Обновляем pip и setuptools
pip install --upgrade pip setuptools

# 4. Устанавливаем Angr с полным набором зависимостей
pip install angr[full]

# 5. (Опционально) Если Z3 не подтянулся, ставим отдельно
pip install z3-solver

После установки важно убедиться в совместимости версий. Достаточно выполнить pip list и убедиться, что Capstone, PyVEX, Cle и другие компоненты стоят актуальных версий.

Если вы планируете работать на Windows, можно воспользоваться WSL (Windows Subsystem for Linux) или Docker-образом, где уже настроено окружение Angr.

Загрузка исполняемого файла и первичная разведка

После настройки окружения переходим к разбору двоичного файла. Пусть он называется challenge. Главная точка входа — класс angr.Project, который автоматически определяет архитектуру, формат PE/ELF/Mach-O и собирает базовые метаданные.

import angr

# Инициализируем проект без загрузки внешних библиотек
project = angr.Project("./challenge", auto_load_libs=False)

print(f"Формат: {project.loader.main_object.binary}")
print(f"Архитектура: {project.arch.name}")

Отменяя auto_load_libs, мы ускоряем анализ и исключаем фоновые вызовы из системных библиотек — в CTF они обычно не влияют на логику флага.

После загрузки полезно получить общее представление о секциях, импортированных функциях и экспортируемых символах:

for section in project.loader.main_object.sections:
    print(section.name, hex(section.min_addr), section.memsize)

print("Импортированные функции:")
for sym in project.loader.main_object.imports:
    print(f"{sym.name} @ {hex(sym.rebased_addr)}")

Это даёт первичную карту: где находятся код, данные, какие вызовы WinAPI или libc присутствуют.

Построение графа потока управления и анализ функций

Следующий шаг — создание Control-Flow Graph (CFG). CFGFast быстро строит приближённый граф, позволяющий увидеть, какие функции вызывает программа и как они взаимосвязаны.

cfg = project.analyses.CFGFast(normalize=True)

print("Найденные функции:")
for addr, func in cfg.kb.functions.items():
    print(f"{hex(addr)} — {func.name}, размер {func.size} байт")

Параметр normalize=True объединяет эквивалентные базовые блоки, делая граф чище. Если задачи требуют более точного представления — например, для сложных хитрых проверок — можно использовать CFGEmulated, который имитирует выполнение и учитывает динамически разрешённые переходы, хотя он работает медленнее.

После получения списка функций обычно интересными оказываются:

функции обработки пользовательского ввода. Их можно угадать по имени или по месту в вызовах read, fgets, scanf;
функции проверки — те, что сравнивают хеши или содержимое буфера;
точка/точки, где программа выводит результат (флаг), чаще всего через puts или printf.

Символические переменные: моделирование пользовательского ввода

Чтобы проверить поведение, создадим символический ввод. Например, если задача ожидает ввод из stdin длиной 64 байта:

import claripy

# Создаём битовую векторную строку длиной 64 байта => 512 бит
input_symbol = claripy.BVS("user_input", 8 * 64)

state = project.factory.full_init_state(
    args=["./challenge"],
    stdin=angr.SimFileStream(name="stdin", content=input_symbol, has_end=False)
)

Параметр has_end=False указывает, что ввод может быть произвольной длины до 64 байт, а не строго ровно 64.

Альтернативный вариант — передавать аргументы командной строки:

state = project.factory.full_init_state(
    args=["./challenge", claripy.BVS("flag_arg", 8 * 32)]
)

Выбор способа зависит от спецификации программы.

Управление путями исполнения с SimulationManager

Задача — найти состояние, в котором программа «придёт» к выводу флага, и исключить все нежелательные «тупики» (функции выхода, обработки ошибок). Для этого используется SimulationManager:

simgr = project.factory.simulation_manager(state)

# Укажите адрес точки, где сигнализируется успех
find_addr  = 0x400800  
# Адрес, ведущий в ошибку или exit
avoid_addr = 0x400900  

simgr.explore(find=find_addr, avoid=avoid_addr)

Под капотом explore разделяет все пути на три группы:

found — успешно достигшие find_addr,
avoid — попавшие в avoid_addr,
active — ещё продолжающиеся.

Если found содержит несколько состояний, можно отфильтровать их по объёму символических данных, по времени обхода или по самому содержимому вывода.

Извлечение флага из состояния программы

Когда simgr.found непуст, берём первый подходящий SimState и извлекаем данные:

found_state = simgr.found[0]

# Вывод через stdout (дескриптор 1)
output_bytes = found_state.posix.dumps(1)
print("Вывод программы:", output_bytes.decode(errors="ignore"))

# Если флаг хранится в памяти по адресу в регистре RAX
flag_addr = found_state.solver.eval(found_state.regs.rax)
raw_flag  = found_state.memory.load(flag_addr, 32)
flag      = found_state.solver.eval(raw_flag, cast_to=bytes)
print("Флаг:", flag)

Метод solver.eval возвращает конкретную модель, удовлетворяющую всем ранее накопленным ограничениям.

Сложности автоматизации и способы их обхода

Организаторы CTF-соревнований порой специально усложняют задачу, внедряя механизмы, которые «ломают» простые скрипты:

Дедупликация путей (state merging). По умолчанию Angr пытается не допустить «взрыв» состояний с одинаковым PC и схожими constraints. Если нужно проанализировать повторяющиеся ветки, можно отключить merge/сделать его менее агрессивным:
```
simgr = project.factory.simulation_manager(state, save_unsat=True)
```
Неограниченные циклы. Если цикл либо while(true), либо с условием, зависящим от вводимых данных, страдает бесконечным разворачиванием, можно вручную задать ограничение по числу шагов:
```
simgr.run(until=lambda sm: sm.step_count > 10000)
```
или задать unroll_limit в анализе CFG, чтобы CFGFast не пытался слишком далеко разворачивать петли.
Таймаут-триггеры. Вставлены счётчики времени или итераций — если анализ идёт слишком медленно, программа намеренно «зависает» или уходит в неожиданные ветви. Решение: уменьшить точность (ограничить глубину state.history), либо вручную включить эвристику по бюджету выполнения:
```
project.factory.simgr(state, bailout=lambda sm: sm.step_count > 50000)
```
Хеш-проверки и anti-debug. Программы могут вызывать специальные функции, вычислять контрольные суммы и бросать исключение при несовпадении. Часто быстрее заменить вызовы таких функций на заранее известные значения:
```
# Псевдокод: переназначаем адрес функции проверки
project.hook(0x401000, lambda state: state.regs.rax = claripy.BVV(1, 32))
```
Или перехватить call и сразу возвращать «правильный» результат.

Ручная формулировка SMT-задач с Z3

Иногда встроенных эвристик Angr оказывается недостаточно, особенно когда логика проверки слишком замысловата. В таких случаях удобно «вытащить» из программы чистую логику хеширования/шифрования, портировать в Python, а затем задать задачу напрямую:

from z3 import Solver, BitVec, sat

# Создаём символические 32-битные переменные
x = BitVec('x', 32)
y = BitVec('y', 32)
target = 0xdeadbeef

s = Solver()
# hash_logic — ваша Python-функция, реализующая ту же логику, что и в challenge
s.add(hash_logic(x, y) == target)

if s.check() == sat:
    model = s.model()
    print("Найдено решение:", model[x].as_long(), model[y].as_long())
else:
    print("Нет решений")

В таком сценарии вы полностью контролируете границы перебора: пока Z3 справляется, вы получаете точный ответ и не тратите ресурсы на симуляцию всего исполняемого файла.

Сборка полноценного Python-модуля

Когда все этапы отработаны, выгодно оформить анализ в виде самостоятельного скрипта с возможностью параметризации:

#!/usr/bin/env python3
import angr, claripy, argparse, logging

def setup_project(path, load_libs=False):
    return angr.Project(path, auto_load_libs=load_libs)

def find_flag_binary(args):
    proj = setup_project(args.binary, load_libs=False)
    symbolic_input = claripy.BVS('inp', 8 * args.stdin_size)
    state = proj.factory.full_init_state(
        args=[args.binary],
        stdin=angr.SimFileStream(name='stdin', content=symbolic_input, has_end=False)
    )
    simgr = proj.factory.simulation_manager(state)
    simgr.explore(find=args.find_addr, avoid=args.avoid_addr)
    if simgr.found:
        fs = simgr.found[0]
        output = fs.posix.dumps(1)
        print(output.decode(errors='ignore'))
    else:
        logging.error("Флаг не найден.")

def parse_cli():
    parser = argparse.ArgumentParser(
        description="Автоматизация реверс-инжиниринга CTF-задач с Angr"
    )
    parser.add_argument("binary", help="Путь к анализируемому файлу")
    parser.add_argument("--stdin-size", type=int, default=32,
                        help="Максимальная длина вводимых данных")
    parser.add_argument("--find-addr", type=lambda x: int(x, 16),
                        required=True, help="Адрес точки успеха (hex)")
    parser.add_argument("--avoid-addr", type=lambda x: int(x, 16),
                        required=True, help="Адрес точки неуспеха (hex)")
    parser.add_argument("--verbose", action="store_true",
                        help="Включить подробное логгирование")
    return parser.parse_args()

def main():
    args = parse_cli()
    if args.verbose:
        logging.basicConfig(level=logging.DEBUG)
    find_flag_binary(args)

if __name__ == "__main__":
    main()

Такой шаблон позволяет быстро подключать новые задачи, перенастраивать адреса точек поиска/избегания и масштабировать автоматизацию.

Отладка и оптимизация производительности

Даже при грамотной организации скрипт может «буксовать» на слишком большом дереве состояний. Несколько практических приёмов:

лимит символических байтов. Не делайте весь ввод символическим, если известно, что только первые N байт участвуют в проверке;
ограничение глубины пути. Параметры max_depth и step_count в SimulationManager позволяют прервать слишком длинные ветки;
Merge и Prune. Объединяйте близкие состояния и удаляйте заведомо неперспективные через переходы simgr.prune();
чекпоинты. Сохраняйте промежуточные SimState с помощью pickle и загружайте при падении скрипта, чтобы не начинать анализ заново;
параллелизм. Если ресурс позволяет, запускайте по несколько экземпляров с разными стратегиями обхода: один — BFS, другой — DFS, третий — с random exploration.

Реальный пример: анализ ELF-исполняемого

Рассмотрим упрощённый пример, где challenge проверяет пароль так:

int main() {
    char buf[16];
    scanf("%15s", buf);
    if (hash(buf) == 0x12345678) {
        puts("SUCCESS!");
        puts(buf);
    } else {
        puts("FAIL");
    }
}

CFGFast найдёт функции scanf, hash, puts.
Создаём символические 16 байт, передаём в stdin.
find_addr — адрес инструкции после puts("SUCCESS!").
avoid_addr — адрес puts("FAIL").

Скрипт автоматом отработает и выведет секретный пароль из памяти, без ручного перебора или отладки.

Практические советы по написанию расширяемого кода

Чтобы ваш автоматический анализатор служил долго:

делайте модульную архитектуру: отдельный модуль — загрузка проекта, отдельный — управление путями, отдельный — интеграция с SMT;
используйте профилировщик (например, cProfile), чтобы понять, какие части работы занимают больше всего времени;
пишите тесты на небольших примерах: задачи «Hello World» и маленькие шифровалки, чтобы проверить, что скрипт корректно определяет границы ввода и точки успеха;
документируйте функции и публикуйте примеры использования в README: новым участникам команды будет проще вникнуть.