manticore
Manticore 0.3.7
Этот проект больше не разрабатывается и не поддерживается внутри компании. Тем не менее, мы рады рассмотреть и принять небольшие, хорошо написанные запросы на включение от сообщества. Мы будем рассматривать только исправления ошибок и незначительные улучшения.
На любые новые или открытые в настоящее время вопросы и обсуждения сообщество ответит и поддержит.
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 и API Python.
Информацию об установке для разработки см. в нашей вики.
Мантикора имеет интерфейс командной строки, который может выполнять базовый символьный анализ двоичного или смарт-контракта. Результаты анализа будут помещены в каталог рабочей области, начинающийся с mcore_ . Информацию о рабочей области смотрите в вики.
Manticore CLI автоматически обнаруживает, что вы пытаетесь протестировать контракт, если (например) контракт имеет расширение .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 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.8029580116271973Manticore предоставляет программный интерфейс 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 непосредственно в вашем коде, чтобы упростить выявление проблем. Мантикора использует внешний решатель, поддерживающий smtlib2. В настоящее время поддерживаются Z3, Yices и CVC4, и их можно выбрать с помощью командной строки или настроек конфигурации. Если Yices доступен, Мантикора будет использовать его по умолчанию. В противном случае он вернется к 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
Йайс невероятно быстр. Подробности здесь 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.
Документация доступна в нескольких местах:
Вики содержит информацию о том, как начать работу с Мантикорой и внести свой вклад.
В справочнике по API содержится более подробная и подробная документация по нашему API.
В каталоге примеров есть несколько небольших примеров, демонстрирующих возможности API.
В репозитории manticore-examples есть еще несколько сложных примеров, включая некоторые реальные проблемы с CTF.
Если вы хотите отправить отчет об ошибке или запросить новую функцию, воспользуйтесь нашей страницей проблем.
Если у вас есть вопросы и разъяснения, пожалуйста, посетите страницу обсуждения.
Мантикора лицензируется и распространяется по лицензии AGPLv3. Свяжитесь с нами, если вы ищете исключение из условий.
Если вы используете Мантикору в академической работе, подумайте о том, чтобы подать заявку на премию Crytic Research Prize в размере 10 тысяч долларов.
