Avverifier опередиет Mythril и EthBMC в обнаружении уязвимости с интеллектуальным контрактом
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.2 RQ1: эффективность и эффективность
5.2.1 Оценка результатов по эталону
Создание эталона.After comprehensively collecting technical reports from well-known blockchain security companies [12], we have identified six confirmed vulnerable contracts, as P. As all their source code files are available, we manually patch each of them to compose P. Moreover, we manually sample four benign contracts from widely-adopted DeFi, i.e., Aave [2], Compound [25], ParaSpace Lending [69], and a yield protocol [32], to form the set Н. Причина выбора этих четырех контрактов - два раза. С одной стороны, все они требуют ввода внешнего адреса контракта. В частности, AAVE и SORUST в основном используют токены как обеспечение
Заимствуйте еще один ценный токен, в то время как Paraspace использует NFT в качестве залога. Протокол доходности использует входной адрес внешнего контракта для генерации доходности обеспечения. Поскольку все эти четыре контракта выполняют необходимую проверку по переданному адресу, они соответствуют как P1, так и P2. С другой стороны, после выполнения определенных операций на цепочке ценные токены в их контрактах передаются вызывающему, что создает потенциальные риски как P3. Точно так же мы намеренно удаляем их проверку по адресам, чтобы сделать их уязвимыми, обозначая этот набор как N., следовательно, мы получили 20 случаев основной истины. Таблица 1 иллюстрирует результаты, где выделенные строки относятся к неправильно обнаруженным результатам.
Среднее время.В среднем он требуется Avverifier около 7,34 с, в то время как Mythril значительно отстает, что занимает в среднем около 28,3 с. Ethainter и Jackal сидят между ними, с временами в среднем от 10,86 до 19,19. Avverifier составляет приблизительно 3,86x, 1,48x и 2,61x быстрее, чем Mythril, Ethainter и Jackal, соответственно. При рассмотрении случаев тайм -аута Avverifier и EthBMC записали ноль, в то время как Mythril, Ethainter и Jackal сталкивались с тайм -аутом в 8, 4 и 6 экземплярах соответственно. Кроме того, мы можем легко заметить, что ETHBMC работает хорошо с точки зрения времени выполнения. Однако после комплексного аудита кода и анализа в журналах вывода мы считаем, что это связано с тем, что его ограниченный подход к проверке модели приоритет эффективности над тщательностью. Другими словами, пути могут быть упущены, что может поставить под угрозу точность в сложных сценариях, таких как уязвимость проверки адреса, ориентированная на эту работу.
Точность и отзыв.Точность и отзыв являются двумя критическими показателями для оценки эффективности анализатора, где Avverifier превосходит другие инструменты. В частности, Avverifier достигает 100% точности и 100% отзывов на эталон. В случае Mythril и Ethbmc основной проблемой являются ложные негативы. Для случаев, которые могут быть завершены в течение срока, Mythril и EthBMC имеют 50% и 100% ложную негативную ставку соответственно. Мы предполагаем, что основная причина неидажных результатов ETHBMC-два раза. С одной стороны, ограниченная стратегия проверки модели ETHBMC по своей природе фокусируется на определенном диапазоне состояний и путей в рамках контрактов, что потенциально пропустила сложности, связанные с проверкой адреса из -за его ограниченного объема. С другой стороны, ETHBMC требует заранее определенного начального состояния для анализа. Тем не менее, это состояние, скорее всего, не оптимально для обнаружения уязвимости проверки адреса, что может повлиять на его производительность. Ethainter также обладает худшей эффективностью по сравнению с Avverifier с точки зрения отзыва, с ложной негативной скоростью около 12,5%. Мы считаем, что наиболее важным фактором является принятие Gigahorse [36], инструментального положения для бинарного анализа. Согласно своей реализации, одним из его ограничений является его неспособность идеально обрабатывать динамическую память, влияя на производительность Ethainter в идентификации функций, которые широко используют динамическую память. Следовательно, это ограничение приводит к ложным негативам.
Корневые причины.Учитывая различия в метрик при проведении анализа на эталонном эталоне среди этих пяти инструментов, мы предполагаем, что существует четыре причины их различий в результате эффективности на эталон. Во -первых, Avverifier полностью использует характеристики, обобщенные из P1. В графике он фильтрует подозрительные функции как кандидаты, что значительно уменьшает количество возможных состояний, затруднение влияет на эти инструменты. Во -вторых, как подробно описано в §4.4.4, стратегия исследования, используемая симулятором, специально предназначена для уязвимости проверки адреса. Эта стратегия отдает приоритет путям, которые могут привести к уязвимости. В -третьих, при обращении с динамической памятью остальные четыре инструмента изо всех сил пытаются точно проанализировать уязвимые функции, которые широко используют сложные динамические распределения памяти. Напротив, Avverifier использует симулятор EVM, позволяя ему точно отслеживать параметры адреса без четкого моделирования поведения динамической памяти, тем самым повышая его способность идентифицировать такие функции. Наконец, Avverifier принимает простой подход моделирования, а не статическое символическое исполнение. Этот выбор способствует его эффективности. Предыдущие исследования, такие как Klee [19], предполагают, что Backend Smt Solvers может быть значительным сопротивлением производительности.
5.2.2 Результаты реальных контрактов
Чтобы дополнительно проиллюстрировать эффективность Avverifier на контрактах на реальность, мы выполняем анализ всех собранных контрактов, всего 5,158 101. Следовательно, 812 из них отмечены как уязвимые Avverifier. Чтобы оценить эффективность Avverifier, мы снова используем Mythril, Ethainter, Jackal и EthBMC в качестве базовых показателей. Однако, потому что ООН
читаемость байт -кода, для более эффективного сравнения мы попытались получить их исходный код от Etherscan. Наконец, мы собрали 369 штук исходного кода. Окончательные результаты сканирования для всех этих пяти инструментов на 369 контрактах с открытым исходным кодом показаны в таблице 2.
Среднее время.Как мы видим, для всех 369 случаев Avverifier достигает второй лучшей производительности с точки зрения среднего времени анализа. Более того, в 10-минутном пределе нет случаев тайм-аутов. Ethainter находится на одном месте, с 8,74 и 6 тайм -аутами. Эффективность Mythril сильно отстает, в среднем составляет 33,69 с за случай и страдает 42 тайм-аута, превышающие 10-минутный порог, самый высокий среди сравниваемых инструментов. Шакал в среднем около 29,96 с 60 тайм -аутами внутри. Наконец, хотя EthBMC имеет приличное среднее время 5,43 с, он страдает 164 случая тайм -аута, что значительно влияет на его эффективность. Сравнивая Таблицу 2 и Таблицу 1, мы можем заметить, что производительность между этими инструментами примерно согласованна, за исключением того, что у ETHBMC больше случаев тайм -аута в реальных случаях. Мы предполагаем, что это связано с тем, что он должен попробовать разные начальные состояния, когда текущие не могут изучить пути эксплуатации, что приводит к огромной проблеме эффективности.
Точность и отзыв.После вручную перепроверьте все эти контракты, количество ложных срабатываний и ложных отрицательных также показано в таблице 2. Мы можем легко заметить, что существует 21 ложный срабатывание, генерируемые Avverifier, что приводит к точке 94,3%. Основная причина этого заключается в том, что существуют нетрадиционные методы проверки по адресам. За исключением трех механизмов, которые мы суммировали в §2.2, некоторые из них делегируют проверку адреса другим контрактам, что не является широко принятым методом проверки. Более того, некоторые контракты выполняют проверку с помощью цифровых подписей [17] или Merkle Proofs [50]. В настоящее время из -за проблем с эффективностью Avverifier не интегрирует такие шаблоны. Более того, поскольку межконтракт-анализ всегда является огромным препятствием для анализа смарт-контрактов [58], должен быть сделан компромисс. Напротив, все остальные четыре базовых показателя страдают от серьезных ложных негативных проблем. Хотя Mythril использует аналогичный подход фильтрации путей к Avverifier, его отзыв составляет всего 5,1%, поскольку символическое исполнение не может эффективно найти возможные пути для использования уязвимых контрактов. Ethainter и Jackal, оба из которых используют структуру Gigahorse, достигают показателей отзыва только 43,0% и 59,7% соответственно. Как мы упоминали в §5.2.1, Gigahorse изо всех сил пытается точно построить полные CFG при обращении с некоторыми контрактами, что связано с его менее оптимизированной обработкой динамической памяти. Отзыв ETHBMC составляет всего 1,1%, причина которого в основном обусловлена принятыми начальными государствами, как мы указали выше. Мы провели тематическое исследование, чтобы проиллюстрировать, как дело неверно обозначено как ложное отрицательное с помощью этих четырех инструментов, пожалуйста, обратитесь к нашему репо с открытым исходным кодом всвязьПолем
Авторы:
(1) Tianle Sun, Университет науки и техники Хуажонга;
(2) Ningyu HE, Peking University;
(3) Цзян Сяо, Университет науки и техники Хуажонга;
(4) Yinliang Yue, лаборатория Zhongguancun;
(5) Сяпу Луо, Гонконгский политехнический университет;
(6) Хаою Ван, Университет науки и техники Хуажонга.
Эта статья есть
Оригинал