Как использовать 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: Сгенерирован тестовый пример № 0 - STOP
3... m.c.manticore:INFO: Сгенерирован тестовый пример № 1 - REVERT
4... m.c.manticore:INFO: Сгенерирован тестовый пример № 2 - RETURN
5... m.c.manticore:INFO: Сгенерирован тестовый пример № 3 - REVERT
6... m.c.manticore:INFO: Сгенерирован тестовый пример № 4 - STOP
7... m.c.manticore:INFO: Сгенерирован тестовый пример № 5 - REVERT
8... m.c.manticore:INFO: Сгенерирован тестовый пример № 6 - REVERT
9... m.c.manticore:INFO: Результаты в /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Показать все

Без дополнительной информации Manticore будет исследовать контракт с новыми символическими транзакциями до тех пор, пока не перестанет находить новые пути в контракте. Manticore не запускает новые транзакции после неудачной (например, после revert).

Manticore выведет информацию в каталог mcore_*. Помимо прочего, в этом каталоге вы найдете:

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

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

Сводка исследования: f(!=65) означает, что f вызывается с любым значением, отличным от 65.

Как вы можете заметить, Manticore создает уникальный тестовый пример для каждой успешной или отмененной транзакции.

Используйте флаг --quick-mode для быстрого исследования кода (он отключает детекторы ошибок, расчет газа и т. д.).

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

В этом разделе подробно описывается, как управлять смарт-контрактом через Manticore Python API. Вы можете создать новый файл с расширением *.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# Инициировать контракт
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("Результаты находятся в {}".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("Результаты в {}".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](https://manticore.readthedocs.io/en/latest/states.html#accessing): список готовых состояний (они не выполнили REVERT/INVALID)
• [m.killed_states](https://manticore.readthedocs.io/en/latest/states.html#accessings): список завершенных состояний
• [m.all_states](https://manticore.readthedocs.io/en/latest/states.html#accessings): все состояния

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('Найдено исключение {}'.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'Найдена ошибка, результаты в {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Ошибок не найдено')
Показать все
Копировать

Весь приведенный выше код вы можете найти в файле 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

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