manticore
Manticore 0.3.7
Este projeto não é mais desenvolvido e mantido internamente. No entanto, teremos prazer em analisar e aceitar solicitações pull pequenas e bem escritas da comunidade. Consideraremos apenas correções de bugs e pequenas melhorias.
Quaisquer questões e discussões novas ou atualmente abertas serão respondidas e apoiadas pela comunidade.
Manticore é uma ferramenta de execução simbólica para análise de contratos inteligentes e binários.
A 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: instalação do PyPI:
pip install manticoreOpção 2: Instalação a partir do PyPI, com dependências extras necessárias para executar binários nativos:
pip install " manticore[native] "Opção 3: Instalando uma compilação de desenvolvimento noturna:
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 Depois de instalada, a ferramenta CLI manticore e a API Python estarão disponíveis.
Para uma instalação de desenvolvimento, consulte nosso wiki.
Manticore possui uma interface de linha de comando que pode realizar uma análise simbólica básica de um contrato binário ou inteligente. Os resultados da análise serão colocados em um diretório de espaço de trabalho começando com mcore_ . Para obter informações sobre o espaço de trabalho, consulte o wiki.
O Manticore CLI detecta automaticamente que você está tentando testar um contrato se (por exemplo) o contrato tiver uma extensão .sol ou .vy . Veja uma demonstração.
$ 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É fornecida uma ferramenta CLI alternativa que simplifica o teste do contrato e permite escrever métodos de propriedades na mesma linguagem de alto nível que o contrato usa. Confira a documentação do verificador de manticore. Veja uma demonstração
$ 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 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 de contratos. Os usuários podem definir as condições iniciais, executar transações simbólicas e, em seguida, revisar os estados descobertos para garantir invariantes para a suspensão de um contrato.
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 customizadas para binários Linux. Adaptar o estado inicial ajuda a evitar problemas de explosão de estado que normalmente 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 ()A Manticore também pode avaliar funções WebAssembly em 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 no seu código para facilitar a identificação de quaisquer problemas. Manticore depende de um solucionador externo que suporta smtlib2. Atualmente Z3, Yices e CVC4 são suportados e podem ser selecionados via linha de comando ou definições de configuração. Se o Yices estiver disponível, a Manticore o usará por padrão. Caso contrário, voltará para Z3 ou CVC4. Se quiser escolher manualmente qual solucionador usar, você pode fazer assim: manticore --smt.solver Z3
Para mais detalhes acesse https://cvc4.github.io/. Caso contrário, basta pegar o binário e usá-lo.
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 no Empire Hacking para obter ajuda para usar ou estender o Manticore.
A documentação está disponível em vários locais:
O wiki contém informações sobre como começar a usar o Manticore e contribuir
A referência da API possui documentação mais completa e aprofundada sobre nossa API
O diretório de exemplos contém alguns pequenos exemplos que mostram os recursos da API
O repositório manticore-examples tem alguns exemplos mais complicados, incluindo alguns problemas reais de CTF
Se desejar enviar um relatório de bug ou solicitação de recurso, use nossa página de problemas.
Para dúvidas e esclarecimentos, visite a página de discussão.
Manticore é licenciado e distribuído sob a licença AGPLv3. Entre em contato conosco se estiver procurando uma exceção aos termos.
Se você estiver usando o Manticore em trabalhos acadêmicos, considere se inscrever no Crytic $ 10k Research Prize.
