Як використовувати Echidna для тестування смарт-контрактів

мова програмування

Смарт-контракти

захист

тестування

фазинг

Для досвідчених користувачів

Trailofbits

Building secure contracts

10 квітня 2020 р.

12 читається за хвилину

Встановлення

Echidna можна встановити через Docker або за допомогою попередньо скомпільованого бінарного файлу.

Echidna через Docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

Остання команда запускає eth-security-toolbox у контейнері Docker, який має доступ до вашого поточного каталогу. Ви можете змінювати файли з вашого хоста та запускати інструменти для файлів із контейнера Docker

Усередині Docker запустіть:

solc-select 0.5.11
cd /home/training

Бінарний файл

https://github.com/crytic/echidna/releases/tag/v1.4.0.0 (opens in a new tab)

Вступ до фазингу на основі властивостей

Echidna — це фазер на основі властивостей, який ми описували в наших попередніх дописах у блозі (1 (opens in a new tab), 2 (opens in a new tab), 3 (opens in a new tab)).

Фазинг

Фазинг (opens in a new tab) — це добре відома техніка у спільноті безпеки. Він полягає в генеруванні більш-менш випадкових вхідних даних для виявлення помилок у програмі. Фазери для традиційного програмного забезпечення (такі як AFL (opens in a new tab) або LibFuzzer (opens in a new tab)) відомі як ефективні інструменти для пошуку помилок.

Окрім суто випадкової генерації вхідних даних, існує багато технік і стратегій для генерації хороших вхідних даних, зокрема:

Отримання зворотного зв’язку від кожного виконання та використання його для керування генерацією. Наприклад, якщо щойно згенеровані вхідні дані ведуть до відкриття нового шляху, має сенс згенерувати нові вхідні дані, близькі до них.
Генерування вхідних даних із дотриманням структурних обмежень. Наприклад, якщо ваші вхідні дані містять заголовок із контрольною сумою, є сенс дозволити фазеру генерувати вхідні дані, що перевіряють цю контрольну суму.
Використання відомих вхідних даних для створення нових: якщо у вас є доступ до великого набору дійсних вхідних даних, ваш фазер може генерувати нові вхідні дані з них, а не починати генерацію з нуля. Зазвичай їх називають сідами.

Фазинг на основі властивостей

Echidna належить до специфічної родини фазерів: фазинг на основі властивостей, значною мірою натхненний QuickCheck (opens in a new tab). На відміну від класичного фазера, який намагатиметься знайти збої, Echidna намагатиметься порушити визначені користувачем інваріанти.

У смарт-контрактах інваріанти — це функції Solidity, які можуть представляти будь-який некоректний або недійсний стан, якого може досягти контракт, зокрема:

Некоректний контроль доступу: зловмисник став власником контракту.
Некоректний кінцевий автомат: токени можна передавати, поки контракт призупинено.
Некоректна арифметика: користувач може викликати спустошення свого балансу (underflow) і отримати необмежену кількість безкоштовних токенів.

Тестування властивості за допомогою Echidna

Розглянемо, як протестувати смарт-контракт за допомогою Echidna. Ціллю є наступний смарт-контракт token.sol (opens in a new tab):

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
Показати все

Припустимо, що цей токен повинен мати такі властивості:

Будь-хто може мати щонайбільше 1000 токенів
Токен не можна передати (це не токен ERC20)

Написання властивості

Властивості Echidna — це функції Solidity. Властивість повинна:

Не мати аргументів
Повертати true у разі успішної перевірки
Мати назву, що починається з echidna

Echidna:

Автоматично генеруватиме довільні транзакції для тестування властивості.
Повідомляти про будь-які транзакції, що змушують властивість повертати false або викликати помилку.
Ігнорувати побічні ефекти під час виклику властивості (тобто якщо властивість змінює змінну стану, ця зміна скасовується після тесту)

Наступна властивість перевіряє, що той, хто викликає функцію, має не більше 1000 токенів:

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}

Використовуйте успадкування, щоб відокремити ваш контракт від ваших властивостей:

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }

token.sol (opens in a new tab) реалізує властивість і успадковує від токена.

Ініціалізація контракту

Echidna потребує конструктор без аргументів. Якщо ваш контракт потребує спеціальної ініціалізації, ви повинні зробити це в конструкторі.

У Echidna є кілька спеціальних адрес:

0x00a329c0648769A73afAc7F9381E08FB43dBEA72, яка викликає конструктор.
0x10000, 0x20000 та 0x00a329C0648769a73afAC7F9381e08fb43DBEA70, які випадково викликають інші функції.

У нашому поточному прикладі нам не потрібна якась особлива ініціалізація, тому наш конструктор порожній.

Запуск Echidna

Echidna запускається за допомогою:

echidna-test contract.sol

Якщо contract.sol містить кілька контрактів, ви можете вказати цільовий:

echidna-test contract.sol --contract MyContract

Підсумок: Тестування властивості

Нижче наведено підсумок запуску Echidna на нашому прикладі:

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }

echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: збій!💥
  Послідовність викликів, скорочення (1205/5000):
    airdrop()
    backdoor()
...
Показати все

Echidna виявила, що властивість порушується, якщо викликається backdoor.

Фільтрування функцій для виклику під час кампанії фазингу

Розглянемо, як фільтрувати функції, що підлягають фазингу. Ціллю є наступний смарт-контракт:

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
Показати все

Цей невеликий приклад змушує Echidna знайти певну послідовність транзакцій, щоб змінити змінну стану. Це складно для фазера (рекомендується використовувати інструмент символьного виконання, наприклад Manticore (opens in a new tab)). Ми можемо запустити Echidna, щоб перевірити це:

echidna-test multi.sol
...
echidna_state4: пройдено! 🎉
Seed: -3684648582249875403

Фільтрування функцій

Echidna має труднощі з пошуком правильної послідовності для тестування цього контракту, оскільки дві функції скидання (reset1 і reset2) встановлюють для всіх змінних стану значення false. Однак ми можемо використати спеціальну функцію Echidna, щоб або додати функцію скидання до чорного списку, або додати до білого списку лише функції f, g, h та i.

Щоб додати функції до чорного списку, ми можемо використати такий файл конфігурації:

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

Інший підхід до фільтрування функцій — це перерахувати функції з білого списку. Для цього ми можемо використати такий файл конфігурації:

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]

filterBlacklist має значення true за замовчуванням.
Фільтрація виконуватиметься лише за назвою (без параметрів). Якщо у вас є f() та f(uint256), фільтр "f" відповідатиме обом функціям.

Запуск Echidna

Щоб запустити Echidna з файлом конфігурації blacklist.yaml:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: збій!💥
  Послідовність виклику:
    f(12)
    g(8)
    h(42)
    i()

Echidna майже миттєво знайде послідовність транзакцій, щоб спростувати властивість.

Підсумок: Фільтрування функцій

Echidna може додавати функції до чорного або білого списку для виклику під час кампанії фазингу за допомогою:

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]

echidna-test contract.sol --config config.yaml
...

Echidna починає кампанію фазингу, або додаючи до чорного списку f1, f2 і f3, або викликаючи тільки їх, залежно від логічного значення filterBlacklist.

Як тестувати `assert` Solidity за допомогою Echidna

У цьому короткому посібнику ми покажемо, як використовувати Echidna для тестування перевірки тверджень (assert) у контрактах. Припустімо, у нас є такий контракт:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
Показати все

Написання твердження

Ми хочемо переконатися, що tmp менше або дорівнює counter після повернення їхньої різниці. Ми могли б написати властивість Echidna, але нам потрібно буде десь зберігати значення tmp. Натомість ми могли б використати таке твердження:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Показати все

Запуск Echidna

Щоб увімкнути тестування збоїв тверджень, створіть файл конфігурації Echidna (opens in a new tab) config.yaml:

1checkAsserts: true

Коли ми запускаємо цей контракт у Echidna, ми отримуємо очікувані результати:

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: збій!💥
  Послідовність викликів, скорочення (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Показати все

Як бачите, Echidna повідомляє про збій твердження у функції inc. Можна додати більше одного твердження на функцію, але Echidna не може сказати, яке саме твердження не виконалося.

Коли і як використовувати твердження

Твердження можна використовувати як альтернативу явним властивостям, особливо якщо умови, які потрібно перевірити, безпосередньо пов'язані з правильним використанням деякої операції f. Додавання тверджень після певного коду забезпечить, що перевірка відбудеться одразу після його виконання:

1function f(..) public {
2    // some complex code
3    ...
4    assert (condition);
5    ...
6}
7

Навпаки, використання явної властивості Echidna призведе до випадкового виконання транзакцій, і немає простого способу точно визначити, коли відбудеться перевірка. Проте, все ще можна зробити це обхідним шляхом:

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}

Однак, є деякі проблеми:

Це не спрацює, якщо f оголошена як internal або external.
Незрозуміло, які аргументи слід використовувати для виклику f.
Якщо f скасовує транзакцію, властивість не буде виконана.

Загалом, ми рекомендуємо дотримуватися рекомендації Джона Регера (opens in a new tab) щодо використання тверджень:

Не викликайте жодних побічних ефектів під час перевірки твердження. Наприклад: assert(ChangeStateAndReturn() == 1)
Не робіть тверджень щодо очевидних речей. Наприклад assert(var >= 0), де var оголошено як uint.

Нарешті, будь ласка, не використовуйте require замість assert, оскільки Echidna не зможе це виявити (але контракт все одно скасує транзакцію).

Підсумок: перевірка тверджень

Нижче наведено підсумок запуску Echidna на нашому прикладі:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Показати все

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: збій!💥
  Послідовність викликів, скорочення (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Показати все

Echidna виявила, що твердження в inc може не виконуватися, якщо ця функція викликається кілька разів із великими аргументами.

Збір і зміна корпусу Echidna

Розглянемо, як збирати та використовувати корпус транзакцій з Echidna. Ціллю є наступний смарт-контракт magic.sol (opens in a new tab):

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
Показати все

Цей невеликий приклад змушує Echidna знайти певні значення для зміни змінної стану. Це складно для фазера (рекомендується використовувати інструмент символьного виконання, як-от Manticore (opens in a new tab)). Ми можемо запустити Echidna, щоб перевірити це:

echidna-test magic.sol
...
echidna_magic_values: пройдено! 🎉
Seed: 2221503356319272685

Однак ми все ще можемо використовувати Echidna для збору корпусу під час запуску цієї кампанії фазингу.

Збір корпусу

Щоб увімкнути збір корпусу, створіть каталог корпусу:

mkdir corpus-magic

І файл конфігурації Echidna (opens in a new tab) config.yaml:

1coverage: true
2corpusDir: "corpus-magic"

Тепер ми можемо запустити наш інструмент і перевірити зібраний корпус:

echidna-test magic.sol --config config.yaml

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

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
Показати все

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

Використання початкових даних для корпусу

Echidna потребує деякої допомоги, щоб впоратися з функцією magic. Ми збираємося скопіювати та змінити вхідні дані, щоб використовувати відповідні параметри для неї:

cp corpus/2712688662897926208.txt corpus/new.txt

Ми змінимо new.txt, щоб викликати magic(42,129,333,0). Тепер ми можемо перезапустити Echidna:

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: збій!💥
  Послідовність виклику:
    magic(42,129,333,0)
Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537
Показати все

Цього разу було виявлено, що властивість порушується негайно.

Пошук транзакцій з високим споживанням газу

Розглянемо, як за допомогою Echidna знаходити транзакції з високим споживанням газу. Ціллю є наступний смарт-контракт:

1contract C {
2  uint state;
3
4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
Показати все

Тут expensive може мати велике споживання газу.

Наразі Echidna завжди потребує властивості для тестування: тут echidna_test завжди повертає true. Ми можемо запустити Echidna, щоб перевірити це:

1echidna-test gas.sol
2...
3echidna_test: пройдено! 🎉
4
5Seed: 2320549945714142710

Вимірювання споживання газу

Щоб увімкнути вимірювання споживання газу за допомогою Echidna, створіть файл конфігурації config.yaml:

1estimateGas: true

У цьому прикладі ми також зменшимо розмір послідовності транзакцій, щоб полегшити розуміння результатів:

1seqLen: 2
2estimateGas: true

Запуск Echidna

Після створення файлу конфігурації ми можемо запустити Echidna так:

echidna-test gas.sol --config config.yaml
...
echidna_test: пройдено! 🎉
f використала максимум 1333608 газу
  Послідовність виклику:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2
Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325
Показати все

Показаний газ є оцінкою, наданою HEVM (opens in a new tab).

Відфільтровування викликів, що зменшують газ

Посібник з фільтрування функцій для виклику під час кампанії фазингу вище показує, як видалити деякі функції з тестування.
Це може бути критично важливим для отримання точної оцінки газу. Розгляньмо такий приклад:

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}
Показати все

Якщо Echidna може викликати всі функції, вона не зможе легко знайти транзакції з високою вартістю газу:

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
Показати все

Це тому, що вартість залежить від розміру addrs, а випадкові виклики, як правило, залишають масив майже порожнім. Однак додавання pop та clear до чорного списку дає нам набагато кращі результати:

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]

1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

Підсумок: пошук транзакцій з високим споживанням газу

Echidna може знаходити транзакції з високим споживанням газу за допомогою параметра конфігурації estimateGas:

1estimateGas: true

echidna-test contract.sol --config config.yaml
...

Echidna повідомить про послідовність із максимальним споживанням газу для кожної функції після завершення кампанії фазингу.

Останні оновлення сторінки: 21 жовтня 2025 р.

Як використовувати Echidna для тестування смарт-контрактів

Встановлення

Echidna через Docker

Бінарний файл

Вступ до фазингу на основі властивостей

Фазинг

Фазинг на основі властивостей

Тестування властивості за допомогою Echidna

Написання властивості

Ініціалізація контракту

Запуск Echidna

Підсумок: Тестування властивості

Фільтрування функцій для виклику під час кампанії фазингу

Фільтрування функцій

Запуск Echidna

Підсумок: Фільтрування функцій

Як тестувати assert Solidity за допомогою Echidna

Написання твердження

Запуск Echidna

Коли і як використовувати твердження

Підсумок: перевірка тверджень

Збір і зміна корпусу Echidna

Збір корпусу

Використання початкових даних для корпусу

Пошук транзакцій з високим споживанням газу

Вимірювання споживання газу

Запуск Echidna

Відфільтровування викликів, що зменшують газ

Підсумок: пошук транзакцій з високим споживанням газу

Чи була ця інструкція корисною?

Як тестувати `assert` Solidity за допомогою Echidna