Обнаружение уязвимостей, байт по байту: архитектура Avverifier
15 июля 2025 г.Таблица ссылок
Аннотация и 1. Введение
Фон
2.1 Ethereum Primer
2.2 Проверка адреса белого списка
2.3 Анализ Taint по интеллектуальным контрактам и 2,4 модели угрозы
Мотивирующий пример и проблемы
3.1 Мотивирующий пример
3.2 Проблемы
3.3 Ограничения существующих инструментов
Дизайн Avverifier и 4.1 Обзор
4.2 обозначения
4.3 Компонент № 1: График кода
4.4 Компонент № 2: симулятор EVM
4.5 Компонент № 3: детектор уязвимости
Оценка
5.1 Экспериментальная настройка и исследовательские вопросы
5.2 RQ1: эффективность и эффективность
5.3 RQ2: характеристики уязвимых контрактов реального мира
5.4 RQ3: обнаружение в реальном времени
Дискуссия
6.1 Угрозы для достоверности и 6.2 ограничения
6.3 Этическое рассмотрение
Связанная работа
Заключение, доступность и ссылки
4 Дизайн Avverifier
В этом разделе выясняется технические тонкости Avverifier, который предназначен для обнаружения уязвимости проверки адреса в интеллектуальных контрактах Ethereum. Сначала мы даем обзор высокого уровня в §4.1 и введение принятых обозначений в §4.2. Затем мы углубимся в три компонента, соответственно, от §4.3 до §4.5.
4.1 Обзор
Рис. 1 иллюстрирует архитектуру и рабочий процесс Avverifier, который состоит из трех основных компонентов, т.е.Кодовый график(обозначается как графер),EVM Simulator(обозначается как симулятор), идетектор уязвимости(обозначается как детектор). В частности, Avverifier принимает только байт -код смарт -контракта Solidity в качестве ввода. Графер анализирует его в график потока управления (CFG), отфильтровывает все подозрительные функции в качестве кандидатов и доставляет их в симулятор. Симулятор поддерживает состояние, состоящее из двух частей. Одна часть - это структуры данных, требуемые EVM, то есть стек, память и хранилище (см. §2.1); Другая часть - собранная информация о том, что Согласно CFG, симулятор обновляет поля в состояниях в соответствии с последовательности OpCode. Он также принимает метод выбора путей на основе эвристики, чтобы сосредоточиться на наиболее ценном пути, то есть те, которые могут привести к уязвимости. После того, как анализ по пути завершен, соответствующее состояние отправляется детектору, чтобы определить, уязвим ли текущий контракт к уязвимости проверки адреса. Каскадная трехфазная стратегия обнаружения в детекторе исключает ложные срабатывания и ложные негативы на основе внутренних характеристик (от P1 до P3).
4.2 обозначения
Чтобы лучше объяснить реализацию Avverifier, мы определяем здесь некоторые обозначения:
• С, набор источников, которые могут контролироваться пользователями;
• Т, набор испорченных переменных;
• Ct, отображение от испорченной переменной на ее источники;
• f, набор подозрительных функций;
• МемВСто, обратитесь к области памяти и хранения в EVM.
• V.ВЕС, иСМ, см. Трехэтапное обнаружение в детекторе соответственно. Каждый из них принимает функциюфони параметрпкак входные данные.
4.3 Компонент № 1: График кода
Вообще говоря, графер отвечает за получение подриса CFG данной функции. Учитывая кусок байт -кода, график сначала извлекает код времени выполнения, состоящий из реализации функций [40]. Затем графер анализирует его в основные блоки и строит CFG в соответствии с их отношениями с прыжками. Тем не менее, некоторые отношения прыжков определяются динамически во время выполнения, а не статически на стадии компиляции. Таким образом, график создает CFG только на статически определенных отношениях с прыжками, учитывая обоснованность. Возьмите на рис. 2 в качестве примера, где BB1 является входом функции Foo, и ее прыжки с BB2 и BB3 могут быть статически определены. Хотя BB3 и BB4 могут прыгать на BB5 во время выполнения, они определяются динамически. Таким образом, хотя графер генерирует два дерева, корни которых являются BB1 и BB5, соответственно, BB5 на самом деле является поддереем BB1 во время выполнения.
Чтобы отфильтровать подозрительные функции, то есть те, которые могут быть уязвимы для уязвимости проверки адреса, графер эвристически сохраняет функции, которые принимают адреса в качестве аргументов (стр.). В частности, каждый параметр адреса подвергается куче и операции с 0xff..ff (длиной 160 бит). Выявляя такую конкретную схему, которая также широко используется в предыдущей работе [7], мы можем извлечь функции, которые соответствуют P1. Эти функции будут добавлены в набор f.
Авторы:
(1) Tianle Sun, Университет науки и техники Хуажонга;
(2) Ningyu HE, Peking University;
(3) Цзян Сяо, Университет науки и техники Хуажонга;
(4) Yinliang Yue, лаборатория Zhongguancun;
(5) Сяпу Луо, Гонконгский политехнический университет;
(6) Хаою Ван, Университет науки и техники Хуажонга.
Эта статья есть
Оригинал