Руководство по инструментам безопасности смарт-контрактов

Мы будем использовать три различных метода тестирования и анализа программ:

• Статический анализ с помощью Slither. Все пути программы аппроксимируются и анализируются одновременно через различные представления программы (например, граф потока управления).
• Фазинг с помощью Echidna. Код выполняется с псевдослучайной генерацией транзакций. Фазер попытается найти последовательность транзакций для нарушения заданного свойства.
• Символическое выполнение с помощью Manticore. Метод формальной верификации, который преобразует каждый путь выполнения в математическую формулу, для которой можно проверить ограничения.

Каждый метод имеет свои преимущества и недостатки и будет полезен в конкретных случаях:

* если все пути исследованы без тайм-аута

Slither анализирует контракты за считаные секунды, однако статический анализ может приводить к ложным срабатываниям и будет менее пригоден для сложных проверок (например, арифметических). Запускайте Slither через API для простого доступа к встроенным детекторам или через API для пользовательских проверок.

Выполнение Echidna занимает несколько минут, и она выдает только истинно-положительные результаты. Echidna проверяет предоставленные пользователем свойства безопасности, написанные на Solidity. Она может пропускать ошибки, поскольку основана на случайном исследовании.

Manticore выполняет самый "тяжеловесный" анализ. Как и Echidna, Manticore проверяет предоставленные пользователем свойства. Ее выполнение занимает больше времени, но она может доказать достоверность свойства и не сообщает о ложных срабатываниях.

Предлагаемый рабочий процесс

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

• Используйте CLI Slither для выявления распространенных проблем
• Используйте Echidna для тестирования высокоуровневых свойств безопасности вашего контракта
• Используйте Slither для написания пользовательских статических проверок
• Используйте Manticore, когда вам потребуется углубленная проверка критически важных свойств безопасности

Примечание о модульных тестах. Модульные тесты необходимы для создания высококачественного программного обеспечения. Однако эти методы не очень подходят для поиска уязвимостей в системе безопасности. Обычно они используются для тестирования позитивного поведения кода (т. е. код работает так, как ожидалось в обычном контексте), в то время как уязвимости в системе безопасности, как правило, находятся в крайних случаях, которые разработчики не учли. В нашем исследовании десятков аудитов безопасности смарт-контрактов покрытие модульными тестами не повлияло на количество или серьезность уязвимостей (opens in a new tab), которые мы обнаружили в коде наших клиентов.

Определение свойств безопасности

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

• Быстрая оценка рисков (Rapid Risk Assessments) (opens in a new tab) (наш предпочтительный подход при нехватке времени)
• Руководство по моделированию угроз для систем, ориентированных на данные (Guide to Data-Centric System Threat Modeling) (opens in a new tab) (также известно как NIST 800-154)
• Моделирование угроз по Шостаку (Shostack threat modeling) (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Использование утверждений (Use of Assertions) (opens in a new tab)

Компоненты

Знание того, что вы хотите проверить, также поможет вам выбрать правильный инструмент.

Общие области, которые часто актуальны для смарт-контрактов, включают в себя:

• Конечный автомат. Большинство контрактов можно представить в виде конечного автомата. Рассмотрите возможность проверки того, что (1) недопустимое состояние не может быть достигнуто, (2) если состояние является допустимым, оно может быть достигнуто и (3) никакое состояние не блокирует контракт.

  • Echidna и Manticore — предпочтительные инструменты для тестирования спецификаций конечного автомата.

• Средства контроля доступа. Если в вашей системе есть привилегированные пользователи (например, владелец, контроллеры и т. д.) вы должны убедиться, что (1) каждый пользователь может выполнять только разрешенные действия и (2) ни один пользователь не может заблокировать действия более привилегированного пользователя.

  • Slither, Echidna и Manticore могут проверять правильность контроля доступа. Например, Slither может проверить, что только у функций из белого списка отсутствует модификатор onlyOwner. Echidna и Manticore полезны для более сложного контроля доступа, например, когда разрешение предоставляется только в том случае, если контракт достигает определенного состояния.

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

  • Manticore — лучший выбор в этом случае. Echidna можно использовать, если арифметика выходит за рамки возможностей решателя SMT.

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

  • Slither — это инструмент для обеспечения обнаружения этих проблем.

• Внешние взаимодействия. Контракты взаимодействуют друг с другом, и некоторым внешним контрактам не следует доверять. Например, если ваш контракт полагается на внешние оракулы, останется ли он безопасным, если половина доступных оракулов будет скомпрометирована?

  • Manticore и Echidna — лучший выбор для тестирования внешних взаимодействий с вашими контрактами. У Manticore есть встроенный механизм для создания заглушек для внешних контрактов.

• Соответствие стандартам. Стандарты Ethereum (например, ERC20) имеют историю недостатков в своей конструкции. Помните об ограничениях стандарта, на котором вы строите.

  • Slither, Echidna и Manticore помогут вам обнаружить отклонения от заданного стандарта.

Шпаргалка по выбору инструментов

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

Наши публичные аудиты содержат примеры проверенных или протестированных свойств. Рекомендуем прочитать разделы Automated Testing and Verification (Автоматическое тестирование и проверка) следующих отчетов, чтобы ознакомиться с реальными свойствами безопасности:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)

Последнее обновление страницы: 22 октября 2025 г.

p (opens in a new tab)

m (opens in a new tab)

c (opens in a new tab)

+9

Посмотреть участников