1 запись с тегом "формальная верификация"

Формальная верификация в аудите смарт-контрактов​

Формальная верификация относится к использованию математических и логических методов для доказательства корректности и безопасности смарт-контрактов. На практике это охватывает спектр методологий: от фазз-тестирования на основе свойств и символического выполнения до строгого доказательства теорем и проверки моделей. Цель состоит в том, чтобы гарантировать соответствие контракта его спецификациям и отсутствие в нем эксплуатируемых ошибок при всех возможных входных данных и состояниях. Учитывая высокие ставки (миллиарды долларов заблокированы в DeFi-протоколах), формальные методы становятся все более важными для Ethereum и других блокчейн-платформ.

Традиционные подходы: Ранние формальные методы для Ethereum включали инструменты символического выполнения, такие как Oyente и Mythril, и статические анализаторы, такие как Slither и Securify. Символическое выполнение исследует пути программы с символическими входными данными для обнаружения проблем (например, реентрабельности, переполнения целых чисел), в то время как статический анализ использует сопоставление с образцом на основе правил. Эти инструменты имели успех, но также и ограничения: например, Oyente выдавал много ложных срабатываний даже на простых контрактах, а детекторы Slither, основанные на шаблонах, могли давать несколько ложных срабатываний. Более того, исследование 2023 года показало, что более 80% эксплуатируемых ошибок в контрактах (особенно сложных ошибок «бизнес-логики») были пропущены существующими инструментами, что подчеркивает необходимость более надежных методов верификации.

Перспективы и проблемы полной верификации: Теоретически, формальная верификация может доказать отсутствие ошибок путем исчерпывающей проверки инвариантов для всех состояний. Такие инструменты, как Certora Prover или фреймворк KEVM от Ethereum Foundation, направлены на математическую верификацию смарт-контрактов в соответствии с формальной спецификацией. Например, «автоматический математический аудитор» Certora использует язык спецификаций (CVL) для доказательства или опровержения правил, определенных пользователем. Однако на практике полное доказательство свойств для реальных контрактов часто недостижимо или очень трудоемко. Код может потребовать переписывания в упрощенные формы для верификации, должны быть написаны пользовательские спецификации, циклы и сложная арифметика могут потребовать ручных ограничений или абстракций, а SMT-солверы часто превышают время ожидания при сложной логике. Как отметили инженеры Trail of Bits, «доказательство отсутствия ошибок обычно недостижимо» для нетривиальных кодовых баз, и его достижение часто требует значительного вмешательства пользователя и экспертных знаний. Из-за этого инструменты формальной верификации традиционно использовались редко для критически важных частей кода (например, для верификации инварианта токена или алгоритма консенсуса), а не для целых контрактов от начала до конца.

Фазз-тестирование и тестирование инвариантов Foundry​

В последние годы тестирование на основе свойств стало практической альтернативой полным формальным доказательствам. Foundry, популярный фреймворк для разработки Ethereum, имеет встроенную поддержку фазз-тестирования и тестирования инвариантов — методов, которые значительно улучшают покрытие тестами и могут рассматриваться как облегченная формальная верификация. Фазз-тестирование Foundry автоматически генерирует большое количество входных данных, чтобы попытаться нарушить заданные свойства, а тестирование инвариантов распространяет это на последовательности операций, изменяющих состояние:

• Фазз-тестирование: Вместо написания модульных тестов для конкретных входных данных разработчик указывает свойства или инварианты, которые должны выполняться для любых входных данных. Foundry затем генерирует сотни или тысячи случайных входных данных для тестирования функции и проверяет, что свойство всегда выполняется. Это помогает выявить граничные случаи, которые разработчик мог бы не догадаться протестировать вручную. Например, фазз-тест может утверждать, что возвращаемое значение функции всегда неотрицательно или что определенное постусловие истинно независимо от входных данных. Движок Foundry использует интеллектуальные эвристики — он анализирует сигнатуры функций и вводит граничные значения (0, максимальное uint и т. д.) — для охвата граничных случаев, которые, вероятно, нарушат свойство. Если утверждение не выполняется, Foundry сообщает входной контрпример, который нарушает свойство.

• Тестирование инвариантов: Тестирование инвариантов Foundry (также называемое фаззингом с учетом состояния) идет дальше, выполняя множественные вызовы функций и переходы состояний последовательно. Разработчик пишет инвариантные функции, которые должны оставаться истинными на протяжении всего срока службы контракта (например, общие активы = сумма балансов пользователей). Foundry затем случайным образом генерирует последовательности вызовов (со случайными входными данными) для имитации множества возможных сценариев использования, периодически проверяя, что условия инвариантов остаются истинными. Это может выявить сложные ошибки, которые проявляются только после определенной последовательности операций. По сути, тестирование инвариантов более тщательно исследует пространство состояний контракта, гарантируя, что ни одна последовательность действительных транзакций не может нарушить заявленные свойства.

Почему Foundry важен: Foundry сделал эти передовые методы тестирования доступными. Функции фаззинга и инвариантов встроены в рабочий процесс разработчика — не требуется специальный каркас или внешний инструмент, а тесты пишутся на Solidity наряду с модульными тестами. Благодаря движку на основе Rust, Foundry может быстро выполнять тысячи тестов (параллелизуя их) и предоставлять подробные трассировки сбоев для любого нарушения инварианта. Разработчики сообщают, что фаззер Foundry прост в использовании и очень производителен, требуя лишь незначительной настройки (например, установки количества итераций или добавления предположений для ограничения входных данных). Простой пример из документации Foundry — это фазз-тест для функции divide(a,b), который использует vm.assume(b != 0) для избежания тривиальных недействительных входных данных, а затем утверждает математические постусловия, такие как result * b <= a. Запуская такой тест с тысячами случайных пар (a,b), Foundry может быстро обнаружить граничные случаи (например, границы переполнения), которые было бы трудно найти путем ручного рассуждения.

Сравнения: Подход Foundry основан на предыдущих работах сообщества. Фаззер Echidna от Trail of Bits был более ранним инструментом тестирования на основе свойств для Ethereum. Echidna аналогичным образом генерирует случайные транзакции для поиска нарушений инвариантов, выраженных как функции Solidity, возвращающие булево значение. Он известен своей «интеллектуальной» генерацией входных данных (включая фаззинг, управляемый покрытием) и использовался для поиска многих ошибок. Фактически, исследователи безопасности отмечают, что движок Echidna чрезвычайно эффективен — «Echidna от Trail of Bits — лучший фаззер благодаря интеллектуальному выбору случайных чисел» — хотя интегрированный рабочий процесс Foundry упрощает написание тестов для разработчиков. На практике фазз-тестирование Foundry часто рассматривается как новый «минимальный стандарт» для безопасной разработки Solidity, дополняющий традиционные модульные тесты. Оно не может доказать отсутствие ошибок (поскольку оно рандомизировано и не является исчерпывающим), но значительно повышает уверенность, охватывая широкий спектр входных данных и комбинаций состояний.

За пределами фаззинга: формальные доказательства и передовые инструменты​

Хотя фаззинг и инварианты выявляют многие проблемы, существуют случаи, когда используются более строгие формальные методы. Проверка моделей и доказательство теорем включают спецификацию желаемых свойств в формальной логике и использование автоматизированных доказателей для их проверки на соответствие коду контракта. Certora Prover (недавно открытый исходный код) является выдающимся инструментом в этой категории. Он позволяет разработчикам писать правила на предметно-ориентированном языке (CVL), а затем автоматически проверяет контракт на нарушения этих правил. Certora использовалась для верификации критических инвариантов в таких протоколах, как MakerDAO и Compound; например, она выявила ошибку «DAI debt invariant» в MakerDAO (тонкое несоответствие в учете), которая оставалась незамеченной в течение четырех лет. Примечательно, что движок Certora теперь поддерживает несколько платформ (EVM, VM Solana и eWASM), а открыв его исходный код в 2025 году, он сделал формальную верификацию промышленного уровня свободно доступной на Ethereum, Solana и Stellar. Этот шаг признает, что формальные доказательства не должны быть роскошью только для хорошо финансируемых команд.

Другие формальные инструменты включают подходы верификации во время выполнения (например, семантика KEVM Ethereum или Move Prover для цепочек на основе Move). В частности, Move Prover встроен в язык Move (используемый блокчейнами Aptos и Sui). Он позволяет писать формальные спецификации наряду с кодом и может автоматически доказывать определенные свойства с пользовательским интерфейсом, похожим на линтер или проверку типов. Эта тесная интеграция снижает барьер для разработчиков на этих платформах для использования формальной верификации как части разработки.

Резюме: Современный аудит смарт-контрактов сочетает в себе эти методологии. Фаззинг и тестирование инвариантов (на примере Foundry и Echidna) широко используются благодаря их простоте использования и эффективности в выявлении распространенных ошибок. Символическое выполнение и статические анализаторы по-прежнему служат для быстрого сканирования на предмет известных уязвимостей (с такими инструментами, как Slither, часто интегрированными в CI/CD-пайплайны). Тем временем, инструменты формальной верификации развиваются и распространяются по цепочкам, но они обычно зарезервированы для конкретных критических свойств или используются специализированными аудиторскими фирмами из-за их сложности. На практике многие аудиты сочетают эти подходы: например, использование фаззеров для поиска ошибок во время выполнения, статических инструментов для выявления очевидных ошибок и формальных проверок спецификаций для ключевых инвариантов, таких как «баланс токенов не превышает общее предложение».

Аудит с помощью ИИ с использованием больших языковых моделей​

Появление больших языковых моделей (БММ), таких как GPT-3/4 (ChatGPT) от OpenAI и Codex, привнесло новую парадигму для анализа смарт-контрактов. Эти модели, обученные на огромных объемах кода и естественного языка, могут рассуждать о поведении программ, объяснять код и даже обнаруживать определенные уязвимости путем распознавания образов и знаний «здравого смысла». Вопрос в том: может ли ИИ дополнить или даже автоматизировать аудит смарт-контрактов?

Инструменты анализа уязвимостей на основе БММ​

Появилось несколько исследовательских работ и прототипов инструментов, которые применяют БММ для аудита смарт-контрактов:

• OpenAI Codex / ChatGPT (общие модели): Ранние эксперименты просто заключались в том, чтобы предложить GPT-3 или Codex код контракта и попросить найти потенциальные ошибки. Разработчики обнаружили, что ChatGPT может идентифицировать некоторые известные шаблоны уязвимостей и даже предлагать исправления. Однако ответы были случайными и не всегда исчерпывающими. Недавняя академическая оценка отметила, что наивное использование ChatGPT для обнаружения уязвимостей «не дало значительно лучших результатов по сравнению со случайным предсказанием» на эталонном наборе данных — по сути, если модель не направляется должным образом, она может галлюцинировать несуществующие проблемы или пропускать реальные уязвимости. Это подчеркнуло необходимость тщательно разработанных промптов или тонкой настройки для получения полезных результатов.

• AuditGPT (2024): Это академический инструмент, который использовал ChatGPT (GPT-3.5/4) специально для проверки соответствия стандартам ERC в контрактах Ethereum. Исследователи заметили, что многие контракты токенов ERC20/ERC721 нарушают тонкие правила стандарта (что может привести к проблемам безопасности или совместимости). AuditGPT работает, разбивая аудит на небольшие задачи и разрабатывая специализированные промпты для каждого типа правил. Результат был впечатляющим: в тестах на реальных контрактах AuditGPT «успешно выявил 418 нарушений правил ERC и сообщил только о 18 ложных срабатываниях», демонстрируя высокую точность. Фактически, в статье утверждается, что AuditGPT превзошел профессиональную аудиторскую службу в поиске ошибок соответствия ERC при меньших затратах. Это говорит о том, что для хорошо определенных, узких областей (например, для обеспечения соблюдения списка стандартных правил) БММ с хорошими промптами может быть удивительно эффективной и точной.

• LLM-SmartAudit (2024): Другой исследовательский проект, LLM-SmartAudit, использует более широкий подход, применяя многоагентную систему диалога для аудита кода Solidity. Он настраивает несколько специализированных агентов GPT-3.5/GPT-4 (например, один «Аудитор», сосредоточенный на корректности, один «Атакующий», думающий о том, как эксплуатировать), которые общаются друг с другом для анализа контракта. В своей оценке LLM-SmartAudit смог обнаружить широкий спектр уязвимостей. Примечательно, что в сравнительном тесте с обычными инструментами система на основе GPT-3.5 достигла наивысшей общей полноты (74%), превзойдя все традиционные статические и символические анализаторы, которые они тестировали (следующим лучшим был Mythril с полнотой 54%). Она также смогла найти все 10 типов уязвимостей в их тестовом наборе (в то время как каждый традиционный инструмент испытывал трудности с некоторыми категориями). Более того, переключившись на GPT-4 и сфокусировав анализ (то, что они называют режимом целевого анализа), система смогла обнаружить сложные логические ошибки, которые инструменты, такие как Slither и Mythril, полностью пропустили. Например, на наборе реальных DeFi-контрактов подход на основе БММ нашел сотни логических ошибок, в то время как статические инструменты «не продемонстрировали эффективности в обнаружении» этих проблем. Эти результаты демонстрируют потенциал БММ в выявлении тонких ошибок, которые выходят за рамки сопоставления с образцом традиционных анализаторов.

• Prometheus (PromFuzz) (2023): Гибридный подход заключается в использовании БММ для управления другими методами. Одним из примеров является PromFuzz, который использует «агента-аудитора» на основе GPT для выявления подозрительных областей в коде, затем автоматически генерирует проверки инвариантов и передает их в фаззинг-движок. По сути, БММ выполняет первоначальный анализ (как с доброжелательной, так и с атакующей точки зрения), чтобы сфокусировать фазз-тестирование на вероятных уязвимостях. В оценках этот подход достиг очень высоких показателей обнаружения ошибок — например, более 86% полноты с нулевыми ложными срабатываниями в определенных эталонных наборах — значительно превосходя автономные фаззеры или предыдущие инструменты. Это многообещающее направление: использование ИИ для оркестровки и улучшения классических методов, таких как фаззинг, сочетая сильные стороны обоих.

• Другие инструменты ИИ: Сообщество видело различные другие концепции аудита с помощью ИИ. Например, проект «Toucan» от Trail of Bits интегрировал OpenAI Codex в свой рабочий процесс аудита (подробнее о его выводах ниже). Некоторые стартапы в области безопасности также рекламируют ИИ-аудиторов (например, услуги «ChainGPT Audit»), обычно обертывая GPT-4 пользовательскими промптами для проверки контрактов. Энтузиасты открытого исходного кода создали аудиторские боты на основе ChatGPT на форумах, которые принимают фрагмент Solidity и выдают потенциальные проблемы. Хотя многие из них являются экспериментальными, общая тенденция ясна: ИИ исследуется на каждом уровне процесса проверки безопасности, от автоматического объяснения кода и генерации документации до обнаружения уязвимостей и даже предложения исправлений.

Возможности и ограничения аудиторов на основе БММ​

БММ продемонстрировали заметные возможности в аудите смарт-контрактов:

• Широкие знания: БММ, такая как GPT-4, была обучена на бесчисленных кодах и уязвимостях. Она «знает» об общих проблемах безопасности (реентрабельность, переполнение целых чисел и т. д.) и даже о некоторых исторических эксплойтах. Это позволяет ей распознавать шаблоны, которые могут указывать на ошибку, и вспоминать лучшие практики из документации. Например, она может помнить, что transferFrom ERC-20 должен проверять разрешения (и отмечать отсутствие такой проверки как нарушение). В отличие от статического инструмента, который отмечает только известные шаблоны, БММ может применять рассуждения к новому коду и выявлять проблемы, которые не были явно закодированы в нем разработчиком инструмента.

• Естественные объяснения: ИИ-аудиторы могут предоставлять понятные для человека объяснения потенциальных проблем. Это чрезвычайно ценно для опыта разработчиков. Традиционные инструменты часто выдают загадочные предупреждения, которые требуют экспертных знаний для интерпретации, в то время как инструмент на основе GPT может сгенерировать абзац, объясняющий ошибку простым языком, и даже предложить исправление. AuditGPT, например, не только отмечал нарушения правил ERC, но и описывал, почему код нарушал правило и каковы были последствия. Это помогает менее опытным разработчикам осваивать концепции безопасности.

• Гибкость: С помощью промпт-инжиниринга БММ можно направить на различные аспекты или следовать пользовательским политикам безопасности. Они не ограничены фиксированным набором правил — если вы можете описать свойство или шаблон словами, БММ может попытаться его проверить. Это делает их привлекательными для аудита новых протоколов, которые могут иметь уникальные инварианты или логику (где написание пользовательского статического анализа с нуля было бы нецелесообразным).

Однако были замечены значительные проблемы и вопросы надежности:

• Ограничения рассуждений: Современные БММ иногда испытывают трудности со сложными логическими рассуждениями, необходимыми для анализа безопасности. Trail of Bits сообщили, что «модели не способны хорошо рассуждать о некоторых высокоуровневых концепциях, таких как владение контрактами, реентрабельность и взаимосвязи между функциями». Например, GPT-3.5/4 может теоретически понимать, что такое реентрабельность (и даже объяснять ее), но может не распознать уязвимость реентрабельности, если для этого требуется понимание последовательности вызовов между функциями и изменений состояния. Модель также может пропустить уязвимости, связанные с взаимодействием нескольких контрактов или логикой, зависящей от времени, потому что они выходят за рамки анализа одного фрагмента кода.

• Ложные срабатывания и галлюцинации: Основная проблема заключается в том, что БММ могут выдавать уверенные, но неверные выводы. В аудите «галлюцинация» может означать выявление несуществующей уязвимости или неправильную интерпретацию кода. Эксперимент Trail of Bits с Codex (GPT) показал, что по мере масштабирования до более крупных реальных контрактов «количество ложных срабатываний и галлюцинаций [стало] слишком высоким», до такой степени, что это замедляло аудиторов слишком большим количеством ложных отчетов. Эта непредсказуемость проблематична — инструменту, который слишком часто кричит «волк», разработчики не будут доверять. Успех AuditGPT в поддержании низкого уровня ложных срабатываний (всего 18 из сотен обнаружений) обнадеживает, но это было в ограниченной области. При общем использовании необходимы тщательная разработка промптов и, возможно, циклы человеческого обзора для фильтрации результатов ИИ.

• Ограничения контекста: БММ имеют ограничение на размер контекстного окна, что означает, что они могут «видеть» только определенное количество кода одновременно. Сложные контракты часто охватывают несколько файлов и тысячи строк. Если ИИ не может обработать всю кодовую базу, он может упустить важные связи. Используются такие методы, как нарезка кода (подача контракта по частям), но они рискуют потерять общую картину. Команда LLM-SmartAudit отметила, что с ограничением в 4k токенов GPT-3.5 они не могли анализировать некоторые крупные реальные контракты, пока не переключились на GPT-4 с большим контекстом. Даже тогда разделение анализа на части может привести к тому, что он упустит ошибки, которые проявляются только при рассмотрении системы в целом. Это делает анализ целых протоколов (с несколькими взаимодействующими контрактами) с помощью ИИ реальной проблемой на данный момент.

• Интеграция и инструментарий: Отсутствует надежный инструментарий для разработчиков вокруг ИИ-аудиторов. Запуск анализа БММ не так прост, как запуск линтера. Он включает вызовы API к модели, обработку промпт-инжиниринга, ограничений скорости и парсинг ответов ИИ. «Экосистема программного обеспечения вокруг интеграции БММ с традиционным программным обеспечением слишком примитивна, и все громоздко», как выразилась одна аудиторская команда. Практически нет готовых фреймворков для непрерывного развертывания ИИ-аудитора в CI/CD-пайплайнах при управлении его неопределенностями. Это медленно улучшается (некоторые проекты исследуют CI-ботов, использующих GPT-4 для обзора кода), но это только начало. Более того, отладка того, почему ИИ дал определенный результат, сложна — в отличие от детерминированных инструментов, вы не можете легко отследить логику, которая привела модель к обнаружению или пропуску чего-либо.

• Стоимость и производительность: Использование больших моделей, таких как GPT-4, дорого и может быть медленным. Если вы хотите включить ИИ-аудит в CI/CD-пайплайн, это может добавить несколько минут на контракт и повлечь значительные затраты на API для большого кода. Тонко настроенные модели или БММ с открытым исходным кодом могут снизить затраты, но они, как правило, менее способны, чем GPT-4. Ведутся исследования по созданию меньших, специализированных моделей для безопасности кода, но в настоящее время лучшие результаты получены от крупных проприетарных моделей.

В заключение, аудит с помощью БММ многообещающ, но не является панацеей. Мы наблюдаем гибридные подходы, где ИИ помогает генерировать тесты или анализировать конкретные аспекты, а не выполняет весь аудит от начала до конца. Например, ИИ может предложить потенциальные инварианты или рискованные области, которые затем исследует человек или другой инструмент. Как заметил один инженер по безопасности, технология еще не готова заменить человеческих аудиторов для критически важных задач, учитывая пробелы в рассуждениях и препятствия для интеграции. Однако она уже может быть полезным помощником — «что-то несовершенное может быть намного лучше, чем ничего» в случаях, когда традиционные инструменты не справляются.

Точность и надежность различных наборов инструментов​

Полезно сравнить точность, охват и надежность различных обсуждаемых подходов к аудиту. Ниже приведено резюме выводов исследований и отраслевых оценок:

• Инструменты статического анализа: Статические анализаторы, такие как Slither, ценятся за быструю обратную связь и простоту использования. Они обычно имеют высокую точность, но умеренную полноту — это означает, что большинство проблем, о которых они сообщают, являются реальными (мало ложных срабатываний по замыслу), но они обнаруживают только определенные классы уязвимостей. Исследование 2024 года (RQ1 LLM-SmartAudit) показало, что Slither обнаружил около 46% известных уязвимостей в тестовом наборе. Mythril (символическое выполнение) показал немного лучший результат — 54% полноты. Каждый инструмент имел сильные стороны в определенных типах ошибок (например, Slither очень хорошо обнаруживает арифметические проблемы или использование tx.origin, в то время как символические инструменты превосходны в поиске простых сценариев реентрабельности), но ни один не имел полного охвата. Ложные срабатывания для зрелых инструментов, таких как Slither, относительно низки — его разработчики рекламируют «минимальное количество ложных тревог и быстрое выполнение (менее 1 с на контракт)», что делает его подходящим для использования в CI/CD. Тем не менее, статические инструменты могут давать сбои, если код использует сложные шаблоны; они могут отмечать граничные случаи, которые фактически обрабатываются, или пропускать глубокие логические ошибки, которые не соответствуют известным антишаблонам.

• Фаззинг и тестирование свойств: Фаззеры, такие как фазз/инвариантные тесты Foundry или Echidna от Trail of Bits, доказали свою высокую эффективность в поиске ошибок во время выполнения и нарушений инвариантов. Эти инструменты, как правило, имеют почти нулевые ложные срабатывания в том смысле, что если ошибка сообщается (утверждение не выполнилось), это реальное выполнение контрпримера. Компромисс заключается в ложноотрицательных результатах — если ошибка не проявляется в протестированном пространстве входных данных или количестве запусков, она может быть пропущена. Покрытие зависит от того, насколько хорошо фаззер исследует пространство состояний. При достаточном времени и хороших эвристиках фаззеры обнаружили много серьезных ошибок, которые статический анализ пропустил. Например, Echidna смог быстро воспроизвести ошибки MakerDAO и Compound, для обнаружения которых потребовались усилия по формальной верификации. Однако фаззинг не гарантирует обнаружение каждой логической ошибки. По мере усложнения контрактов фаззерам может потребоваться написание дополнительных инвариантов или использование более интеллектуальных стратегий поиска для достижения более глубоких состояний. С точки зрения метрик, фаззинг не имеет единого показателя «полноты», но эмпирические данные показывают, что важные инварианты обычно могут быть нарушены фаззером, если они могут быть нарушены. Надежность высока для того, что он находит (не требуется ручная сортировка ложных отчетов), но следует помнить, что пройденный фазз-тест не является доказательством корректности — это лишь повышение уверенности.

• Инструменты формальной верификации: Применительно, формальная верификация обеспечивает наивысшую гарантию — успешное доказательство означает, что 100% состояний удовлетворяют свойству. С точки зрения точности, она фактически идеальна (корректна и полна) для свойств, которые она может доказать. Самая большая проблема здесь не в точности результатов, а в сложности использования и узкой области применения. Формальные инструменты также могут иметь ложноотрицательные результаты на практике: они могут просто быть неспособны доказать истинное свойство из-за сложности (давая нулевой результат или тайм-аут, что не является ложным срабатыванием, но означает, что мы не можем верифицировать что-то, что на самом деле безопасно). Они также могут иметь ошибки спецификации, когда инструмент «доказывает» что-то, что не было тем свойством, которое вы имели в виду (ошибка пользователя). В реальных аудитах формальные методы выявили некоторые критические ошибки (успехи Certora включают обнаружение тонкой ошибки SushiSwap и проблемы с библиотекой PRBMath до развертывания). Но их послужной список ограничен тем, как редко они применяются комплексно — как отметили Trail of Bits, было «трудно найти публичные проблемы, обнаруженные исключительно с помощью формальной верификации, в отличие от множества ошибок, найденных фаззингом». Таким образом, хотя формальная верификация чрезвычайно надежна при успехе, ее влияние на общее покрытие инструментария ограничено требуемыми усилиями и опытом.

• Анализ на основе БММ: Точность ИИ-аудиторов в настоящее время является движущейся целью, поскольку новые методы (и более новые модели) быстро расширяют границы. Мы можем получить несколько данных:

  • Система AuditGPT, ориентированная на правила ERC, достигла очень высокой точности (≈96% по количеству ложных срабатываний) и обнаружила сотни проблем, которые статические инструменты или люди упустили из виду. Но это было в узкой области с структурированными промптами. Мы не должны обобщать, что ChatGPT будет на 96% точен при произвольном поиске уязвимостей — вне контролируемой настройки его производительность ниже.
  • В более широком обнаружении уязвимостей LLM-SmartAudit (GPT-3.5) показал ~74% полноты на бенчмарке с умеренным уровнем ложных срабатываний, что лучше, чем любой отдельный традиционный инструмент. При обновлении до GPT-4 со специализированным промптингом (режим TA) он значительно улучшился — например, на наборе из 1400 реальных уязвимостей агент GPT-4 обнаружил ~48% конкретных проблем и ~47% сложных логических проблем, в то время как Slither/Mythril/Conkas обнаружили ~0% (ни одной) из этих конкретных сложных проблем. Это демонстрирует, что БММ могут значительно расширить охват до типов ошибок, которые статический анализ полностью пропускает. С другой стороны, БММ не обнаружила более половины проблем (поэтому у нее также есть существенные ложноотрицательные результаты), и неясно, сколько ложных срабатываний было среди тех, о которых она сообщила — исследование больше фокусировалось на полноте, чем на точности.
  • Эксперимент Trail of Bits Codex/GPT-4 «Toucan» показателен для проблем с надежностью. Изначально, на небольших примерах, Codex мог идентифицировать известные уязвимости (проблемы владения, реентрабельность) при тщательном промптинге. Но как только они попытались масштабировать, они столкнулись с непоследовательными и неверными результатами. Они сообщили, что «количество сбоев было высоким даже в коде среднего размера» и трудно предсказуемым. В конечном итоге они пришли к выводу, что GPT-4 (по состоянию на начало 2023 года) был лишь незначительным улучшением и все еще «не хватало ключевых функций», таких как рассуждение о межфункциональных потоках. Результатом стало то, что ИИ не существенно уменьшил количество ложных срабатываний по сравнению с их статическими инструментами, и не ускорил их рабочий процесс аудита. Другими словами, текущая надежность общего БММ в качестве аудитора была признана недостаточной профессиональными аудиторами в этом испытании.

Подводя итог, каждый набор инструментов имеет свои сильные стороны:

• Статические инструменты: Надежны для быстрого обнаружения известных проблем; низкий уровень шума, но ограниченные типы ошибок (средняя полнота ~40–50% на бенчмарках).
• Фазз/инвариантное тестирование: Очень высокая точность (почти нет ложных тревог) и сильная сторона в поиске функциональных и зависящих от состояния ошибок; покрытие может быть широким, но не гарантированным (нет простой метрики, зависит от времени и качества инвариантов). Часто находит те же ошибки, что и формальные доказательства, если даны достаточные указания.
• Формальная верификация: Золотой стандарт для абсолютной корректности по конкретным свойствам; по сути, 100% полнота/точность для этих свойств при успешном применении. Но практически ограничена узкими проблемами и требует значительных усилий (пока не является решением «одной кнопкой» для полных аудитов).
• Анализ ИИ (БММ): Потенциально высокий охват — может находить ошибки в различных категориях, включая те, которые пропущены другими инструментами — но переменная точность. При специализированных настройках может быть как точным, так и широким (как показал AuditGPT для проверок ERC). Без тщательных ограничений может охватывать широкий круг проблем и требовать человеческой проверки результатов. «Средняя» точность ChatGPT при обнаружении уязвимостей не является впечатляющей (близка к угадыванию, согласно одному исследованию), но лучшие разработанные системы, использующие БММ, превосходят традиционные инструменты. Ведутся активные исследования по повышению надежности результатов ИИ (например, путем перекрестной проверки несколькими агентами или объединения БММ со статическим рассуждением для перепроверки выводов ИИ).

Стоит отметить, что сочетание подходов дает наилучшие результаты. Например, можно запустить Slither (чтобы поймать низко висящие плоды без шума), затем использовать Foundry/Echidna для более глубокого фаззинга поведения, и, возможно, использовать инструмент на основе БММ для сканирования на предмет любых шаблонов или инвариантов, которые не были учтены. Каждый из них будет охватывать различные слепые зоны других.

Проблемы и ограничения внедрения в реальном мире​

На практике внедрение формальной верификации или инструментов ИИ в рабочий процесс разработки сопряжено с прагматическими проблемами. Некоторые ключевые проблемы включают:

• Опыт разработчиков и экспертиза: Традиционная формальная верификация имеет крутую кривую обучения. Написание формальных спецификаций (на CVL, Coq, языке спецификаций Move и т. д.) больше похоже на написание математических доказательств, чем на написание кода. Многим разработчикам не хватает этого опыта, а экспертов по формальным методам не хватает. Напротив, фаззинг с Foundry или написание инвариантов на Solidity гораздо более доступны — это похоже на написание дополнительных тестов. Это главная причина, по которой фазз-тестирование получило более быстрое распространение, чем формальные доказательства в сообществе Ethereum. Команда Trail of Bits явно отметила, что фаззинг «дает аналогичные результаты, но требует значительно меньше навыков и времени», чем формальные методы во многих случаях. Таким образом, хотя формальная верификация может выявлять различные ошибки, многие команды выбирают более простой подход, который дает достаточно хорошие результаты с меньшими усилиями.

• Интеграция в рабочий процесс разработки: Чтобы инструмент получил широкое распространение, он должен вписываться в CI/CD-пайплайны и повседневное кодирование. Такие инструменты, как Slither, здесь преуспевают — он «легко интегрируется в настройки CI/CD, оптимизируя автоматизацию и помогая разработчикам». Разработчик может добавить Slither или Mythril в GitHub Action и заставить его прерывать сборку, если обнаружены проблемы. Фазз-тесты Foundry могут запускаться как часть forge test каждый раз. Тесты инвариантов могут даже непрерывно запускаться в облаке с помощью таких инструментов, как CloudExec, и любой сбой может быть автоматически преобразован в модульный тест с помощью fuzz-utils. Эти интеграции означают, что разработчики получают быструю обратную связь и могут итерировать. Напротив, что-то вроде Certora Prover исторически запускалось как отдельный процесс (или внешней аудиторской командой) и могло занимать часы для получения результата — это не то, что вы запускали бы при каждом коммите. Инструменты на основе ИИ также сталкиваются с препятствиями интеграции: вызов API и детерминированная обработка его вывода в CI/CD нетривиальны. Существует также вопрос безопасности и конфиденциальности — многие организации не хотят отправлять проприетарный код контракта стороннему ИИ-сервису для анализа. Самостоятельно размещенные решения БММ пока не так мощны, как крупные облачные API, поэтому это является камнем преткновения для внедрения ИИ-аудиторов в CI/CD.

• Ложные срабатывания и шум: Инструмент, который сообщает о множестве ложных срабатываний или низкоприоритетных обнаружений, может снизить доверие разработчиков. Статические анализаторы сталкивались с этим в прошлом — например, ранние версии некоторых инструментов заваливали пользователей предупреждениями, многие из которых были неактуальны. Баланс между сигналом и шумом имеет решающее значение. Slither хвалят за минимальное количество ложных тревог, в то время как такой инструмент, как Securify (в его исследовательской форме), часто выдавал множество предупреждений, которые требовали ручной фильтрации. БММ, как обсуждалось, могут генерировать шум, если не нацелены должным образом. Вот почему в настоящее время предложения ИИ обычно воспринимаются как консультативные, а не абсолютные. Команды с большей вероятностью примут шумный инструмент, если он запускается отдельной командой безопасности или в контексте аудита, но для повседневного использования разработчики предпочитают инструменты, которые дают четкие, действенные результаты с низким уровнем шума. Идеал — «прерывать сборку» только при определенных ошибках, а не при гипотетических. Достижение такой надежности является постоянной проблемой, особенно для инструментов ИИ.

• Масштабируемость и производительность: Формальная верификация может быть вычислительно интенсивной. Как отмечалось, солверы могут превышать время ожидания на сложных контрактах. Это затрудняет масштабирование до больших систем. Если проверка одного свойства занимает часы, вы не будете проверять десятки свойств при каждом изменении кода. Фазз-тестирование также сталкивается с ограничениями масштабируемости — исследование огромного пространства состояний или контракта с множеством методов комбинаторно может быть медленным (хотя на практике фаззеры могут работать в фоновом режиме или ночью, чтобы углубить свой поиск). Модели ИИ имеют фиксированные размеры контекста, и увеличение емкости модели дорого. Хотя контекст GPT-4 в 128k токенов является благом, подача ему сотен килобайт кода контракта обходится дорого и все еще недостаточно для очень крупных проектов (представьте сложный протокол с множеством контрактов — вы можете превысить это). Существует также мультичейн-масштабирование: если ваш проект включает взаимодействия между контрактами в разных цепочках (Ethereum ↔ другая цепочка), верификация или анализ этой межцепочечной логики еще более сложны и, вероятно, выходят за рамки существующих инструментов.

• Человеческий надзор и верификация: В конечном итоге большинство команд по-прежнему полагаются на экспертов-аудиторов для окончательного утверждения. Автоматизированные инструменты — это помощники, а не замены. Одно из ограничений всех этих инструментов заключается в том, что они работают в рамках известных свойств или шаблонов. Они могут пропустить совершенно новый тип ошибки или тонкий экономический недостаток в дизайне DeFi-протокола. Человеческие аудиторы используют интуицию и опыт, чтобы рассмотреть, как злоумышленник может подойти к системе, иногда способами, которые ни один инструмент явно не запрограммирован делать. Были случаи, когда контракты проходили все автоматизированные проверки, но человек позже находил уязвимость в бизнес-логике или креативный вектор атаки. Таким образом, проблема заключается в избегании ложного чувства безопасности — разработчики должны правильно интерпретировать вывод формальных инструментов и ИИ и не предполагать, что «проблем не обнаружено» означает, что код на 100% безопасен.

• Поддержание спецификаций и тестов: Для формальной верификации, в частности, одной практической проблемой является отклонение спецификации. Спецификация (инварианты, правила и т. д.) может устареть по мере развития кода. Обеспечение синхронизации кода и его формальной спецификации является нетривиальной задачей управления. Если разработчики не бдительны, доказательства могут «пройти» просто потому, что они доказывают что-то, что больше не имеет отношения к фактическим требованиям кода. Аналогично, инвариантные тесты должны обновляться по мере изменения ожидаемого поведения системы. Это требует культуры разработки, управляемой инвариантами, которой нет у всех команд (хотя есть стремление поощрять ее).

В итоге, основные ограничения — это люди и процессы, а не сырые возможности технологии. Формальные методы и методы с помощью ИИ могут значительно улучшить безопасность, но они должны быть развернуты таким образом, чтобы соответствовать рабочим процессам и навыкам разработчиков. Обнадеживает то, что такие тенденции, как разработка, управляемая инвариантами (запись критических инвариантов с первого дня), набирают обороты, а инструментарий медленно улучшается, чтобы сделать расширенный анализ более простым в использовании. Открытие исходного кода основных инструментов (например, Certora Prover) и интеграция фаззинга в популярные фреймворки (Foundry) снижают барьеры. Со временем мы ожидаем, что разрыв между тем, что может сделать «средний разработчик», и тем, что может сделать «исследователь с докторской степенью», сократится в плане использования этих мощных методов верификации.

Инструменты аудита с открытым исходным кодом и коммерческие​

Ландшафт инструментов безопасности смарт-контрактов включает как проекты с открытым исходным кодом, так и коммерческие услуги. У каждого из них своя роль, и часто они дополняют друг друга:

• Инструменты с открытым исходным кодом: Большинство широко используемых инструментов аудита в экосистеме Ethereum являются открытыми. Сюда входят Slither (статический анализатор), Mythril (символическое выполнение), Echidna (фаззер), Manticore (символическое/конкретное выполнение), Securify (анализатор из ETH Zurich), Solhint/Ethlint (линтеры) и, конечно же, сам Foundry. Инструменты с открытым исходным кодом предпочитают по нескольким причинам: (1) Прозрачность — разработчики могут видеть, как работает инструмент, и доверять тому, что ничего вредоносного или скрытого не происходит (важно в открытой экосистеме). (2) Вклад сообщества — правила и функции добавляются широким сообществом (Slither, например, имеет множество детекторов, внесенных сообществом). (3) Стоимость — они бесплатны в использовании, что важно для многих небольших проектов/стартапов в Web3. (4) Интеграция — открытые инструменты обычно могут запускаться локально или в CI/CD без юридических препятствий, и часто их можно настраивать или скриптовать для конкретных нужд проекта.

  Инструменты с открытым исходным кодом быстро развивались. Например, поддержка Slither для новых версий Solidity и шаблонов постоянно обновляется Trail of Bits. Mythril, разработанный ConsenSys, может анализировать не только Ethereum, но и любую EVM-совместимую цепочку, работая с байт-кодом — показывая, как открытые инструменты могут быть легко перепрофилированы для разных цепочек. Недостатком открытых инструментов является то, что они часто поставляются с оговоркой «используйте на свой страх и риск» — без официальной поддержки или гарантий. Они могут не масштабироваться или не иметь такой же отполированный пользовательский интерфейс, как коммерческий продукт. Но в блокчейне даже многие компании используют открытый исходный код в качестве своих основных внутренних инструментов (иногда с небольшими пользовательскими модификациями).

• Коммерческие услуги и инструменты: Несколько компаний предлагали анализ безопасности как продукт. Примеры включают MythX (облачный API сканирования от ConsenSys Diligence), Certora (которая предлагала свой prover как услугу до открытия исходного кода), CertiK и SlowMist (фирмы, имеющие внутренние сканеры и ИИ, которые они используют в аудитах или предлагают через дашборды), а также некоторые новые участники, такие как Securify от ChainSecurity (компания была приобретена, и ее инструмент используется внутри) или SolidityScan (облачный сканер, который выдает аудиторский отчет). Коммерческие инструменты часто нацелены на предоставление более удобного пользовательского опыта или интегрированного сервиса. Например, MythX интегрировался с расширениями IDE и плагинами CI/CD, чтобы разработчики могли отправлять свои контракты в MythX и получать подробный отчет, включая оценку уязвимости и детали для исправления проблем. Эти сервисы обычно используют комбинацию методов анализа (сопоставление с образцом, символическое выполнение и т. д.), настроенных для минимизации ложных срабатываний.

  Ценностное предложение коммерческих инструментов обычно заключается в удобстве и поддержке. Они могут поддерживать постоянно обновляемую базу знаний об уязвимостях и предоставлять поддержку клиентам в интерпретации результатов. Они также могут обрабатывать сложные вычисления в облаке (так что вам не нужно запускать солвер локально). Однако стоимость является фактором — многие проекты предпочитают не платить за эти услуги, учитывая наличие бесплатных альтернатив. Кроме того, в духе децентрализации некоторые разработчики не решаются полагаться на закрытые сервисы для обеспечения безопасности (этика «проверяй, а не доверяй»). Открытие исходного кода Certora Prover в 2025 году является заметным событием: оно превратило высококлассный коммерческий инструмент в ресурс сообщества. Ожидается, что этот шаг ускорит внедрение, поскольку теперь любой желающий может попытаться формально верифицировать свои контракты без платной лицензии, а открытость кода позволит исследователям улучшать инструмент или адаптировать его к другим цепочкам.

• Услуги по аудиту человеком: Стоит отметить, что помимо программных инструментов, многие аудиты выполняются профессиональными фирмами (Trail of Bits, OpenZeppelin, Certik, PeckShield и т. д.). Эти фирмы используют комбинацию вышеупомянутых инструментов (в основном с открытым исходным кодом) и проприетарных скриптов. Результаты этих усилий часто остаются конфиденциальными или лишь кратко излагаются в аудиторских отчетах. Здесь нет четкой дихотомии «открытый против коммерческого», поскольку даже коммерческие аудиторские фирмы в значительной степени полагаются на инструменты с открытым исходным кодом. Различие больше в экспертизе и ручном труде. Тем не менее, некоторые фирмы разрабатывают проприетарные платформы аудита с помощью ИИ, чтобы получить преимущество (например, были сообщения об использовании «ChainGPT» для внутренних аудитов или разработке CertiK ИИ под названием Skynet для мониторинга в сети). Это не публичные инструменты как таковые, поэтому их точность и методы не широко документированы.

На практике распространенной моделью является сначала открытый исходный код, затем коммерческий (по желанию). Команды будут использовать открытые инструменты во время разработки и тестирования (потому что они могут легко интегрировать их и запускать так часто, как это необходимо). Затем они могут использовать одну или две коммерческие услуги в качестве дополнительной проверки перед развертыванием — например, запустить сканирование MythX, чтобы получить «второе мнение», или нанять фирму, которая использует передовые инструменты, такие как Certora, для формальной верификации критически важного компонента. Поскольку границы размываются (Certora с открытым исходным кодом, результаты MythX часто совпадают с открытыми инструментами), различие меньше касается возможностей и больше — поддержки и удобства.

Одним из примечательных пересечений является мультичейн-поддержка Certora — поддерживая Solana и Stellar формально, они охватывают платформы, где существует меньше открытых альтернатив (например, у Ethereum много открытых инструментов, у Solana до недавнего времени почти не было). По мере расширения инструментов безопасности на новые экосистемы мы можем увидеть, как больше коммерческих предложений заполняют пробелы, по крайней мере, до тех пор, пока открытый исходный код не догонит.

Наконец, стоит отметить, что открытый и коммерческий подходы здесь не являются антагонистическими; они часто учатся друг у друга. Например, методы, впервые примененные в академических/коммерческих инструментах (такие как абстрактная интерпретация, используемая в Securify), в конечном итоге находят свое применение в открытых инструментах, и наоборот, данные об использовании открытых инструментов могут направлять улучшения коммерческих инструментов. Конечный результат, к которому стремятся обе стороны, — это повышение безопасности для всей экосистемы.

Применимость к различным блокчейнам​

Хотя Ethereum был в центре внимания большинства этих инструментов (учитывая его доминирование в активности смарт-контрактов), концепции формальной верификации и аудита с помощью ИИ применимы и к другим блокчейн-платформам. Вот как они трансформируются:

• EVM-совместимые цепочки: Блокчейны, такие как BSC, Polygon, Avalanche C-Chain и т. д., которые используют виртуальную машину Ethereum (EVM), могут напрямую использовать все те же инструменты. Фазз-тест или статический анализ не заботятся о том, будет ли ваш контракт развернут в основной сети Ethereum или на Polygon — байт-код и исходный язык (Solidity/Vyper) одинаковы. Действительно, Mythril и Slither могут анализировать контракты из любой EVM-цепочки, извлекая байт-код из адреса (Mythril просто нужен RPC-эндпоинт). Многие DeFi-проекты в этих цепочках запускают Slither и Echidna так же, как и проекты Ethereum. Аудиты протоколов на BSC или Avalanche обычно используют тот же набор инструментов, что и аудиты Ethereum. Таким образом, кросс-чейн в контексте EVM в основном означает повторное использование инструментария Ethereum.

• Solana: Смарт-контракты Solana написаны на Rust (обычно через фреймворк Anchor) и выполняются на виртуальной машине BPF. Это очень отличающаяся среда от Ethereum, поэтому инструменты, специфичные для Ethereum, не работают из коробки. Однако применяются те же принципы. Например, можно проводить фазз-тестирование программ Solana, используя собственные библиотеки фаззинга Rust или такие инструменты, как cargo-fuzz. Формальная верификация на Solana до недавнего времени практически отсутствовала. Сотрудничество между инженерами Certora и Solana привело к созданию внутреннего инструмента верификации для программ Solana, который может доказывать контракты Rust/Anchor в соответствии со спецификациями. Как отмечалось, Certora расширила свой prover до VM Solana, что означает, что разработчики могут писать правила о поведении программы Solana и проверять их так же, как они делали бы это для Solidity. Это важно, потому что подход Solana «двигайся быстро» означал, что многие контракты запускались без такого строгого тестирования, как в Ethereum; формальные инструменты могли бы улучшить это. ИИ-аудит для Solana также возможен — БММ, которая понимает Rust, может быть запрошена для проверки программы Solana на уязвимости (такие как отсутствующие проверки владения или арифметические ошибки). Это может потребовать тонкой настройки на специфические для Solana шаблоны, но, учитывая популярность Rust, GPT-4 достаточно хорошо разбирается в чтении кода Rust. Вскоре могут появиться инструменты в стиле «ChatGPT для Anchor».

• Polkadot и цепочки на основе Substrate: Смарт-контракты Polkadot могут быть написаны на Rust (скомпилированы в WebAssembly) с использованием фреймворка ink!, или вы можете запустить EVM-паллет (как это делает Moonbeam), что снова позволяет использовать Solidity. В случае ink!/Wasm инструменты верификации все еще находятся в зачаточном состоянии. Можно попытаться формально верифицировать свойства контракта Wasm, используя общие фреймворки верификации Wasm (например, Project Verona от Microsoft или другие рассматривали безопасность Wasm). Открытый prover Certora также упоминает поддержку смарт-контрактов Stellar на WASM, которые по концепции аналогичны любой цепочке на основе Wasm. Так что, вероятно, он применим и к контрактам Wasm Polkadot. Фазз-тестирование контрактов ink! может быть выполнено путем написания тестов на Rust (тесты свойств в Rust могут выполнять аналогичную роль). ИИ-аудит контрактов ink! также будет включать анализ кода Rust, что опять же БММ может сделать с правильным контекстом (хотя она может не знать о специфических макросах или трейтах ink! без некоторых подсказок).

  Кроме того, Polkadot исследует язык Move для параллельной разработки смарт-контрактов (как намекалось на некоторых форумах сообщества). Если Move будет использоваться на парачейнах Polkadot, Move Prover будет поставляться вместе с ним, привнося возможности формальной верификации по умолчанию. Акцент Move на безопасности (ресурсно-ориентированное программирование) и встроенный prover демонстрируют кросс-чейн распространение формальных методов с самого начала.

• Другие блокчейны: Платформы, такие как Tezos (смарт-контракты Michelson) и Algorand (программы TEAL), каждая из которых имела усилия по формальной верификации. Tezos, например, имеет инструмент под названием Mi-Cho-Coq, который предоставляет формальную семантику Michelson и позволяет доказывать свойства. Это больше относится к академической стороне, но показывает, что любой блокчейн с хорошо определенной семантикой контракта может быть подвергнут формальной верификации. ИИ-аудит мог бы, в принципе, быть применен к любому языку программирования — это вопрос соответствующего обучения или промптинга БММ. Для менее распространенных языков БММ может потребоваться некоторая тонкая настройка, чтобы быть эффективной, поскольку она могла быть недостаточно предварительно обучена на достаточном количестве примеров.

• Межцепочечные взаимодействия: Новая проблема — верификация взаимодействий между цепочками (например, мосты или межцепочечный обмен сообщениями). Формальная верификация здесь может включать моделирование состояния нескольких цепочек и протокола связи. Это очень сложно и в настоящее время выходит за рамки большинства инструментов, хотя конкретные протоколы мостов были вручную проанализированы на предмет безопасности. ИИ может помочь в проверке межцепочечного кода (например, проверка контракта Solidity, который взаимодействует с протоколом IBC на Cosmos), но готового решения пока нет.

По сути, инструментарий Ethereum проложил путь для других цепочек. Многие инструменты с открытым исходным кодом адаптируются: например, предпринимаются усилия по созданию статического анализатора, подобного Slither, для Solana (Rust), а концепции тестирования инвариантов не зависят от языка (тестирование на основе свойств существует во многих языках). Открытие исходного кода мощных движков (таких как Certora для нескольких VM) особенно многообещающе для межцепочечной безопасности — одна и та же платформа может использоваться для верификации контракта Solidity, программы Solana и контракта Move, при условии, что для каждого из них написана соответствующая спецификация. Это способствует более единой позиции безопасности во всей отрасли.

Также стоит отметить, что аудит с помощью ИИ принесет пользу всем цепочкам, поскольку модель может быть обучена уязвимостям в любом контексте. Пока ИИ предоставляется правильная информация (спецификации языка, известные шаблоны ошибок в этой экосистеме), он может применять аналогичные рассуждения. Например, ChatGPT можно попросить провести аудит контракта Solidity или модуля Move с соответствующим промптом, и он сделает и то, и другое — он может даже обнаружить что-то вроде «этот модуль Move может нарушать сохранение ресурсов», если у него есть эта концепция. Ограничение заключается в том, была ли ИИ подвержена достаточному количеству обучающих данных для этой цепочки. Ethereum, будучи самым популярным, вероятно, сместил модели в сторону лучшего понимания Solidity. По мере роста других цепочек будущие БММ или тонко настроенные производные могут охватить и их.

Заключение​

Формальная верификация смарт-контрактов и аудит с помощью ИИ — это быстро развивающаяся область. Теперь у нас есть богатый набор инструментов: от детерминированных статических анализаторов и фаззинг-фреймворков, повышающих надежность кода, до передового ИИ, который может рассуждать о коде по-человечески. Формальная верификация, когда-то нишевое академическое занятие, становится более практичной благодаря улучшенным инструментам и интеграции. ИИ, несмотря на его текущие ограничения, показал проблески революционных возможностей в автоматизации анализа безопасности.

Пока нет универсального решения — реальный аудит сочетает в себе несколько методов для достижения эшелонированной обороны. Фаззинг и тестирование инвариантов Foundry уже повышают планку ожиданий перед развертыванием (выявляя многие ошибки, которые могли бы проскользнуть мимо базовых тестов). Аудит с помощью ИИ, при осторожном использовании, может выступать в качестве множителя силы для аудиторов, выявляя проблемы и проверяя соответствие в масштабе и со скоростью, которые ручной обзор в одиночку не может обеспечить. Однако человеческий опыт остается решающим для управления этими инструментами, интерпретации их результатов и определения правильных свойств для проверки.

В дальнейшем мы можем ожидать большей конвергенции этих подходов. Например, ИИ может помочь писать формальные спецификации или предлагать инварианты («ИИ, какие свойства безопасности должны выполняться для этого DeFi-контракта?»). Инструменты фаззинга могут включать ИИ для более интеллектуального управления генерацией входных данных (как это делает PromFuzz). Движки формальной верификации могут использовать машинное обучение для принятия решений о том, какие леммы или эвристики применять. Все это будет способствовать повышению безопасности смарт-контрактов не только в Ethereum, но и на всех блокчейн-платформах. Конечная цель — это будущее, в котором критически важные смарт-контракты могут быть развернуты с высокой уверенностью в их корректности — цель, которая, вероятно, будет достигнута синергетическим использованием формальных методов и помощи ИИ, а не каждым из них по отдельности.

Источники:

• Обзор фаззинга и тестирования инвариантов Foundry
• Trail of Bits о фаззинге против формальной верификации
• Trail of Bits об ограничениях формальной верификации
• Патрик Коллинз о фаззинге/инвариантах против формальных методов
• Trail of Bits об инвариантах в аудитах
• Medium (BuildBear) об использовании Slither и Mythril
• Результаты AuditGPT (соответствие ERC)
• Trail of Bits об ограничениях БММ (Codex/GPT-4)
• Производительность LLM-SmartAudit по сравнению с традиционными инструментами
• Исследование «Detection Made Easy» о точности ChatGPT
• Производительность PromFuzz (БММ+фаззинг)
• Анонс открытого исходного кода Certora (мультичейн)
• Описание Move Prover (Aptos)
• Основы статического анализа (литература по безопасности смарт-контрактов)