Как использовать Мантикору для поиска ошибок в смарт-контрактах

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

Установка

Для Мантикоры требуется Python версии 3.6 или выше. Ее можно установить через pip или с помощью Docker.

Мантикора через 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/

Мантикора через pip

pip3 install --user manticore

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

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

Чтобы запустить скрипт Python с помощью Python 3:

python3 script.py

Введение в динамическое символьное выполнение

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

Динамическое символьное выполнение (DSE) — это метод анализа программ, который исследует пространство состояний с высокой степенью семантической осведомленности. Этот метод основан на обнаружении «путей программы», представленных в виде математических формул, называемых path predicates. Концептуально этот метод работает с предикатами путей в два этапа:

1. Они строятся с использованием ограничений на входные данные программы.
2. Они используются для генерации входных данных программы, которые приведут к выполнению соответствующих путей.

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

Пример предиката пути

Чтобы понять, как работает DSE, рассмотрим следующий пример:

function f(uint a){

  if (a == 65) {
      // Присутствует баг
  }

}

Поскольку f() содержит два пути, DSE построит два разных предиката пути:

• Путь 1: a == 65
• Путь 2: Not (a == 65)

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

Проверка свойств

Мантикора позволяет полностью контролировать выполнение каждого пути. В результате это позволяет добавлять произвольные ограничения практически ко всему. Этот контроль позволяет создавать свойства для контракта.

Рассмотрим следующий пример:

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // нет защиты от переполнения
  return c;
}

Здесь в функции есть только один путь для исследования:

• Путь 1: c = a + b

Используя Мантикору, вы можете проверить наличие переполнения и добавить ограничения к предикату пути:

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

Если возможно найти значения a и b, для которых приведенный выше предикат пути выполним, это означает, что вы нашли переполнение. Например, солвер может сгенерировать входные данные a = 10 , b = MAXUINT256.

Если рассмотреть исправленную версию:

function safe_add(uint a, uint b) returns(uint c){
  c = a + b;
  require(c>=a);
  require(c>=b);
  return c;
}

Связанная формула с проверкой переполнения будет выглядеть так:

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

Эта формула не может быть решена; иными словами, это доказательство того, что в safe_add значение c всегда будет увеличиваться.

Таким образом, DSE — это мощный инструмент, который может проверять произвольные ограничения в вашем коде.

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

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

pragma solidity >=0.4.24 <0.6.0;

contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

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

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

$ manticore project

Вы получите вывод тестовых случаев, похожий на этот (порядок может меняться):

...
... m.c.manticore:INFO: Generated testcase No. 0 - STOP
... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
... m.c.manticore:INFO: Generated testcase No. 4 - STOP
... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

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

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

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

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

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

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

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

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

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

Создание аккаунтов

Первое, что вам следует сделать, это инициализировать новый блокчейн с помощью следующих команд:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

Аккаунт, не являющийся контрактом, создается с помощью m.create_account (opens in a new tab):

user_account = m.create_account(balance=1000)

Контракт Solidity можно развернуть с помощью m.solidity_create_contract (opens in a new tab):

source_code = '''
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}
'''
# Initiate the contract
contract_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).

Выполнение транзакций

Мантикора поддерживает два типа транзакций:

• Необработанная транзакция (raw transaction): исследуются все функции
• Именованная транзакция (named transaction): исследуется только одна функция

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

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

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

Вызывающая сторона, адрес, данные или значение транзакции могут быть как конкретными, так и символьными:

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

Например:

symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
              address=contract_address,
              data=symbolic_data,
              value=symbolic_value)

Если данные символьные, Мантикора исследует все функции контракта во время выполнения транзакции. Будет полезно ознакомиться с объяснением резервной функции в статье Практика в Ethernaut CTF (opens in a new tab), чтобы понять, как работает выбор функции.

Именованная транзакция

Функции могут быть выполнены по их имени. Чтобы выполнить f(uint var) с символьным значением от user_account и с 0 эфира, используйте:

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var, caller=user_account, value=0)

Если value транзакции не указано, по умолчанию оно равно 0.

Итоги

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

Рабочее пространство

m.workspace — это директория, используемая в качестве выходной для всех сгенерированных файлов:

print("Results are in {}".format(m.workspace))

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

Чтобы остановить исследование, используйте m.finalize() (opens in a new tab). После вызова этого метода больше не следует отправлять транзакции, и Мантикора сгенерирует тестовые случаи для каждого исследованного пути.

Итоги: Запуск под управлением Мантикоры

Объединив все предыдущие шаги, мы получим:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

print("Results are in {}".format(m.workspace))
m.finalize() # остановить исследование

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

Получение путей с выбросом исключений

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

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Использование информации о состоянии

Каждый выполненный путь имеет свое состояние блокчейна. Состояние может быть либо готовым (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): все состояния

for state in m.all_states:
    # сделать что-то с состоянием

Вы можете получить доступ к информации о состоянии. Например:

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

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

data = state.platform.transactions[0].return_data
data = ABI.deserialize("uint", data)

Как сгенерировать тестовый случай

Используйте m.generate_testcase(state, name) (opens in a new tab) для генерации тестового случая:

m.generate_testcase(state, 'BugFound')

Итоги

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

Итоги: Получение путей с выбросом исключений

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

## Проверить, завершается ли выполнение откатом или INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        print('Throw found {}'.format(m.workspace))
        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):

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Операторы

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

• Operators.AND,
• Operators.OR,
• Operators.UGT (беззнаковое больше),
• Operators.UGE (беззнаковое больше или равно),
• Operators.ULT (беззнаковое меньше),
• Operators.ULE (беззнаковое меньше или равно).

Для импорта модуля используйте следующее:

from manticore.core.smtlib import Operators

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

last_return = Operators.CONCAT(256, *last_return)

Ограничения

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

Глобальное ограничение

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

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
              address=contract_account,
              data=m.make_symbolic_buffer(320),
              value=0)

Ограничение состояния

Используйте state.constrain(constraint) (opens in a new tab) для добавления ограничения к конкретному состоянию. Это можно использовать для ограничения состояния после его исследования, чтобы проверить на нем какое-либо свойство.

Проверка ограничения

Используйте solver.check(state.constraints), чтобы узнать, выполнимо ли еще ограничение. Например, следующее ограничит symbolic_value значением, отличным от 65, и проверит, выполнимо ли еще состояние:

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # состояние достижимо

Итоги: Добавление ограничений

Добавив ограничение к предыдущему коду, мы получим:

from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib.solver import Z3Solver

solver = Z3Solver.instance()

m = ManticoreEVM()

with open("example.sol") as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

no_bug_found = True

## Проверить, завершается ли выполнение откатом или INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        # мы не рассматриваем путь, где a == 65
        condition = symbolic_var != 65
        if m.generate_testcase(state, name="BugFound", only_if=condition):
            print(f'Bug found, results are in {m.workspace}')
            no_bug_found = False

if no_bug_found:
    print(f'No bug found')

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

Последнее обновление страницы: 3 апреля 2026 г.

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+6

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