Проверка смарт контракта: инструменты аудита и методы защиты кода

Почему проверка смарт-контракта не формальность

Эти цифры показывают масштаб риска для Web3, но сами по себе не говорят, какая доля потерь пришлась на ошибки смарт-контрактов, а какая связана с другими причинами. Приписывать все инциденты одному типу уязвимостей было бы неверно.

Для команды проекта практический вопрос всё равно остаётся прежним: что именно в коде может пойти не так и как это обнаружить до запуска. Смарт-контракты часто управляют активами и исполняют заданную логику автоматически. Если в этой логике есть ошибка, её последствия могут проявиться после публикации контракта, когда исправление уже требует отдельного механизма обновления или миграции. Неизменяемость блокчейна не означает, что любой контракт вообще невозможно заменить, но менять его без предусмотренной архитектуры обычно сложно.

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

Ландшафт угроз: что именно нужно искать

Контракт может быть написан синтаксически корректно и при этом ошибочно управлять балансами, разрешениями или взаимодействием с другими контрактами. Поэтому поиск багов в Solidity коде начинается с понимания того, какие действия доступны пользователям, внешним системам и привилегированным ролям.

Повторный вход, или reentrancy. Контракт вызывает внешний адрес до того, как завершил обновление собственного состояния. Если внешний адрес контролируется атакующим, он может повторно вызвать функцию в момент, когда внутренние данные ещё отражают старое состояние. В результате логика способна повторно обработать уже использованное право или баланс. Уязвимость такого рода стала причиной атаки на The DAO в 2016 году. Современные сценарии могут быть тоньше: повторный вход возникает между разными функциями, при чтении внешнего контракта или через нестандартный токен, поэтому проверять нужно цепочку вызовов и изменения состояния в целом.

Манипуляция ценами и оракулами. DeFi-контракт может опираться на цену, полученную из внешнего источника или вычисленную по данным торгового пула. Если источник допускает кратковременное искажение цены, протокол способен принять неверное решение о залоге, обмене или ликвидации. Здесь уязвимость часто находится в сочетании архитектурных решений: источника цены, способа её усреднения, глубины ликвидности и логики использования котировки.

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

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

Инструмент видит только те риски, которые умеет выразить его метод. Бизнес-правило протокола всё равно должен сформулировать человек.

Статический анализ: первый рубеж

Статический анализ проверяет исходный код без запуска контракта. Анализатор строит представление программы, отслеживает связи между функциями и ищет конструкции, соответствующие известным классам проблем. Для Solidity одним из распространённых инструментов такого рода является Slither, разработанный Trail of Bits.

Slither преобразует Solidity-код во внутреннее представление SlithIR и запускает набор детекторов. Они могут подсветить подозрительные внешние вызовы, потенциальные проблемы с повторным входом, ошибки в применении модификаторов и другие типовые ситуации. Конкретный результат зависит от версии анализатора, компилятора, конфигурации и структуры проекта. Поэтому число предупреждений само по себе мало что говорит о качестве проверки.

Анализатор полезен прежде всего как быстрый способ получить карту мест, требующих внимания. Если детектор указывает на внешний вызов до обновления состояния, это повод проследить весь путь выполнения и проверить, может ли управление вернуться в контракт. Если он отмечает проблему с доступом, предупреждение нужно сопоставить с моделью ролей и ожидаемым поведением протокола. Иногда срабатывание оказывается ложным или несущественным в конкретном контексте. Иногда оно показывает реальную ошибку, которую легко пропустить при обычном чтении кода.

У Slither есть важное ограничение: он распознаёт определённые свойства кода, но не знает, как должен работать конкретный протокол. Анализатор может показать, что функция доступна без ограничений, однако только авторы системы знают, является ли это намеренным поведением. И наоборот, код может не содержать знакомого детектору паттерна, но нарушать финансовое правило проекта.

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

• Проверить, относится ли предупреждение к коду, который действительно используется в развёртываемой версии.
• Проследить, как состояние меняется до и после внешних вызовов.
• Уточнить, какие роли могут вызывать функцию и как эти роли назначаются.
• Зафиксировать причину, по которой ложное срабатывание не требует исправления.
• Повторить запуск после изменений, чтобы убедиться, что правка не создала новую проблему.

Чистый отчёт Slither нельзя превращать в заключение о безопасности. Он показывает, что конкретный запуск не сообщил о проблемах, распознаваемых его детекторами.

Чем Mythril отличается от Echidna

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

Mythril: символьное исполнение

Mythril анализирует байткод EVM с помощью символьного исполнения. Вместо одного конкретного значения инструмент рассматривает входные данные как символические переменные и ищет условия, при которых выполнение приводит к определённому результату. Анализатор может обнаружить путь, на котором нарушается проверка или достигается подозрительная операция.

Символьное исполнение отвечает на вопрос о достижимости состояния. Инструмент строит ветвление программы, связывает его с ограничениями на входные данные и проверяет, существует ли путь к опасному действию. Mythril нельзя приравнивать к случайному перебору вызовов: его задача состоит в систематическом исследовании путей с symbolically заданными условиями.

Полный обход всех путей не гарантирован. Глубина и полнота анализа ограничены сложностью контракта, количеством состояний, настройками инструмента и временем запуска. Каждое ветвление увеличивает число сценариев, поэтому пространство состояний сложного протокола быстро становится слишком большим.

Отчёт Mythril следует читать как указание на сценарий, который стоит воспроизвести и изучить. Нужно проверить достижим ли найденный путь в реальной конфигурации, соблюдены ли предусловия и даёт ли результат атакующему возможность нарушить свойства протокола. Отсутствие находок также не доказывает безопасность: инструмент мог исследовать лишь часть состояний или не распознать конкретное бизнес-правило.

Echidna: динамический фаззинг

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

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

Качество результата Echidna зависит от Properties и сценариев. Если важный инвариант не задан, инструмент не сможет проверить соответствующее поведение. Неверное утверждение способно давать ложные срабатывания или уводить фаззер в недостижимые состояния. Настройка генерации вызовов, начального состояния и ограничений также влияет на полезность найденных примеров.

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

Формальная верификация: математическая строгость в заданных границах

Формальная верификация начинается с описания того, что контракт должен гарантировать. Это описание оформляют как спецификацию, после чего проверяют соответствие реализации заданным свойствам. Для работы с контрактами применяются специализированные средства, в том числе Certora Prover.

Успешная проверка даёт сильную гарантию относительно конкретного свойства, выбранной модели и проверенной части системы. Она не означает, что весь протокол безопасен при любых обстоятельствах. Если спецификация упускает важное условие, доказательство не обнаружит это упущение автоматически. Если компонент, влияющий на результат, не включён в модель, вывод на него не распространяется.

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

Работа требует времени и специалистов, которые понимают код, бизнес-логику и язык спецификаций. Поэтому формальную верификацию обычно сосредоточивают на критических компонентах: логике учёта средств, механизмах ликвидации, управлении доступом или других частях, где ошибка способна нарушить ключевые свойства протокола. Она дополняет статический анализ, фаззинг и ручную проверку, позволяя сосредоточить математические гарантии на действительно важных правилах.

Защита логики от повторного входа и ошибок доступа

Один из известных защитных паттернов, Checks-Effects-Interactions, задаёт порядок действий внутри функции:

1. Сначала проверяются условия: доступ, баланс, лимиты и допустимость операции.

2. Затем обновляется внутреннее состояние: пересчитывается баланс или отмечается, что действие уже выполнено.

3. После этого выполняются внешние вызовы, включая отправку средств или обращение к другому контракту.

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

Ещё один распространённый механизм, ReentrancyGuard, блокирует повторный вход в защищённую функцию с помощью состояния-замка. В библиотеках OpenZeppelin такой механизм доступен как отдельный инструмент. Его наличие не делает весь контракт неуязвимым. Нужно проверить, какие функции помечены защитой, могут ли они вызывать друг друга и как устроены внешние взаимодействия. Если уязвимый путь проходит через незащищённую функцию, использование ReentrancyGuard ничего не меняет.

Контроль доступа требует такой же предметной проверки. Для каждой привилегированной операции стоит определить, кто её вызывает, кто назначает и меняет роли, предусмотрена ли передача полномочий и существует ли обходной путь к той же операции. Ошибки появляются не только из-за отсутствующего модификатора. Роль может быть назначена неверному адресу, остаться у прежнего участника после изменения модели управления или получить лишние полномочия.

В сложных протоколах полномочия обычно разделяют между несколькими участниками. Двухшаговая передача роли снижает риск ошибки с одним адресом. Мультиподпись требует согласия нескольких держателей ключей, а временная задержка даёт возможность заметить подозрительную операцию до её исполнения. Эти механизмы сами по себе не гарантируют правильность действий, но сокращают последствия ошибки или злоупотребления.

Аудит как часть процесса разработки

Автоматические инструменты помогают быстрее находить определённые классы ошибок, но внешний аудит нужен для проверки того, как компоненты и бизнес-правила работают вместе. Аудитор изучает код, архитектуру, предположения проекта и результаты автоматических проверок. Его работа состоит в анализе поведения системы, а не в запуске набора анализаторов и пересылке отчёта.

Аудит безопасности смарт контракта имеет определённый объём. Проверенная версия кода, набор зависимостей, параметры развёртывания и предполагаемая конфигурация ролей должны быть зафиксированы. Если после заключения меняется логика, добавляются функции или меняются зависимости, часть выводов может потерять актуальность. Даже неизменный код сохраняет риски, связанные с ключами управления, прокси-контрактами, внешними системами и настройкой развёртывания.

Разумная последовательность работы выглядит как цикл:

1. На ранних этапах запускать статический анализ, чтобы замечать типовые проблемы до усложнения кодовой базы.

2. Формулировать инварианты и проверять их фаззером на последовательностях вызовов.

3. Использовать символьное исполнение для проверки достижимости подозрительных состояний и переходов.

4. Применять формальную верификацию к критическим свойствам, где цена ошибки особенно велика.

5. Вручную исследовать архитектуру, роли, внешние зависимости и экономические допущения протокола.

6. Воспроизводить каждую находку, проверять её достижимость и устранять как уязвимость, так и ошибку в самом тесте.

7. Повторять проверки после исправлений и фиксировать новую версию кода.

8. Сопоставлять выводы аудита с фактической конфигурацией релиза.

Такой процесс связывает автоматизацию с инженерным разбором. Slither помогает выбрать подозрительные места, Mythril исследует пути к ним, Echidna ищет последовательности, нарушающие свойства, а формальные методы проверяют наиболее важные гарантии. Решение о готовности контракта к запуску принимается после сопоставления всех результатов с архитектурой и правилами протокола.

Что важно помнить перед релизом

Проверка смарт-контракта начинается не с выбора инструмента, а с точного описания того, как система обязана работать. Спецификация, модель ролей и перечень критических инвариантов позволяют превратить общий риск в проверяемые утверждения. После этого Slither, Mythril, Echidna и средства формальной верификации решают разные задачи, а ручной анализ связывает их результаты с реальной архитектурой.

Защитные механизмы имеют конкретные границы. Checks-Effects-Interactions и ReentrancyGuard помогают организовать внешние вызовы и защитить выбранные функции, но не заменяют проверку цепочки состояний. Контроль доступа требует прослеживания полномочий от их выдачи до исполнения привилегированных операций.

Итоговый аудит остаётся выводом о проверенной версии и заданной конфигурации. После изменения кода или ролей прежние гарантии требуют перепроверки. Для протокола, который управляет активами, именно такой цикл становится практической защитой от ошибок, скрытых за обычным внешним вызовом.