⚠️ Проект заархивирован ⚠️

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

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")