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

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

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

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

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

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

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

Мантикора выполняет самый «тяжелый» анализ. Как и Эхидна, Мантикора проверяет предоставленные пользователем свойства. Ей потребуется больше времени на выполнение, но она может доказать валидность свойства и не будет выдавать ложных срабатываний.

Рекомендуемый рабочий процесс

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

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

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

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

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

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

Компоненты

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

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

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

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

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

  • Слизер, Эхидна и Мантикора могут проверять правильность контроля доступа. Например, Слизер может проверить, что только функции из белого списка не имеют модификатора onlyOwner. Эхидна и Мантикора полезны для более сложного контроля доступа, например, для разрешения, предоставляемого только в том случае, если контракт достигает заданного состояния.

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

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

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

  • Слизер — это инструмент, обеспечивающий обнаружение этих проблем.

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

  • Мантикора и Эхидна — лучший выбор для тестирования внешних взаимодействий с вашими контрактами. Мантикора имеет встроенный механизм для создания заглушек (stub) внешних контрактов.

• Соответствие стандартам. Стандарты Эфириума (например, ERC-20) имеют историю недостатков в своем дизайне. Помните об ограничениях стандарта, на котором вы строите.

  • Слизер, Эхидна и Мантикора помогут вам обнаружить отклонения от заданного стандарта.

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

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

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

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