2025-11-10T03:00:57.254697

Decompiling for Constant-Time Analysis

Arranz-Olmos, Barthe, Blatter et al.
Cryptographic libraries are a main target of timing side-channel attacks. A practical means to protect against these attacks is to adhere to the constant-time (CT) policy. However, it is hard to write constant-time code, and even constant-time code can be turned vulnerable by mainstream compilers. So how can we verify that binary code is constant-time? The obvious answer is to use binary-level CT tools. To do so, a common approach is to use decompilers or lifters as a front-end for CT analysis tools operating on source code or IR. Unfortunately, this approach is problematic with current decompilers. To illustrate this fact, we use the recent Clangover vulnerability and other constructed examples to show that five popular decompilers eliminate CT violations, rendering them not applicable with the approach. In this paper, we develop foundations to asses whether a decompiler is fit for the Decompile-then-Analyze approach. We propose CT transparency, which states that a transformation neither eliminates nor introduces CT violations, and a general method for proving that a program transformation is CT transparent. Then, we build CT-RetDec, a CT analysis tool based on a modified version of the LLVM-based decompiler RetDec. We evaluate CT-RetDec on a benchmark of real-world vulnerabilities in binaries, and show that the modifications had significant impact on CT-RetDec's performance. As a contribution of independent interest, we found that popular tools for binary-level CT analysis rely on decompiler-like transformations before analysis. We show that two such tools employ transformations that are not CT transparent, and, consequently, that they incorrectly accept non-CT programs. While our examples are very specific and do not invalidate the general approach of these tools, we advocate that tool developers counter such potential issues by proving the transparency of such transformations.
academic

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

Основная информация

  • ID статьи: 2501.04183
  • Название: Decompiling for Constant-Time Analysis
  • Авторы: Santiago Arranz-Olmos (MPI-SP), Gilles Barthe (MPI-SP & IMDEA), Lionel Blatter (MPI-SP), Youcef Bouzid (ENS Paris-Saclay), Sören van der Wall (TU Braunschweig), Zhiyuan Zhang (MPI-SP)
  • Категория: cs.PL (Языки программирования)
  • Дата публикации: Январь 2025 (препринт arXiv)
  • Ссылка на статью: https://arxiv.org/abs/2501.04183

Аннотация

Криптографические библиотеки являются основной мишенью атак по времени выполнения. Практический метод защиты от таких атак — соблюдение стратегии постоянного времени (ПВ). Однако написание кода с постоянным временем сложно, и даже исходный код с постоянным временем может быть преобразован основными компиляторами в уязвимый двоичный код. В данной работе исследуется вопрос проверки соответствия двоичного кода требованиям постоянного времени. Распространённый подход заключается в использовании декомпилятора в качестве интерфейса для преобразования двоичного кода в исходный код или промежуточное представление, а затем применении существующих инструментов анализа ПВ. К сожалению, этот метод «декомпиляция-анализ» имеет проблемы. В данной работе на примере уязвимости Clangover и других случаев показано, что пять популярных декомпиляторов устраняют нарушения ПВ, делая результаты анализа ненадёжными.

Исследовательский контекст и мотивация

Проблемный фон

  1. Угроза атак по времени выполнения: Криптографические реализации уязвимы для атак по времени выполнения, когда злоумышленник может вывести секретную информацию, наблюдая время выполнения программы
  2. Стратегия постоянного времени: Стратегия ПВ требует, чтобы время выполнения программы не зависело от секретных входных данных, включая отсутствие доступа к памяти, зависящего от секретов, и условных переходов
  3. Уязвимости компилятора: Оптимизации основных компиляторов могут преобразовать безопасный исходный код в двоичный код с нарушениями ПВ

Основная проблема

Существующий метод «декомпиляция-анализ» имеет фундаментальный недостаток: декомпиляторы могут устранять нарушения ПВ во время преобразования, что приводит к тому, что инструменты анализа ошибочно считают уязвимый двоичный код безопасным.

Исследовательская мотивация

  1. Практическая необходимость: Требуется анализ ПВ двоичного кода, но существующие инструменты ориентированы в основном на исходный код
  2. Недостатки метода: Текущий подход использования декомпилятора в качестве интерфейса ненадёжен
  3. Теоретический пробел: Отсутствует теоретическая база для оценки пригодности преобразований программ для анализа ПВ

Основные вклады

  1. Выявление и доказательство проблемы: На примере уязвимости Clangover и других случаев показано, что пять основных декомпиляторов устраняют нарушения ПВ, делая результаты анализа ненадёжными
  2. Предложение теории прозрачности ПВ: Формальное определение концепции прозрачности ПВ, то есть преобразования программ, которое ни устраняет, ни вводит нарушения ПВ
  3. Разработка методов доказательства: Предложен универсальный метод на основе симуляции для доказательства прозрачности ПВ преобразований программ
  4. Создание практического инструмента: Разработан инструмент CT-RetDec на основе модифицированного декомпилятора RetDec для надёжного анализа ПВ двоичного кода
  5. Обнаружение дефектов инструментов: Доказано, что преобразования, используемые существующими инструментами анализа ПВ (CT-Verif и BinSec), также не прозрачны и содержат уязвимости безопасности

Подробное описание методов

Определение задачи

Вход: Двоичная программа Выход: Результат анализа ПВ (безопасна/небезопасна) Ограничение: Результат анализа должен точно отражать фактические свойства ПВ двоичной программы

Теоретическая база

Определение прозрачности ПВ

Для преобразования программы ⟦⋅⟧:Ls→Lt\llbracket \cdot \rrbracket : L_s \to L_t определены три свойства:

  1. Рефлексивность (Reflection): Если ⟦P⟧\llbracket P \rrbracket является φ-ПВ, то P является φ-ПВ
  2. Сохранение (Preservation): Если P является φ-ПВ, то ⟦P⟧\llbracket P \rrbracket является φ-ПВ
  3. Прозрачность (Transparency): Одновременное удовлетворение рефлексивности и сохранению

Методы симуляции

Используются два метода: синхронная симуляция и ослабленная симуляция:

Синхронная симуляция: Каждый шаг выходной программы соответствует шагу входной программы

  • Отношение симуляции: s∼ts \sim t
  • Преобразователь наблюдений: T:Os→OtT : O_s \to O_t
  • Ключевое условие: T должен быть инъективным

Ослабленная симуляция: Позволяет входной и выходной программам выполняться с разным числом шагов

  • Функция числа шагов: ns:PC→N>0ns : PC \to \mathbb{N}_{>0}
  • Функция суффикса: sf:PC→Os∗sf : PC \to O_s^*
  • Инъективность PC: Для каждой точки программы преобразователь наблюдений является инъективным

Технические инновации

  1. Концепция инъективности PC: Расширение существующих методов сохранения ПВ путём требования инъективности преобразователя наблюдений в каждой точке программы для обеспечения рефлексивности
  2. Единая база: Анализ множества преобразований программ в рамках единой теоретической базы
  3. Практическая ориентация: Предоставление не только теоретического анализа, но и разработка практически применимых инструментов

Экспериментальная установка

Набор данных

  1. Тестирование декомпиляторов: Использование уязвимости Clangover и построенных минимальных контрпримеров для тестирования 5 декомпиляторов
  2. Набор эталонных тестов: 160 двоичных программ, содержащих 10 известных уязвимостей временных боковых каналов
    • Компиляторы: Clang 10/14/18/21
    • Уровни оптимизации: -O0, -Os
    • Архитектуры: x86-32, x86-64

Метрики оценки

  • Точность: Правильное ли выявление нарушений ПВ
  • Полнота: Отсутствие пропусков реальных уязвимостей
  • Уровень ложных срабатываний: Ошибочное ли обозначение безопасного кода как небезопасного

Методы сравнения

  • Оригинальный RetDec + CT-LLVM
  • CT-RetDec (модифицированная версия)
  • Ручной анализ в качестве эталона

Детали реализации

  • Отключение 10 непрозрачных оптимизационных проходов в RetDec
  • Сохранение 52 проходов, из которых 7 теоретически доказаны как прозрачные
  • Использование CT-LLVM для финального анализа ПВ

Результаты экспериментов

Основные результаты

Тестирование прозрачности декомпиляторов

Все 5 протестированных декомпиляторов устраняют определённые нарушения ПВ:

ДекомпиляторClangoverBranch CoalescingEmpty BranchDead LoadDead Store
Angr✗✗-✗-
BinaryNinja-✗✗✗✗
Ghidra--✗✗-
Hex-Rays-✗✗✗-
RetDec✗✗✗✗✗

Оценка производительности CT-RetDec

На 160 эталонных программах:

  • Точность: 100% (без ложных срабатываний и пропусков)
  • Оригинальный RetDec: Пропускает большинство нарушений ПВ
  • Эффект улучшения: Значительное повышение надёжности анализа ПВ

Анализ преобразований программ

Анализ прозрачности 10 распространённых преобразований программ:

Прозрачные преобразования (7):

  • Замена выражений (свёртывание констант, развёртывание и т.д.)
  • Исключение мёртвых ветвей
  • Исключение мёртвых присваиваний
  • Оптимизация против переполнения
  • Структурный анализ
  • Ротация циклов

Непрозрачные преобразования (3):

  • Слияние ветвей
  • Преобразование if
  • Исключение доступа к памяти

Обнаружение дефектов инструментов

Обнаружены уязвимости безопасности в инструментах CT-Verif и BinSec:

  • CT-Verif: Преобразователь SMACK устраняет мёртвые загрузки, что приводит к принятию программ, не соответствующих ПВ
  • BinSec: Процесс повышения DBA объединяет пустые ветви, устраняя нарушения ПВ

Связанные работы

Анализ боковых каналов

Существующие инструменты анализа ПВ основаны на:

  • Построении произведения программ (CT-Verif)
  • Системах типов (Jasmin)
  • Решателях SMT (Vale)
  • Абстрактной интерпретации (Blazy и др.)
  • Символическом выполнении (BinSec)

Безопасная компиляция

Связанные исследования сосредоточены на том, как компиляторы сохраняют свойства безопасности:

  • Методы симуляции ПВ (Barthe и др.)
  • Метод преобразователя утечек
  • Доказательства сохранения ПВ компиляторами Jasmin и CompCert

Корректность декомпиляции

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

Заключение и обсуждение

Основные выводы

  1. Универсальность проблемы: Основные декомпиляторы повсеместно имеют проблемы с прозрачностью ПВ
  2. Необходимость теории: Требуется формальная теория для оценки и обеспечения прозрачности преобразований программ
  3. Практическая осуществимость: Посредством теоретического руководства можно построить надёжные инструменты анализа ПВ двоичного кода
  4. Дефекты инструментов: Существующие инструменты анализа ПВ сами содержат проблемы с прозрачностью

Ограничения

  1. Охват: Анализ охватывает только базовые стратегии ПВ, не включая расшифровку и детализированные модели утечек
  2. Типы преобразований: Теоретический анализ охватывает только 10 распространённых преобразований, в то время как RetDec содержит 62 прохода
  3. Дефекты реализации: Даже теоретически прозрачные преобразования могут содержать ошибки в реализации

Направления будущих исследований

  1. Расширение теории: Поддержка более сложных свойств безопасности и моделей утечек
  2. Автоматизированная верификация: Разработка инструментов для автоматической проверки прозрачности преобразований
  3. Улучшение компиляторов: Интеграция требований прозрачности в проектирование компиляторов

Глубокая оценка

Преимущества

  1. Важность проблемы: Решение критической проблемы в практическом анализе безопасности
  2. Теоретический вклад: Предложение полной теоретической базы прозрачности ПВ
  3. Достаточная эмпирическая база: Проверка теории на множестве примеров и эталонных тестов
  4. Практическая ценность: Разработка применимых инструментов и обнаружение дефектов существующих инструментов
  5. Формальная строгость: Предоставление механизированных доказательств на Coq

Недостатки

  1. Охват теории: Анализ охватывает только часть типов преобразований программ
  2. Масштаб экспериментов: Хотя эталонные тесты содержат реальные уязвимости, масштаб относительно ограничен
  3. Совершенство инструмента: CT-RetDec всё ещё основан на эмпирическом методе отключения части проходов

Влияние

  1. Академическая ценность: Предоставление новой теоретической базы для анализа безопасности преобразований программ
  2. Практическое значение: Прямое влияние на практику анализа безопасности криптографического программного обеспечения
  3. Влияние инструментов: Обнаруженные дефекты инструментов будут способствовать улучшению соответствующих инструментов

Применимые сценарии

  1. Анализ криптографического ПО: Применимо к сценариям, требующим анализа ПВ двоичных криптографических реализаций
  2. Разработка компиляторов: Предоставление теоретической базы для верификации безопасности оптимизаций компилятора
  3. Разработка инструментов безопасности: Предоставление руководства для разработки надёжных инструментов анализа безопасности двоичного кода

Библиография

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