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

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

Manticore

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

Возможности

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

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

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

Установка

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

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

pip install manticore

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

pip install "manticore[native]"

Вариант 3: Установка ночной сборки для разработки:

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, поэтому некоторые опкоды могут не поддерживаться. В крайнем случае вы можете попробовать компилировать с использованием 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

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

Не стесняйтесь заходить в наш Slack-канал #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 во время исследования.
• Under-constrained symbolic execution Интерфейс для символьного исследования отдельных функций с помощью Manticore.