Сергей Попов
Администратор
- 30.12.2015
- 6 280
- 6 992
- Специализация
- OSINT
- Веб-безопасность
- Статус верификации
- ✓ Verified
В 2013 году Bangert et al. показали на USENIX WOOT штуку, от которой у меня до сих пор мурашки: Тьюринг-полную вычислительную систему, построенную исключительно на механизме обработки page fault в x86. Ни одна инструкция оригинальной программы не исполнялась - вся «логика» порождалась взаимодействием аппаратного обработчика исключений с таблицами страниц. Двумя годами ранее Oakley и Bratus (WOOT'11) собрали рабочий троян из DWARF debugging-метаданных, а Shapiro et al. (WOOT'13) нашли скрытый вычислительный потенциал в метаданных ELF-формата. Суть одна: достаточно сложная система обработки данных содержит «компьютер внутри компьютера», работающий за пределами спецификации. Обнаружить его стандартным статическим анализом - нельзя. Ниже - разбор конкретного pipeline автоматического обнаружения weird machines через формальные методы, symbolic execution и fuzzing.
Weird machine эксплуатация: зачем искать непреднамеренные вычисления
Weird machine - вычислительный артефакт, который появляется при расхождении между задуманной моделью программы и её реальной реализацией. Программа-спецификация моделирует конечный автомат с ограниченным набором допустимых состояний и переходов. Но конкретная реализация на CPU способна переходить в состояния, не предусмотренные разработчиком, - и делает это под воздействием крафтованных входных данных. Thomas Dullien (работа ~2017, опубликована в IEEE Transactions on Emerging Topics in Computing, 2020) сформулировал это чётко: разрыв между абстрактной и конкретной машиной - корневая причина эксплуатируемости. Атакующий «программирует» weird machine, заставляя целевую систему выполнять произвольный код.По MITRE ATT&CK weird machines в ряде сценариев попадают под Exploitation for Client Execution (T1203, Execution) - когда эксплуатация идёт через клиентское ПО (браузер, PDF-reader). Но для серверных и kernel-level weird machines (page fault, memory deduplication) T1203 - не точный маппинг; тут релевантнее общая тактика Execution. В сложных сценариях weird machine может реализовать Reflective Code Loading (T1620, Stealth) - загрузку кода через непредусмотренный механизм - или обеспечить Obfuscated Files or Information (T1027, Stealth), когда код, исполняемый weird machine, полностью невидим для дизассемблеров.
Эволюция exploit-mitigation сделала weird machines критически ценными для атакующих. Trail of Bits приводит хронологию: в 1995 году Windows NT позволяла выполнять данные как код (все read → execute). В 2003 - DEP/NX в Windows XP SP2, в 2006 - ASLR в Vista, в 2016 - Control Flow Guard в Windows 8.1/10. Каждый уровень защиты сужает «контракт выполнения» - количество валидных непрямых переходов уменьшается. Но чем жёстче контракт, тем выше ценность обнаруженной weird machine: она обходит все слои одновременно, потому что работает вне модели, контролируемой защитными механизмами. По сути, защиты закрывают двери, а weird machine - это окно, о существовании которого архитектор не знал.
Для обороняющейся стороны обнаружение weird machines означает: (а) возможность доказать неэксплуатируемость уязвимости при отсутствии подходящих weird machines, (б) целенаправленное «затягивание контрактов» для устранения вычислительных путей, (в) приоритизацию патчинга по реальной достижимости weird-состояний, а не по абстрактному CVSS-скору.
Формальная верификация программ и безопасность: контракты и SAT/SMT решатели
Анализ непреднамеренной вычислительной модели через контракты
Trail of Bits предлагает описывать weird machines через тройки Хоара (Hoare triples): {P} C {Q}, где P - предусловие, C - код, Q - постусловие. Weird machine возникает при «рыхлом контракте» (loose contract): реальные предусловия исполнения функции шире задуманных разработчиком.Классический пример из их анализа - функция
ListItem::TrySetItem. На уровне исходного кода предусловия требуют два валидных указателя на сконструированные объекты ListItem. На уровне машинного кода предусловия совсем другие: this - указатель на любую область памяти размером от 8 байт, item - любой второй параметр произвольного типа. Атакующий, перезаписавший указатель m_next, использует функцию для чтения или записи памяти по произвольному адресу - функция становится гаджетом weird machine. Постусловия тоже рыхлые: функция безусловно модифицирует или возвращает память, независимо от состояния программы.Добавление
dynamic_cast и runtime guards - один из способов затянуть контракт. Для автоматического обнаружения рыхлых контрактов нужны инструменты, перечисляющие множество достижимых состояний.Работает если: доступен исходный код или качественная декомпиляция (IDA Pro / Ghidra); контракты формально выразимы (типизированный язык, assertions); целевая функция изолирована.
Не работает если: бинарник stripped и обфусцирован; кодовая база слишком велика для ручной спецификации контрактов (>100K строк); weird machine возникает из межкомпонентного взаимодействия (hardware + OS + application).
SAT/SMT решатели для доказательства достижимости weird-состояний
Z3, CVC4 и другие SMT-решатели - ядро любого symbolic execution engine, но их можно применять и напрямую: доказать, что конкретное weird-состояние достижимо при определённых входных данных. Согласно обзору arxiv 2508.06643, constraint solver «действует как мозг операции»: path conditions подаются на вход солверу, и если допустимый путь существует, солвер генерирует конкретные входы.
Python:
from z3 import Int, Solver, sat
# Достижимость weird-состояния: overflow до return address
buf_size, offset, ret = Int('buf'), Int('off'), Int('ret')
s = Solver()
s.add(offset == buf_size + 264) # overflow достигает return address
s.add(ret >= 0x400000, ret <= 0x401000) # адрес в пределах .text segment
s.add(buf_size > 0, buf_size <= 4096) # реалистичный размер буфера
if s.check() == sat:
print(f"Weird-состояние достижимо: {s.model()}")Кстати, Stephen Dolan доказал, что даже одна инструкция MOV на x86 Тьюринг-полна (2013). Крайний случай, демонстрирующий теоретическую экспрессивность ISA. Но это свойство архитектуры набора команд, а не weird machine в обсуждаемом смысле - тут нет расхождения между спецификацией и реализацией, MOV делает ровно то, что задокументировано.
Symbolic execution для анализа уязвимостей: от теории к обнаружению weird machines
Поиск скрытых вычислений в бинарном коде: angr и KLEE
Symbolic execution подставляет вместо конкретных входов символические переменные и систематически прослеживает все возможные пути выполнения, накапливая path conditions - логические выражения, описывающие ограничения на вход для каждого пути. Это позволяет перечислять состояния, недостижимые при обычном тестировании. Именно то, что нужно для обнаружения weird machines.KLEE работает на уровне LLVM bitcode: исходный код компилируется через
clang -emit-llvm, после чего KLEE исследует пути и генерирует тест-кейсы для обнаруженных ошибок. Ограничения: нужен исходный код, конкретная версия clang, высокие требования к ресурсам.angr работает на уровне бинарника (ELF, PE, Mach-O) и не требует исходного кода. Для анализа weird machines это принципиально: angr оперирует тем же представлением, которое видит CPU, а weird machines по определению существуют на уровне машинного кода, не исходного текста.
Python:
import angr # ищем путь до weird-состояния в бинарнике
proj = angr.Project('./target', auto_load_libs=False)
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x401337, avoid=[0x401000])
if simgr.found:
inp = simgr.found[0].posix.dumps(0) # stdin, вызывающий weird path
print(f"Trigger input: {len(inp)} bytes")Работает если: бинарник небольшого размера (до 10 МБ для полного анализа); ограниченный набор системных вызовов; отсутствие тяжёлого I/O.
Не работает если: целевой бинарник содержит JIT-компиляцию (JVM, V8); интенсивно использует многопоточность; содержит anti-analysis техники - Debugger Evasion (T1622) или Virtualization/Sandbox Evasion (T1497) - symbolic execution engine может быть обнаружен и обойдён.
Главная проблема - path explosion: каждое условное ветвление удваивает число путей. Два символических условия дают 4 пути, три - 8, рост экспоненциальный. На практике бинарник с десятком вложенных
if превращается в миллионы путей за минуты. Техники митигации: loop unrolling limits, state merging (объединение похожих состояний), concretization символических переменных. Помогает, но не спасает полностью.Concolic execution и уязвимости: Driller как гибридный подход
Driller реализует concolic execution - комбинацию конкретного и символического выполнения. Стратегия: coverage-guided фаззер (AFL) работает основным двигателем, генерируя входы с высокой скоростью. Когда фаззер «застревает» (coverage перестаёт расти), Driller переключается на selective concolic execution - анализирует только пути, найденные фаззером интересными, и генерирует входы для условий (magic bytes, сложные проверки), которые фаззер не может удовлетворить мутациями.Для обнаружения weird machines это критично: weird-состояния часто скрыты за цепочкой проверок, непреодолимых для чистого фаззинга, но разрешаемых symbolic execution за секунды. Driller избегает path explosion, анализируя не всё пространство путей, а подмножество, отмеченное фаззером.
Driller - исследовательский инструмент. По данным Code Intelligence, он «потребляет значительные вычислительные ресурсы» и «требует специализированных знаний для настройки». На практике это означает: настройка под конкретный бинарник может занять больше времени, чем сам анализ. Промышленное применение пока ограничено лабораториями и CTF-подготовкой.
Fuzzing для поиска weird machines: от crash до weird-состояния
Coverage-guided fuzzing и обнаружение аномальных состояний
AFL++ и libFuzzer - современные coverage-guided фаззеры, использующие инструментацию кода для отслеживания покрытия. В отличие от random fuzzing, они мутируют входы для максимизации покрытия новых путей - что напрямую коррелирует с обнаружением неожиданных состояний программы.Группа Abhik Roychoudhury (National University of Singapore) формализовала coverage-based greybox fuzzing как марковскую цепь: вход - состояние, мутация - переход, вероятность перехода определяется покрытием. Математический аппарат позволяет оценивать вероятность достижения weird-состояний и направлять мутации в сторону менее исследованных областей. Та же группа разработала stateful greybox fuzzing для протоколов (Usenix Security 2022) и directed greybox fuzzing (CCS 2017) для целенаправленного достижения конкретных участков кода.
Работает если: доступен harness или бинарник поддаётся инструментации (QEMU mode для binary fuzzing, source instrumentation для libFuzzer); достаточно вычислительных ресурсов для многодневного запуска; crash выступает индикатором weird-состояния.
Не работает если: weird machine не приводит к crash, а лишь к утечке данных или изменению логики - coverage-guided фаззер этого не обнаружит без специального oracle. Также проблема с target, требующим сложного stateful setup (embedded firmware без эмулятора, протоколы с handshake).
Отдельно стоит упомянуть KLEESpectre - адаптацию KLEE для обнаружения утечек через спекулятивное выполнение (Spectre), описанную группой Roychoudhury. Спекулятивный кеш процессора выступает weird machine, а KLEESpectre находит входы, провоцирующие наблюдаемые side-channel. Это связано с работой ExSpectre (NDSS 2019), где авторы продемонстрировали скрытие malware в спекулятивном выполнении - по их собственному признанию, результаты расширяют исследования weird machines. Аналогичный подход применим к memory deduplication: Bosman et al. (IEEE S&P 2016) показали, что встроенная дедупликация памяти Windows 8.1-10 в сочетании с RowHammer формирует мощную weird machine. Тут CPU буквально становится соучастником атаки.
Gadget chains, ROP анализ и weird machine construction эксплойтов
ROP (Return-Oriented Programming) - каноничный пример weird machine construction: атакующий собирает из гаджетов (коротких последовательностей инструкций, заканчивающихсяret) полноценную Тьюринг-полную программу. Каждый гаджет - легитимный фрагмент кода, но их комбинация - weird machine, не предусмотренная разработчиком. Bosman и Bos (IEEE S&P 2014) показали аналогичный подход через фальшивые signal frames в Unix: обработчик сигналов «возвращается» из сигналов, которые ядро никогда не доставляло. Красиво и жутковато одновременно.Автоматизированный поиск ROP-гаджетов (
ROPgadget, ropper, встроенные модули angr) перечисляет компоненты потенциальной weird machine. Но обнаружение гаджетов - первый шаг. Критический вопрос: компонуются ли они в Тьюринг-полную систему? Trail of Bits предлагает подход через «Turing thunks» - идентификацию программных слайсов с контролируемыми побочными эффектами, которые сами Тьюринг-полны. Для определения Тьюринг-полноты применяются:- Data flow analysis - построение графа зависимостей данных между гаджетами
- Shape analysis - реконструкция heap-объектов, их layout и взаимодействий для определения ограничений на входы
- Symbolic/concolic execution - валидация: собирается ли цепочка гаджетов в цельную weird machine при реальных ограничениях памяти
Автоматизированный поиск уязвимостей бинарного кода: сравнение инструментов
| Инструмент | Тип анализа | Целевой формат | Сила в контексте weird machines | Когда использовать | Когда НЕ использовать |
|---|---|---|---|---|---|
| Z3 / CVC4 | SMT-solving | Constraint-формулы | Доказательство достижимости конкретного состояния | Верификация кандидатов, отдельные функции | Полный анализ бинарника без предварительной декомпозиции |
| KLEE | Symbolic execution (source) | LLVM bitcode | Покрытие путей в исходном коде, генерация тестов | Проекты с исходным кодом, C/C++ | Binary-only, JIT-код, масштабные проекты |
| angr | Symbolic execution (binary) | ELF, PE, Mach-O | Перечисление нестандартных путей на уровне бинарника | CTF, firmware, бинарный анализ | Приложения >10 MB, тяжёлый I/O |
| AFL++ | Coverage-guided fuzzing | Любой бинарник | Массовое обнаружение crash-состояний, масштабируемость | Поиск аномальных входов, разведка | Определение Тьюринг-полноты, silent weird machines |
| Driller | Concolic (fuzzing + SE) | Бинарники | Преодоление magic bytes, глубокий анализ | Когда чистый fuzzing стагнирует | Без предварительного fuzzing-этапа |
| CBMC | Model checking | C/C++ source | Формальная верификация bounded model | Критичные модули с ограниченной глубиной | Большие кодовые базы, бинарный анализ |
Ни один инструмент не решает задачу обнаружения weird machines целиком. Z3 доказывает достижимость, но не находит кандидатов. AFL++ обнаруживает аномалии, но не доказывает Тьюринг-полноту. angr перечисляет пути, но упирается в path explosion. Рабочий подход - композиция: fuzzing для масштабного поиска кандидатов, symbolic execution для верификации, SMT для доказательства свойств. По отдельности - каждый инструмент слеп, вместе - видят картину.
Практический pipeline обнаружения weird machines
Шаг 5: Устранение и документирование. Для подтверждённых weird machines определите минимальное изменение контракта (runtime check, CFI-аннотация,
dynamic_cast), устраняющее вычислительное свойство без нарушения легитимной функциональности.Когда pipeline НЕ работает: если weird machine возникает из межкомпонентного взаимодействия (hardware + OS kernel + userland), полный pipeline неприменим одним инструментом. Page-fault weird machine (Bangert et al.) требует моделирования MMU; Spectre-класс weird machines (ExSpectre, NDSS 2019) требует моделирования спекулятивного выполнения. Для таких случаев нужны специализированные инструменты вроде KLEESpectre или кастомные angr-хуки, моделирующие поведение железа. Это уже не автоматизация - это исследовательская работа.
Индустрия расходует основные ресурсы на латание конкретных CVE. Каждый патч - точечное решение, не затрагивающее weird machine surface бинарника. Можно закрыть конкретный buffer overflow, а та же кодовая база продолжит содержать десятки Тьюринг-полных фрагментов из легитимных паттернов: обход связных списков, парсинг файлов, обработка сигналов. По данным Dullien (2017), доказательство неэксплуатируемости (provable unexploitability) возможно только при подтверждении отсутствия подходящих weird machines в окрестности уязвимости - а этого не делает практически никто.
Одна из причин: инструменты разрозненны, pipeline не стандартизирован, формальная верификация не готова к production-масштабу. Мой прогноз: в горизонте двух-трёх лет offensive-инструментарий получит автоматизированные модули обнаружения weird machines. Trail of Bits уже описывает архитектуру такого решения, академические группы из Dartmouth (Bratus et al.) и NUS (Roychoudhury et al.) двигаются в том же направлении.
Защитная сторона отстаёт. Разрыв между скоростью обнаружения weird machines атакующими и способностью защитников их устранять будет расти - и это главный аргумент вкладываться в формальные методы сейчас, а не когда automated weird machine scanner станет стандартным компонентом exploit-фреймворков. LangSec-подход, направленный на устранение целых классов input-related багов и ассоциированных weird machines, выглядит перспективнее точечного патчинга - но требует пересмотра того, как мы проектируем парсеры и форматы данных с самого начала. Попробуйте прогнать свой парсер через шаги 1-3 pipeline выше - результаты могут неприятно удивить.
