⚠️ Projeto arquivado ⚠️

Este projeto não é mais desenvolvido e mantido internamente.

Manticore

Manticore é uma ferramenta de execução simbólica para análise de contratos inteligentes e binários.

Recursos

• Exploração de Programas: Manticore pode executar um programa com entradas simbólicas e explorar todos os estados possíveis que pode alcançar
• Geração de Entradas: Manticore pode produzir automaticamente entradas concretas que resultam em um estado de programa específico
• Descoberta de Erros: Manticore pode detectar falhas e outros casos de erro em binários e contratos inteligentes
• Instrumentação: Manticore fornece controle refinado da exploração de estados por meio de callbacks de eventos e hooks de instrução
• Interface Programática: Manticore expõe acesso programático ao seu mecanismo de análise via uma API Python

Manticore pode analisar os seguintes tipos de programas:

• Contratos inteligentes Ethereum (bytecode EVM)
• Binários ELF Linux (x86, x86_64, aarch64 e ARMv7)
• Módulos WASM

Instalação

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.

Uso

CLI

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.

EVM

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

Manticore-verifier

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

Nativo

$ 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 fornece uma interface de programação Python que pode ser usada para implementar análises personalizadas poderosas.

EVM

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

Nativo

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

WASM

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