Як використовувати Manticore для пошуку помилок у смарт-контрактах

Мета цього посібника — показати, як використовувати Manticore для автоматичного пошуку помилок у смарт-контрактах.

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

Для Manticore потрібна версія Python >= 3.6. Його можна інсталювати за допомогою pip або за допомогою Docker.

Manticore через 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/trufflecon/

Manticore через pip

pip3 install --user manticore

Рекомендується використовувати solc 0.5.11.

Запуск скрипту

Щоб запустити скрипт Python за допомогою Python 3:

python3 script.py

Вступ до динамічного символьного виконання

Коротко про динамічне символьне виконання

Динамічне символьне виконання (DSE) — це метод аналізу програм, який досліджує простір станів із високим ступенем семантичної обізнаності. Цей метод базується на виявленні "шляхів програми", представлених у вигляді математичних формул, які називаються предикатами шляху. Концептуально цей метод оперує предикатами шляху у два етапи:

1. Вони будуються з використанням обмежень на вхідні дані програми.
2. Вони використовуються для генерації вхідних даних програми, які спричинять виконання пов'язаних шляхів.

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

Приклад предиката шляху

Щоб зрозуміти, як працює DSE, розгляньмо такий приклад:

1function f(uint a){
2
3  if (a == 65) {
4      // Наявна помилка
5  }
6
7}
Копіювати

Оскільки f() містить два шляхи, DSE побудує два різні предикати шляху:

• Шлях 1: a == 65
• Шлях 2: Not (a == 65)

Кожен предикат шляху — це математична формула, яку можна передати так званому SMT-рішувачу (opens in a new tab), який спробує розв'язати рівняння. Для Шляху 1 рішувач повідомить, що шлях можна дослідити за допомогою a = 65. Для Шляху 2 рішувач може надати a будь-яке значення, відмінне від 65, наприклад a = 0.

Перевірка властивостей

Manticore дає змогу повністю контролювати виконання кожного шляху. Завдяки цьому ви можете додавати довільні обмеження майже до будь-чого. Цей контроль дає змогу створювати властивості контракту.

Розгляньмо такий приклад:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // немає захисту від переповнення
3  return c;
4}
Копіювати

Тут є лише один шлях для дослідження у функції:

• Шлях 1: c = a + b

За допомогою Manticore ви можете перевірити наявність переповнення та додати обмеження до предиката шляху:

• c = a + b AND (c < a OR c < b)

Якщо можливо знайти такі значення a та b, для яких наведений вище предикат шляху є здійсненним, це означає, що ви знайшли переповнення. Наприклад, рішувач може згенерувати вхідні дані a = 10, b = MAXUINT256.

Якщо розглянути виправлену версію:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
Копіювати

Відповідна формула з перевіркою переповнення матиме такий вигляд:

• c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

Цю формулу неможливо розв'язати; іншими словами, це доказ того, що в safe_add c завжди збільшуватиметься.

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

Запуск у Manticore

Ми розглянемо, як досліджувати смарт-контракт за допомогою Manticore API. Цільовим є такий смарт-контракт example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
Показати все
Копіювати

Запуск автономного дослідження

Ви можете запустити Manticore безпосередньо для смарт-контракту за допомогою такої команди (project може бути файлом Solidity або каталогом проєкту):

$ manticore project

Ви отримаєте вивід тестових випадків, подібний до цього (порядок може змінюватися):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Показати все

Без додаткової інформації Manticore досліджуватиме контракт за допомогою нових символьних транзакцій, доки не перестане знаходити нові шляхи в контракті. Manticore не запускає нові транзакції після невдалої (наприклад, після скасування).

Manticore виведе інформацію в каталог mcore_*. Серед іншого, у цьому каталозі ви знайдете:

• global.summary: покриття та попередження компілятора
• test_XXXXX.summary: покриття, остання інструкція, баланси облікових записів для кожного тестового випадку
• test_XXXXX.tx: детальний список транзакцій для кожного тестового випадку

Тут Manticore знаходить 7 тестових випадків, які відповідають (порядок імен файлів може змінюватися):

Підсумок дослідження: f(!=65) означає виклик f із будь-яким значенням, відмінним від 65.

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

Використовуйте прапорець --quick-mode для швидкого дослідження коду (він вимикає детектори помилок, розрахунок газу тощо)

Маніпулювання смарт-контрактом через API

У цьому розділі докладно описано, як маніпулювати смарт-контрактом за допомогою Manticore Python API. Ви можете створити новий файл із розширенням Python *.py і написати необхідний код, додавши в цей файл команди API (основи яких будуть описані нижче), а потім запустити його за допомогою команди $ python3 *.py. Також ви можете виконати наведені нижче команди безпосередньо в консолі Python. Щоб запустити консоль, скористайтеся командою $ python3.

Створення облікових записів

Перше, що вам потрібно зробити, це ініціювати новий блокчейн за допомогою таких команд:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Копіювати

Неконтрактний обліковий запис створюється за допомогою m.create_account (opens in a new tab):

1user_account = m.create_account(balance=1000)
Копіювати

Контракт Solidity можна розгорнути за допомогою m.solidity_create_contract (opens in a new tab):

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Показати все
Копіювати

Підсумок

• Ви можете створювати облікові записи користувачів і контракти за допомогою m.create_account (opens in a new tab) та m.solidity_create_contract (opens in a new tab).

Виконання транзакцій

Manticore підтримує два типи транзакцій:

• Необроблена транзакція: досліджуються всі функції
• Іменована транзакція: досліджується лише одна функція

Необроблена транзакція

Необроблена транзакція виконується за допомогою m.transaction (opens in a new tab):

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
Копіювати

Той, хто викликає, адреса, дані або значення транзакції можуть бути конкретними або символьними:

• m.make_symbolic_value (opens in a new tab) створює символьне значення.
• m.make_symbolic_buffer(size) (opens in a new tab) створює символьний масив байтів.

Наприклад:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
Копіювати

Якщо дані є символьними, Manticore дослідить усі функції контракту під час виконання транзакції. Щоб зрозуміти, як працює вибір функції, корисно ознайомитися з поясненням резервної функції в статті Hands on the Ethernaut CTF (opens in a new tab).

Іменована транзакція

Функції можна виконувати за їхньою назвою. Щоб виконати f(uint var) із символьним значенням від user_account і з 0 ефіру, використовуйте:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
Копіювати

Якщо value транзакції не вказано, за замовчуванням воно дорівнює 0.

Підсумок

• Аргументи транзакції можуть бути конкретними або символьними
• Необроблена транзакція досліджуватиме всі функції
• Функції можна викликати за їхньою назвою

Робоча область

m.workspace — це каталог, який використовується як вихідний каталог для всіх створених файлів:

1print("Results are in {}".format(m.workspace))
Копіювати

Завершення дослідження

Щоб зупинити дослідження, використовуйте m.finalize() (opens in a new tab). Після виклику цього методу не слід надсилати жодних транзакцій, і Manticore генерує тестові випадки для кожного дослідженого шляху.

Підсумок: Запуск у Manticore

Об'єднавши всі попередні кроки, отримуємо:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # зупинити дослідження
Показати все
Копіювати

Весь наведений вище код можна знайти в example_run.py (opens in a new tab)

Отримання шляхів, що спричиняють винятки

Тепер ми згенеруємо конкретні вхідні дані для шляхів, які викликають виняток у f(). Цільовим є такий смарт-контракт example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Копіювати

Використання інформації про стан

Кожен виконаний шлях має свій стан блокчейну. Стан може бути або готовим (ready), або завершеним (killed), що означає, що він досяг інструкції THROW або REVERT:

• m.ready_states (opens in a new tab): список готових станів (вони не виконали REVERT/INVALID)
• m.killed_states (opens in a new tab): список завершених станів
• m.all_states (opens in a new tab): усі стани

1for state in m.all_states:
2    # щось зробити зі станом
Копіювати

Ви можете отримати доступ до інформації про стан. Наприклад:

• state.platform.get_balance(account.address): баланс облікового запису
• state.platform.transactions: список транзакцій
• state.platform.transactions[-1].return_data: дані, повернуті останньою транзакцією

Дані, повернуті останньою транзакцією, є масивом, який можна перетворити на значення за допомогою ABI.deserialize, наприклад:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
Копіювати

Як згенерувати тестовий випадок

Використовуйте m.generate_testcase(state, name) (opens in a new tab) для генерації тестового випадку:

1m.generate_testcase(state, 'BugFound')
Копіювати

Підсумок

• Ви можете ітерувати стани за допомогою m.all_states
• state.platform.get_balance(account.address) повертає баланс облікового запису
• state.platform.transactions повертає список транзакцій
• transaction.return_data — це повернуті дані
• m.generate_testcase(state, name) генерує вхідні дані для стану

Підсумок: Отримання шляху, що спричиняє виняток

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Перевірка, чи завершується виконання з REVERT або INVALID
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Throw found {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Показати все
Копіювати

Весь наведений вище код можна знайти в example_run.py (opens in a new tab)

Зауважте, що ми могли б створити набагато простіший скрипт, оскільки всі стани, що повертаються terminated_state, мають у своєму результаті REVERT або INVALID: цей приклад мав лише продемонструвати, як маніпулювати API.

Додавання обмежень

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

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Копіювати

Оператори

Модуль Operators (opens in a new tab) полегшує маніпулювання обмеженнями, серед іншого він надає:

• Operators.AND,
• Operators.OR,
• Operators.UGT (беззнакове «більше ніж»),
• Operators.UGE (беззнакове «більше або дорівнює»),
• Operators.ULT (беззнакове «менше ніж»),
• Operators.ULE (беззнакове «менше або дорівнює»).

Щоб імпортувати модуль, використовуйте таке:

1from manticore.core.smtlib import Operators
Копіювати

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

1last_return = Operators.CONCAT(256, *last_return)
Копіювати

Обмеження

Ви можете використовувати обмеження глобально або для певного стану.

Глобальне обмеження

Використовуйте m.constrain(constraint) для додавання глобального обмеження. Наприклад, ви можете викликати контракт із символьної адреси та обмежити цю адресу певними значеннями:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
Копіювати

Обмеження стану

Використовуйте state.constrain(constraint) (opens in a new tab) для додавання обмеження до певного стану. Його можна використовувати для обмеження стану після його дослідження, щоб перевірити певну властивість.

Перевірка обмеження

Використовуйте solver.check(state.constraints), щоб дізнатися, чи є обмеження все ще здійсненним. Наприклад, наступний код обмежить symbolic_value значенням, відмінним від 65, і перевірить, чи стан все ще є здійсненним:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # стан є здійсненним
Копіювати

Підсумок: Додавання обмежень

Додавши обмеження до попереднього коду, отримуємо:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Перевірка, чи завершується виконання з REVERT або INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # ми не розглядаємо шлях, де a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Bug found, results are in {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'No bug found')
Показати все
Копіювати

Весь наведений вище код можна знайти в example_run.py (opens in a new tab)

Останні оновлення сторінки: 26 квітня 2024 р.

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+5

Переглянути учасників