:warning: Проект архивирован :warning:

Этот проект больше не разрабатывается и поддерживается внутри компании.

Manticore

Manticore — это инструмент символьного выполнения для анализа смарт-контрактов и бинарных файлов.

Функции

• Изучение программ: Manticore может выполнять программу с символьными входными данными и исследовать все возможные состояния, которые она может достичь
• Генерация входных данных: Manticore может автоматически создавать конкретные входные данные, приводящие к заданному состоянию программы
• Обнаружение ошибок: Manticore может обнаруживать сбои и другие ошибки в бинарных файлах и смарт-контрактах
• Инструменты для наблюдения: Manticore предоставляет точечное управление исследованием состояний через обратные вызовы событий и хуки инструкций
• Программный интерфейс: Manticore предоставляет доступ к своему движку анализа через Python API

Manticore может анализировать следующие типы программ:

• Смарт-контракты Ethereum (байткод EVM)
• Бинарные файлы Linux ELF (x86, x86_64, aarch64 и ARMv7)
• Модули WASM

Установка

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

Вариант 1: Установка из PyPI:

pip install manticore

Вариант 2: Установка из PyPI с дополнительными зависимостями для выполнения нативных бинарных файлов:

pip install "manticore[native]"

Вариант 3: Установка ночной development-сборки:

pip install --pre "manticore[native]"

Вариант 4: Установка из ветки master:

git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"

Вариант 5: Установка через Docker:

docker pull trailofbits/manticore

После установки будут доступны CLI-утилита manticore и Python API.

Для разработки см. нашу вики.

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

CLI

У Manticore есть командная строка, которая может выполнять базовый символьный анализ бинарного файла или смарт-контракта. Результаты анализа будут помещены в рабочий каталог, начинающийся с mcore_. Для получения информации о рабочем каталоге см. вики.

EVM

CLI Manticore автоматически определяет, что вы пытаетесь протестировать контракт, если (например) у контракта есть расширение .sol или .vy. Смотрите демо.

Нажмите, чтобы раскрыть:

$ manticore examples/evm/umd_example.sol 
 [9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ...
 [9921] m.e.manticore:INFO: Starting symbolic create contract
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 0
 [9921] m.e.manticore:INFO: 4 alive states, 6 terminated states
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 1
 [9921] m.e.manticore:INFO: 16 alive states, 22 terminated states
[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
...
[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs)
[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs)
[9921] m.c.manticore:INFO: Results in ~/manticore/mcore_gsncmlgx

Manticore-verifier

Предоставляется альтернативный CLI-инструмент, упрощающий тестирование контрактов и позволяющий писать методы проверки свойств на том же высокоуровневом языке, который используется в контракте. Изучите документацию manticore-verifier. Смотрите демо

Native

Нажмите, чтобы раскрыть:

$ manticore examples/linux/basic
[9507] m.n.manticore:INFO: Loading program examples/linux/basic
[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Results in ~/manticore/mcore_7u7hgfay
[9507] m.n.manticore:INFO: Total time: 2.8029580116271973

API

Manticore предоставляет программный интерфейс на языке Python, который можно использовать для реализации мощных специфичных анализов.

EVM

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

Нажмите, чтобы раскрыть:

from manticore.ethereum import ManticoreEVM
contract_src="""
contract Adder {
  function incremented(uint value) public returns (uint){
      if (value == 1)
          revert();
      return value + 1;
  }
}
"""
m = ManticoreEVM()

user_account = m.create_account(balance=10000000)
contract_account = m.solidity_create_contract(contract_src,
                                            owner=user_account,
                                            balance=0)
value = m.make_symbolic_value()

contract_account.incremented(value)

for state in m.ready_states:
  print("can value be 1? {}".format(state.can_be_true(value == 1)))
  print("can value be 200? {}".format(state.can_be_true(value == 200)))

Native

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

Нажмите, чтобы раскрыть:

# example Manticore script
from manticore.native import Manticore

m = Manticore.linux('./example')

@m.hook(0x400ca0)
def hook(state):
cpu = state.cpu
print('eax', cpu.EAX)
print(cpu.read_int(cpu.ESP))

m.kill()  # tell Manticore to stop

m.run()

WASM

Manticore также может оценивать функции WebAssembly над символьными входными данными для проверки свойств или общего анализа.

Нажмите, чтобы раскрыть:

from manticore.wasm import ManticoreWASM

m = ManticoreWASM("collatz.wasm")

def arg_gen(state):
  # Generate a symbolic argument to pass to the collatz function.
  # Possible values: 4, 6, 8
  arg = state.new_symbolic_value(32, "collatz_arg")
  state.constrain(arg > 3)
  state.constrain(arg < 9)
  state.constrain(arg % 2 == 0)
  return [arg]


# Run the collatz function with the given argument generator.
m.collatz(arg_gen)

# Manually collect return values
# Prints 2, 3, 8
for idx, val_list in enumerate(m.collect_returns()):
  print("State", idx, "::", val_list[0])

Требования

• Manticore требует Python 3.7 или новее
• Manticore официально поддерживает последнюю LTS-версию Ubuntu, предоставляемую Github Actions
  • Manticore имеет экспериментальную поддержку EVM и WASM (но не нативных бинарных файлов Linux) на macOS
• Мы рекомендуем запускать с увеличенным размером стека. Это можно сделать, выполнив команду ulimit -s 100000 или передав --ulimit stack=100000000:100000000 в docker run

Компиляция смарт-контрактов

• Для анализа смарт-контрактов Ethereum необходимо наличие программы solc в вашем $PATH.
• Manticore использует crytic-compile для сборки смарт-контрактов. Если у вас возникают проблемы с компиляцией, попробуйте запустить crytic-compile на вашем коде напрямую, чтобы проще идентифицировать возможные проблемы.
• Мы всё ещё работаем над реализацией полной поддержки семантики инструкций EVM Istanbul, поэтому некоторые opcode-инструкции могут быть не поддержаны. В качестве обходного пути вы можете попробовать компилировать с использованием Solidity 0.4.x, чтобы избежать генерации этих инструкций.

Использование другого решателя (Yices, Z3, CVC4)

Manticore опирается на внешний решатель, поддерживающий smtlib2. В настоящее время поддерживаются Z3, Yices и CVC4, и их можно выбрать через командную строку или настройки конфигурации. Если Yices доступен, Manticore будет использовать его по умолчанию. Если нет, то переключится на Z3 или CVC4. Если вы хотите вручную выбрать, какой решатель использовать, вы можете сделать это так: manticore --smt.solver Z3

Установка CVC4

Для более подробной информации перейдите на https://cvc4.github.io/. В остальных случаях просто получите бинарный файл и используйте его.

    sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
    sudo chmod +x /usr/bin/cvc4

Установка Yices

Yices невероятно быстрый. Более подробную информацию здесь https://yices.csl.sri.com/

    sudo add-apt-repository ppa:sri-csl/formal-methods
    sudo apt-get update
    sudo apt-get install yices2

Получение помощи

Смело заходите на наш канал #manticore в Empire Hacking для получения помощи по использованию или расширению Manticore.

Документация доступна в нескольких местах:

* Вики содержит информацию о начале работы с Manticore и участии в разработке

* Ссылка на API имеет более подробную и глубокую документацию нашего API

* Примеры каталог содержит несколько небольших примеров, демонстрирующих функции API

* Репозиторий manticore-examples содержит более сложные примеры, включая некоторые реальные CTF-задачи

Если вы хотите сообщить о ошибке или пожелании, пожалуйста, используйте нашу страницу issues.

Для вопросов и уточнений, посетите страницу обсуждений.

Лицензия

Manticore лицензируется и распространяется на условиях лицензии AGPLv3. Свяжитесь с нами если вы ищете исключение из условий.

Публикации

• Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts, Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, Artem Dinaburg - ASE 19

Если вы используете Manticore в академической работе, рассмотрите возможность подачи заявки на Crytic $10k Research Prize.

Видеодемонстрация с ASE 2019

Интеграции с инструментами

• MATE: Merged Analysis To prevent Exploits
  • Mantiserve: REST API взаимодействие с Manticore для запуска, остановки и проверки экземпляров Manticore
  • Dwarfcore: Плагины и детекторы для использования в движке Mantiserve во время исследования
  • Символьное выполнение с ограничениями Интерфейс для символьного исследования отдельных функций с использованием Manticore