Echidna: Быстрый фаззер для смарт-контрактов

Echidna — это странное существо, которое питается багами и обладает высокой электрочувствительностью (с извинениями перед Джейкобом Стэнли)

Если говорить серьёзно, Echidna — это программа на Haskell, предназначенная для фаззинга и тестирования на основе свойств смарт-контрактов Ethereum. Она использует сложные кампании грамматического фаззинга на основе ABI контракта для опровержения определяемых пользователем предикатов или утверждений Solidity. Мы разработали Echidna с учётом модульности, поэтому её легко расширять, добавляя новые мутации или тестируя конкретные контракты в особых случаях.

Возможности

• Генерирует входные данные, адаптированные к вашему реальному коду
• Опциональный сбор корпуса, мутации и наведение по покрытию для поиска более глубоких багов
• Работает на основе Slither для извлечения полезной информации перед кампанией фаззинга
• Интеграция с исходным кодом для определения того, какие строки покрыты после кампании фаззинга
• Интерактивный терминальный интерфейс, вывод в текстовом формате или JSON
• Автоматическая минимизация тестовых случаев для быстрой триажной сортировки
• Бесшовная интеграция в процесс разработки

.. и прекрасный логотип ручной работы в высоком разрешении.

Использование

Запуск средства выполнения тестов

Основная функциональность Echidna — это исполняемый файл под названием echidna, который принимает контракт и список инвариантов (свойств, которые всегда должны оставаться истинными) в качестве входных данных. Для каждого инварианта он генерирует случайные последовательности вызовов контракта и проверяет, выполняется ли инвариант. Если ему удаётся найти способ опровергнуть инвариант, он выводит последовательность вызовов, которая это делает. Если не удаётся, у вас есть некоторая уверенность в том, что контракт безопасен.

Написание инвариантов

Инварианты выражаются в виде функций Solidity, имена которых начинаются с echidna_, не имеют аргументов и возвращают логическое значение. Например, если у вас есть переменная balance, которая никогда не должна опускаться ниже 20, вы можете написать дополнительную функцию в вашем контракте, подобную этой:```solidity function echidna_check_balance() public returns (bool) { return(balance >= 20); }

Чтобы проверить эти инварианты, выполните:```sh
$ echidna myContract.sol

Пример контракта с тестами можно найти в tests/solidity/basic/flags.sol. Чтобы запустить его, выполните:```sh $ echidna tests/solidity/basic/flags.sol

Echidna должна найти последовательность вызовов, которая опровергает `echidna_sometimesfalse`, и не должна найти опровергающий вход для `echidna_alwaystrue`.

### Режимы тестирования

В приведённом выше примере используется режим **property** по умолчанию, но Echidna поддерживает несколько режимов тестирования, настраиваемых через `testMode` в файле конфигурации или `--test-mode` в CLI:

* **`property`** (по умолчанию): Тестирование функций с префиксом `echidna_`, возвращающих `bool`.
* **`assertion`**: Обнаружение сбоев утверждений из `assert()` и хелперов Foundry `assertX` (`assertTrue`, `assertEq` и т. д.).
* **`foundry`**: Запуск тестов в стиле Foundry, следуя его соглашениям об именовании: юнит- и фаззинг-тесты с префиксом `test` (те, что с префиксом `testFail`, должны ревертиться) и stateful-инварианты с префиксом `invariant` или `statefulFuzz`. Функции с префиксами `check` и `prove` являются символическими точками входа, но поскольку этот режим представляет собой кампанию фаззинга, они фаззятся как любая другая тестовая функция.
* **`verification`**: Символическая верификация каждой функции контракта с использованием одной транзакции. Функции с префиксами `check` и `prove` всегда используются как точки входа.
* **`overflow`**: Обнаружение целочисленных переполнений/недополнений (Solidity >= 0.8.0).
* **`optimization`**: Максимизация возвращаемого значения функций с префиксом `echidna_`, возвращающих `int256` (использует тот же настраиваемый префикс, что и режим property).
* **`exploration`**: Сбор покрытия без проверки свойств.

### Сбор и визуализация покрытия

После завершения кампании Echidna может сохранить **корпус**, максимизирующий покрытие, в специальном каталоге, указанном в опции конфигурации `corpusDir`. Этот каталог будет содержать две записи: (1) каталог с именем `coverage` с JSON-файлами, которые могут быть воспроизведены Echidna, и (2) обычный текстовый файл с именем `covered.txt` — копию исходного кода с аннотациями покрытия.

Если вы запустите пример `tests/solidity/basic/flags.sol`, Echidna сохранит несколько файлов сериализованных транзакций в каталоге `coverage` и файл `covered.$(date +%s).txt` со следующими строками:```text
*r  |  function set0(int val) public returns (bool){
*   |    if (val % 100 == 0)
*   |      flag0 = false;
  }

*r  |  function set1(int val) public returns (bool){
*   |    if (val % 10 == 0 && !flag0)
*   |      flag1 = false;
  }

Наш инструмент помечает каждый трейс выполнения в корпусе следующим "маркером строки":

• * если выполнение завершилось STOP
• r если выполнение завершилось REVERT
• o если выполнение завершилось ошибкой out-of-gas
• e если выполнение завершилось любой другой ошибкой (деление на ноль, ошибка утверждения и т.д.)

Поддержка систем сборки смарт-контрактов

Echidna может тестировать контракты, скомпилированные с помощью различных систем сборки смарт-контрактов, включая Foundry, Hardhat и Truffle, используя crytic-compile. Чтобы запустить Echidna с текущей платформой компиляции, используйте echidna ..

Кроме того, Echidna поддерживает два режима тестирования сложных контрактов. Во-первых, можно воспользоваться существующим состоянием сети и использовать его в качестве базового состояния для Echidna. Во-вторых, Echidna может вызывать любой контракт с известным ABI, передав соответствующий исходный код Solidity в CLI. Используйте allContracts: true в вашей конфигурации, чтобы включить это.

Краткий курс по Echidna

Наш репозиторий Building Secure Smart Contracts содержит краткий курс по Echidna, включая примеры, уроки и упражнения.

Использование Echidna в рабочем процессе GitHub Actions

Существует действие Echidna, которое можно использовать для запуска echidna в рамках рабочего процесса GitHub Actions. Пожалуйста, обратитесь к репозиторию crytic/echidna-action за инструкциями по использованию и примерами.

Параметры конфигурации