Тестирование Smart Contract Security с Avverifier
16 июля 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 Этическое рассмотрение
Связанная работа
Заключение, доступность и ссылки
5 Оценка
5.1 Экспериментальная настройка и исследовательские вопросы
Базовые линииПолем Насколько нам известно, никакая существующая структура анализа смарт -контрактов не поддерживает обнаружение уязвимости проверки адреса. Однако, чтобы проиллюстрировать эффективность Avverifier, мы расширили Mythril [70] (Commit: F5E2784), Ethainter [14], Jackal [39] (Commit: 3993e5c) и EthBMC [33] (Commit: E887f33), четыре популярных анализатора контрактов, как базовые. В частности, Mythril является хорошо известным и широко принятым символическим исполнителем, который специально предназначен для обнаружения уязвимостей в интеллектуальных контрактах Ethereum. Таким образом, мы сначала интегрируем те же правила размножения в Mythril. Затем мы используем ту же трехэтапную логику обнаружения, что и в §4.5. Следовательно, Mythril модифицируется как статический символический анализатор на основе символического исполнения. Что касается Ethainter, это является авторитетным, широко используемым и масштабируемым анализатором уровня кода исходного кода, основанным на DataLog. После получения исходного кода Ethainter сначала выполнит полный анализ и извлечет текущий поток управления и зависимости потока данных в контракте. Поэтому мы также реализуем трехступенчатый детектор в Datalog для фильтрации тех, которые соответствуют правилам, упомянутым в §4.5 из всех генерируемых состояний. Что касается шакала, он декомпилирует ethereum Smart Contracts 'Bytecode на промежуточное представление для построения графиков потока управления. Мы интегрируем те же правила размножения в шакале и используем трехэтапную логику обнаружения, изложенную в §4.5. Эта модификация расширяет возможность шакала сосредоточиться на выявлении уязвимостей проверки адреса в интеллектуальных контрактах. Наконец, ETHBMC использует ограниченную проверку модели и символическое исполнение. Мы также вручную интегрируем в нее трехэтапную логику обнаружения, чтобы обострить его сосредоточенность на выявлении уязвимостей проверки адреса. Поскольку детекторы во всех этих инструментах следуют одному и тому же набору принципов на семантическом уровне, это может отражать различие между ними с точки зрения эффективности и эффективности.
Реализация Avverifier.Avverifier написан на Python и состоит из 1,3 тыс. Строков кода. Как показано на рис. 1, он состоит из трех основных модулей:
Кодовый график.Он отвечает за разборку данного байт -кода в OPCODES и построение CFG в соответствии со статической функцией вызовов вызовов, как мы упоминали в §4.3. Кроме того, в селекторе функций график выбирает подозрительные функции в соответствии с эвристикой в §4.3 и получает соответствующий базовый блок записи.
EVM Simulator.Корпус симулятора представляет собой двухслойную вложенную петлю, внешняя итерация итерации всех подозрительных функций, собранных у графы, и внутренние итерации все выпиты. Согласно правилам распространения, определяемых в §4.4, состояние, состоящее из структур данных, таких как стек EVM, память, хранилище и информация о том, что информация обновляется. Когда столкнулся Jumpi, Avverifier использует подход на эвристическом выборе пути. Окончательное состояние каждого пути будет отправлено детектору. После того, как функция помечена как уязвимая, внутренняя петля будет сломаться до следующей функции, чтобы повысить эффективность анализа.
Детектор уязвимости.Используя состояние, данное симулятором, все штаты проходят трехфазную проверку, как представлено в §4.5. Если какое -либо состояние может пройти все три этапа, то есть уязвимые, оно будет немедленно возвращено в симулятор.
Экспериментальная установка.Эксперименты проводятся на 48 базовом сервере, оснащенном двумя процессорами Intel Xeon 6248R, сопровождаемым 256 ГБ оперативной памяти, в то время как его ограничение по времени для каждого контракта составляет 10 минут.
Мы отвечаем на следующие вопросы исследования (RQS):
RQ1Является ли Avverifier эффективным и эффективным для определения уязвимости проверки адреса?
RQ2Сколько умных контрактов уязвимо в дикой природе и каковы их характеристики?
RQ3Можно ли развернуть Avverifier в качестве системы обнаружения в реальном времени?
Чтобы ответить на RQ1, мы запускаем Avverifier и четыре базовых инструмента на хорошо построенных эталонных и реальных контрактах в дикой природе, от блока Genesis до того, что с высотой 17 421 000, созданных в 6 июня 2023 года, в общей сложности около 59 миллионов контрактов. Среди этих контрактов мы рассматриваем те, которые участвуют по крайней мере в одной части транзакции как заслуживающие анализа. Таким образом, 5,158 101 интеллектуальных контрактов остаются в качестве кандидатов. Чтобы ответить на RQ2, мы характеризуем уязвимые контракты с разных точек зрения, например, количество транзакций и токенов. Чтобы ответить на RQ3, мы развернули Avverifier как на Ethereum, так и на BSC [20], известной EVM-подобной платформе блокчейна с рыночной капитализацией в 37,7 млрд долларов [24]. Мы всесторонне его удобство использования и масштабируемость детектора в реальном времени.
Авторы:
(1) Tianle Sun, Университет науки и техники Хуажонга;
(2) Ningyu HE, Peking University;
(3) Цзян Сяо, Университет науки и техники Хуажонга;
(4) Yinliang Yue, лаборатория Zhongguancun;
(5) Сяпу Луо, Гонконгский политехнический университет;
(6) Хаою Ван, Университет науки и техники Хуажонга.
Эта статья есть
Оригинал