На CSAW CTF 2015 задача «wyvern» из категории Reversing 500 содержала бинарь с десятками вложенных проверок ввода - ручной реверс в Ghidra занял бы часы на восстановление логики всех ветвлений. Скрипт на шести строках решил задачу за 15 минут, автоматически сгенерировав входные данные, удовлетворяющие каждому условию. Это из официальных примеров angr, не фантазия. Разница между «знаю, что такое символьное исполнение» и «умею выбрать angr, Triton или Manticore под конкретную задачу» - это разница между 4 часами на CTF-таск и 10 минутами. Ниже - практическое сравнение трёх фреймворков с decision tree, кодом и честным разбором того, где каждый из них ломается.
Как работает символьное исполнение и зачем реверсеру SMT-солвер Z3
Ghidra показывает функцию с десятком вложенныхif-условий. Два пути: восстанавливать логику руками или скормить бинарь символьному движку. Движок заменяет конкретные входные данные символическими переменными - абстрактными значениями, которые могут принимать что угодно из допустимого диапазона. На каждом ветвлении (if, switch, граница цикла) создаются два состояния: для ветки true и для false. К каждому привязывается набор ограничений (constraints) - условий, которым должны удовлетворять символические переменные, чтобы исполнение пошло по этому пути.В целевой точке - допустим, при вызове
puts("Access granted") - движок передаёт накопленные constraints SMT-солверу Z3. Солвер решает систему уравнений и возвращает конкретные значения для подачи на вход программы. Никакого перебора - формулируется математическая задача: «найди такой x, чтобы x > 5 && x * 3 == 42 && x % 7 == 0». Это основа автоматического поиска уязвимостей в бинарном коде: если целевой точкой назначить вызов strcpy с контролируемым буфером, солвер найдёт ввод, приводящий к buffer overflow.Где constraint solving упирается в стену
Первая проблема - path explosion. Каждое ветвление удваивает количество состояний. Цикл на 1000 итераций с условием внутри - теоретически 2^1000 путей. Движок зависает, не добравшись до целевого адреса. Стратегии борьбы: ограничение глубины анализа, concretization (замена части символических переменных конкретными значениями), state merging (слияние состояний на сходящихся путях) и Veritesting - техника в angr для автоматического объединения путей. Помогает, но не спасает от всего.Вторая проблема - сложные constraints. Криптографические функции, хеш-операции, побитовые манипуляции порождают ограничения, которые Z3 не решает за приемлемое время. Если проверка ввода включает SHA-256 - символьное исполнение бесполезно. В задаче Whitehat CTF 2015 (Crypto 400) angr использовался не для полного решения, а для сужения пространства ключей: символьный анализ отсёк невозможные варианты, остальные перебирались brute force. Типичный паттерн - angr как фильтр, а не как серебряная пуля.
angr, Manticore и Triton: сравнение символьных движков
Все три фреймворка решают одну задачу - автоматическое исследование путей исполнения бинаря. Но архитектура, сценарии применения и текущий статус проектов различаются радикально. Выбор инструмента определяется не фичелистом, а ответом на один вопрос: «что за задача передо мной прямо сейчас?»angr: автоматический анализ бинарных файлов
angr (версия 9.2.208, активно поддерживается группой из UC Santa Barbara, коммиты еженедельно) - наиболее зрелый фреймворк символьного выполнения. Поддерживает x86/x64, ARM, MIPS, PPC. Работает в чисто символьном и concolic режиме через интеграцию с Unicorn Engine для конкретного исполнения.По официальной документации angr, фреймворк закрывает три категории задач:
Reversing: восстановление входных данных для crackme и keygen. CSAW CTF «wyvern» (Reversing 500) - 15 минут runtime. FlareOn 2015 Challenge 5 - 2 минуты 10 секунд. ASIS CTF Finals 2015 «license» - 3.6 секунды. DEFCON Quals 2017 - целая категория Crackme2000 решалась автоматически скриптами Shellphish.
Vulnerability Discovery: поиск путей к опасным вызовам. Пример
strcpy_find - обнаружение buffer overflow менее чем за 2 секунды. CGC crash identification - анализ бинарей из DARPA Cyber Grand Challenge.Exploitation: автоматическая генерация эксплойтов (AEG). Insomnihack Simple AEG, SECCON 2016 ropsynth - автоматическое построение ROP-цепочек.
Когда тянуться за angr: CTF-категории rev и pwn, исследование проприетарных бинарей на пентесте, автоматизация рутинного реверса. Документация богатая, десятки готовых примеров, сообщество живое - порог входа ниже, чем у альтернатив.
Manticore: symbolic execution для бинарей и EVM
Manticore от Trail of Bits - символьный движок для нативных бинарей (x86/x64, ARM) и смарт-контрактов Ethereum (EVM). По данным блога Trail of Bits, Manticore использовался как основа Cyber Reasoning System в рамках DARPA Cyber Grand Challenge. В анализе смарт-контрактов фреймворк помог обнаружить CVE-2020-5232 (CVSS 8.7 HIGH, CWE-285 - Improper Authorization) в Ethereum Name Service: уязвимость позволяла бывшему владельцу ENS-домена установить trapdoor и вернуть контроль без согласия нового владельца.Manticore поддерживает taint analysis и бинарную инструментацию. Trail of Bits также выпустила Maat - кросс-архитектурный фреймворк символьного исполнения на базе Ghidra IR (p-code), позиционируемый как более производительная альтернатива.
Статус проекта: последний крупный релиз - Manticore 0.3.3 (добавлена поддержка символьного исполнения WebAssembly). Активность разработки фактически остановилась - новых релизов нет, issues обрабатываются минимально. Команда Trail of Bits переключилась на Echidna для property-based fuzzing смарт-контрактов и Medusa для аудита. Начинать новый проект бинарного анализа на Manticore - рискованно, и я бы не советовал. Для EVM-аудита наработки ещё ценны, но учитывайте отсутствие поддержки.
Triton: динамический анализ и деобфускация
Triton (Jonathan Salwan, активный репозиторий) - фреймворк Dynamic Symbolic Execution (DSE). В отличие от angr, Triton привязан к конкретному исполнению: бинарь запускается с реальными данными, а Triton строит символьные выражения поверх наблюдаемого trace.Архитектурное преимущество - работа с обфусцированным кодом. VMProtect, Themida, кастомные пакеры порождают слишком много путей для чисто символьного анализа: виртуализированные инструкции создают тысячи ветвлений, не относящихся к логике программы. Triton видит уже распакованные инструкции из конкретного trace и строит символьную модель только для наблюдаемого кода - path explosion в контексте обфускации перестаёт быть проблемой. Это решает задачу деобфускации бинарей, защищённых техникой Obfuscated Files or Information (T1027 по MITRE ATT&CK), и соответствует аналитической задаче Deobfuscate/Decode Files or Information (T1140).
Порог входа выше, чем у angr: C++ core с Python-биндингами, документация скуднее, готовых CTF-примеров меньше. Зато если задача - препарировать VMProtect'нутый бинарь, Triton вне конкуренции.
| Критерий | angr | Manticore | Triton |
|---|---|---|---|
| Статус проекта (2025) | Активен, еженедельные коммиты | Разработка остановлена | Активен |
| Режим исполнения | Символьный + concolic | Символьный + concolic | DSE (concolic) |
| Архитектуры | x86, x64, ARM, MIPS, PPC | x86, x64, ARM, EVM | x86, x64, ARM |
| CTF rev/pwn | Основной use case | Да, но без поддержки | Частично |
| Поиск уязвимостей | Да (AEG, crash detection) | Да | Не нативно |
| Деобфускация | Частично | Нет | Основной use case |
| Смарт-контракты EVM | Нет | Да | Нет |
| Порог входа | Средний | Средний | Высокий |
Практика: решаем CTF-задачу с angr
Требования к окружению
- ОС: Linux (Ubuntu 20.04+), macOS. Windows - через WSL2
- RAM: минимум 4 ГБ свободных; для сложных бинарей - 8–16 ГБ
- Python: 3.10+ (angr 9.2.x требует 3.10+)
- Установка:
pip install angr(Z3 solver ставится автоматически) - Режим: локальный, интернет не требуется после установки
- Дополнительно: Ghidra или
objdumpдля определения целевых адресов
Python:
import angr
proj = angr.Project('./fauxware', auto_load_libs=False)
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x400844, avoid=0x40073A)
if simgr.found:
found_state = simgr.found[0]
print(found_state.posix.dumps(0)) # вот он, наш парольauto_load_libs=False - критично для производительности: без этого флага angr символьно исполняет libc, что бессмысленно и на порядок медленнее (на практике разница между 10 секунд и «убил процесс через полчаса»). Адреса find и avoid определяются через Ghidra или objdump -d ./fauxware: find - адрес инструкции после успешной проверки пароля, avoid - ветка отказа.Для более сложных задач подход масштабируется. Задача TUMCTF 2016 «zwiebel» содержала self-unpacking код - angr с Unicorn Engine исполнял распаковку конкретно, а символьный анализ включался после. Runtime - 2 часа 31 минута с PyPy и Unicorn. Без Unicorn - неприемлемо долго, символьное исполнение unpacking-логики порождает миллионы состояний.
Задача 0ctf 2016 «trace» демонстрирует ещё один подход - guided symbolic tracing. Вместо полного символьного исполнения angr направляется по известному trace (файл с адресами инструкций), символьно обрабатывая только данные. Runtime - 1 минута 50 секунд на CPython, 1 минута 12 секунд на PyPy. Здесь angr не «исследует» пути - он идёт по единственному известному пути и решает constraints на данных. Тонкое, но принципиальное различие.
Автоматический поиск уязвимостей в бинарном коде
Переход от CTF к реальному vulnerability discovery - замена целевого адреса. Вместо точки «Access granted» целью становится вызов опасной функции с контролируемым аргументом.Ограничения символьного исполнения
Path explosion и сложные constraints
CTF-задачи компактны: десятки-сотни ветвлений. Реальный бинарь (nginx, OpenSSL, firmware контроллера) - миллионы путей. angr предлагает стратегии: DFS и BFS для управления порядком обхода, Veritesting для автоматического слияния состояний. Но анализ бинаря крупнее нескольких мегабайт в чисто символьном режиме - задача на часы или дни. Иногда - на «никогда».Практический подход: не анализировать весь бинарь. Определите интересующую функцию в Ghidra, ограничьте scope. angr позволяет подменять вызовы через SimProcedures - хуки на функции: замените
malloc упрощённой моделью, printf - заглушкой, и символьный движок не будет тратить ресурсы на библиотечный код. В примере Whitehat CTF 2015 авторы скрипта вручную подставили function summaries для статически слинкованных функций - без этого angr не справился бы.Z3 не инвертирует AES или SHA-256. Увидели хеш-проверку в декомпиляторе - это стоп-сигнал для чистого символьного подхода. Варианты: concretize хеш-значение, обойти проверку через хук, использовать комбинацию с brute force. Третий вариант - чаще всего самый честный.
Обфусцированный и самомодифицирующийся код
Бинари с runtime-распаковкой (UPX, кастомные пакеры) создают проблему: код, который будет исполняться, не существует на диске в открытом виде. angr обрабатывает это через Unicorn Engine - участки с распаковкой исполняются конкретно, символьный анализ включается после. Для тяжёлой обфускации (VMProtect, Themida) angr теряет эффективность: количество виртуализированных инструкций делает символьный анализ непрактичным.Triton здесь имеет архитектурное преимущество: DSE работает поверх конкретного trace, где весь код уже распакован и де-виртуализирован. Задача - «понять, что делает обфусцированный бинарь»? Triton. «Найти ввод для конкретного пути в необфусцированном бинаре»? angr.
Контекст применимости
Символьное исполнение - инструмент офлайн-анализа: вы работаете с копией бинаря на своей машине. EDR, SIEM, сетевые защиты нерелевантны. Но anti-reversing защиты внутри бинаря влияют напрямую: обфускация Control Flow Graph, opaque predicates, MBA-обфускация (Mixed Boolean-Arithmetic) экспоненциально усложняют constraint solving.Где применимо: внутренний пентест - анализ проприетарных бинарей заказчика (firmware IoT-устройств, desktop-клиенты, ICS-софт); CTF - категории rev и pwn; vulnerability research - поиск 0-day в open-source и closed-source ПО. Для внешнего пентеста веб-приложений символьное исполнение неприменимо - там работают Burp, sqlmap, nuclei. Для мобильных приложений angr поддерживает ARM, но практичнее Frida или r2.
Concolic execution: гибрид конкретного и символьного анализа
Чисто символьное исполнение пытается исследовать все пути и тонет в path explosion. Concolic (CONCrete + symbOLIC) execution - компромисс: программа запускается с конкретными входными данными, символьные альтернативы создаются только на ключевых ветвлениях.В angr concolic режим активируется через Unicorn Engine:
Python:
state = proj.factory.entry_state(
add_options=angr.options.unicorn # нативное исполнение где можно
)Triton работает в concolic режиме по умолчанию - это его архитектурная основа. Бинарь запускается, Triton записывает trace, а затем позволяет «спросить»: какой ввод нужен, чтобы пойти по альтернативной ветке? Техника path predicate negation - инвертирование одного из условий пути для генерации нового тестового ввода. Это фундамент concolic fuzzing, где символьный анализ генерирует вводы для покрытия новых путей, а fuzzer обеспечивает скорость и масштаб.
Выбор между чистым символьным и concolic определяется задачей. Компактный CTF без криптографии - чистый символьный режим angr. Реальный бинарь с библиотеками - concolic через angr+Unicorn. Тяжёлая обфускация - Triton с DSE.
Какой инструмент выбрать: decision tree
| Ситуация | Инструмент | Обоснование |
|---|---|---|
| CTF rev/pwn, линейная проверка | angr | Десятки CTF-примеров в документации |
| Деобфускация VMProtect/Themida | Triton | DSE поверх trace обходит виртуализацию |
| Self-unpacking binary | angr + Unicorn | Concolic: распаковка конкретно, анализ символьно |
| AEG (генерация эксплойтов) | angr | Готовые примеры AEG, SimProcedures |
| Аудит Solidity-контрактов (EVM) | Manticore (legacy) | Единственный SE-фреймворк с EVM |
| Большой бинарь (>5 МБ) | angr + SimProcedures | Хуки для масштабирования, Veritesting |
| Directed fuzzing + символика | Triton | Path predicate negation для генерации corpus |
За несколько лет применения символьных движков на CTF и в бинарном анализе на проектах у меня сложился неудобный вывод: большинство тех, кто «знает angr», умеют скопировать шаблонный скрипт с
explore(find=..., avoid=...) и ждать результата. Когда angr зависает - а на реальном бинаре это случается чаще, чем нет - начинается бессистемное добавление avoid-адресов и перезапуск.Навык, который реально ценен - за 30 секунд оценить, поддаётся ли бинарь символьному анализу: есть ли криптография на критическом пути, сколько ветвлений до целевой точки, нужны ли хуки на библиотечные вызовы. Этот навык не приходит из туториалов - только из десятков «сломанных» запусков, когда потратил час на настройку скрипта и получил timeout.
Вторая правда, которую не принято озвучивать: для большинства задач практического vulnerability research направленный fuzzing (AFL++, LibFuzzer) даёт лучший ROI, чем символьное исполнение. Fuzzer за час находит crash, который символьный движок будет искать сутки. Но когда fuzzer упирается в сложное условие (magic bytes, checksum-проверка) - один concolic-запуск с angr генерирует ввод, который fuzzer сам не нашёл бы за неделю.
Будущее - в гибридных пайплайнах, где fuzzing и symbolic execution дополняют друг друга. Кто строит такие пайплайны сейчас - получает преимущество, которое через пару лет станет индустриальным стандартом. Если идёте к OSCP и нужна подготовка по бинарной части - на WAPT проходят аналогичные цепочки с лабами и ментором.
