trailofbits/manticoreFerramenta de execução simbólica
Este projeto não é mais desenvolvido e mantido internamente.
Manticore é uma ferramenta de execução simbólica para análise de contratos inteligentes e binários.
Manticore pode analisar os seguintes tipos de programas:
Nota: Recomendamos instalar o Manticore em um ambiente virtual para evitar conflitos com outros projetos ou pacotes
Opção 1: Instalando a partir do PyPI:
pip install manticore
Opção 2: Instalando a partir do PyPI, com dependências extras necessárias para executar binários nativos:
pip install "manticore[native]"
Opção 3: Instalando uma versão de desenvolvimento nightly:
pip install --pre "manticore[native]"
Opção 4: Instalando a partir do branch master:
git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"
Opção 5: Instalar via Docker:
docker pull trailofbits/manticore
Uma vez instalado, a ferramenta CLI manticore e a API Python estarão disponíveis.
Para uma instalação de desenvolvimento, veja nossa wiki.
Manticore possui uma interface de linha de comando que pode realizar uma análise simbólica básica de um binário ou contrato inteligente.
Os resultados da análise serão colocados em um diretório de workspace começando com mcore_. Para informações sobre o workspace, veja a wiki.
A CLI do Manticore detecta automaticamente que você está tentando testar um contrato se (por ex.)
o contrato tiver uma extensão .sol ou .vy. Veja uma demo.
$ 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
Uma ferramenta CLI alternativa é fornecida que simplifica o teste de contratos e permite escrever métodos de propriedades na mesma linguagem de alto nível que o contrato usa. Confira a documentação do manticore-verifier. Veja uma demo
$ 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 fornece uma interface de programação Python que pode ser usada para implementar análises personalizadas poderosas.
Para contratos inteligentes Ethereum, a API pode ser usada para verificação detalhada de propriedades arbitrárias do contrato. Os usuários podem definir as condições iniciais, executar transações simbólicas e então revisar os estados descobertos para garantir que invariantes de um contrato sejam mantidos.
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)))
Também é possível usar a API para criar ferramentas de análise personalizadas para binários Linux. Personalizar o estado inicial ajuda a evitar problemas de explosão de estados que comumente ocorrem ao usar a 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 também pode avaliar funções WebAssembly sobre entradas simbólicas para validação de propriedades ou análise geral.
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 ou passando --ulimit stack=100000000:100000000 para docker runsolc em seu $PATH.crytic-compile diretamente em seu código para facilitar a identificação de quaisquer problemas.Manticore depende de um solver externo compatível com smtlib2. Atualmente Z3, Yices e CVC4 são suportados e podem ser selecionados via linha de comando ou configurações.
Se Yices estiver disponível, Manticore o usará por padrão. Caso contrário, ele usará Z3 ou CVC4. Se você quiser escolher manualmente qual solver usar, pode fazer assim:
manticore --smt.solver Z3
Para mais detalhes, acesse https://cvc4.github.io/. Caso contrário, apenas obtenha o binário e use-o.
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 é incrivelmente rápido. Mais detalhes aqui https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
Sinta-se à vontade para visitar nosso canal #manticore no Slack do Empire Hacking para ajuda com o uso ou extensão do Manticore.
A documentação está disponível em vários lugares:
A wiki contém informações sobre como começar com o Manticore e contribuir
A referência da API possui documentação mais completa e aprofundada sobre nossa API
O diretório examples possui alguns exemplos pequenos que mostram recursos da API
O repositório manticore-examples possui alguns exemplos mais complexos, incluindo problemas reais de CTF
Se você gostaria de registrar um relatório de bug ou solicitação de recurso, por favor, use nossa página de issues.
Para perguntas e esclarecimentos, visite a página de discussão.
Manticore é licenciado e distribuído sob a licença AGPLv3. Contate-nos se você estiver procurando por uma exceção aos termos.
Se você está usando Manticore em trabalho acadêmico, considere se candidatar ao Prêmio de Pesquisa Crytic de $10k.
