trailofbits/manticoreИнструмент символьного исполнения
Этот проект больше не разрабатывается и не поддерживается.
Manticore — это инструмент символьного выполнения для анализа смарт-контрактов и бинарных файлов.
Manticore может анализировать следующие типы программ:
Примечание: Мы рекомендуем устанавливать 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.
Для разработочной установки обратитесь к нашей вики.
Manticore имеет интерфейс командной строки, который может выполнять базовый символьный анализ бинарного файла или смарт-контракта.
Результаты анализа будут помещены в рабочую директорию, начинающуюся с mcore_. Для информации о рабочей директории см. вики.
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
Предоставляется альтернативный CLI-инструмент, который упрощает тестирование контрактов и позволяет писать методы свойств на том же высокоуровневом языке, который использует контракт. Ознакомьтесь с документацией manticore-verifier. Смотрите демо
$ 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
Manticore предоставляет программный интерфейс Python, который можно использовать для реализации мощных пользовательских анализов.
Для смарт-контрактов 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)))
Также возможно использовать 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()
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])
ulimit -s 100000 или передав --ulimit stack=100000000:100000000 в docker runsolc в $PATH.crytic-compile непосредственно на вашем коде — это упростит выявление любых проблем.Manticore полагается на внешний решатель, поддерживающий smtlib2. В настоящее время поддерживаются Z3, Yices и CVC4, и их можно выбрать через командную строку или настройки конфигурации.
Если Yices доступен, Manticore будет использовать его по умолчанию. Если нет, он вернётся к Z3 или CVC4. Если вы хотите вручную выбрать, какой решатель использовать, вы можете сделать это следующим образом:
manticore --smt.solver Z3
Для получения более подробной информации перейдите на 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 невероятно быстр. Подробнее здесь 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.
Директория examples содержит несколько небольших примеров, демонстрирующих возможности API.
Репозиторий manticore-examples содержит более сложные примеры, включая несколько реальных задач CTF.
Если вы хотите сообщить об ошибке или запросить новую функцию, пожалуйста, используйте нашу страницу issues.
Для вопросов и разъяснений, пожалуйста, посетите страницу обсуждений.
Manticore лицензирован и распространяется под лицензией AGPLv3. Свяжитесь с нами, если вы ищете исключение из условий.
Если вы используете Manticore в академической работе, рассмотрите возможность подачи заявки на Crytic $10k Research Prize.
