⚠️ Project is archived ⚠️

Este proyecto ya no se desarrolla ni mantiene internamente.

Manticore

Manticore es una herramienta de ejecución simbólica para el análisis de contratos inteligentes y binarios.

Características

• Exploración de programas: Manticore puede ejecutar un programa con entradas simbólicas y explorar todos los estados posibles que puede alcanzar
• Generación de entradas: Manticore puede producir automáticamente entradas concretas que resulten en un estado de programa dado
• Descubrimiento de errores: Manticore puede detectar caídas y otros casos de fallo en binarios y contratos inteligentes
• Instrumentación: Manticore proporciona un control detallado de la exploración de estados mediante callbacks de eventos y hooks de instrucciones
• Interfaz programática: Manticore expone acceso programático a su motor de análisis a través de una API de Python

Manticore puede analizar los siguientes tipos de programas:

• Contratos inteligentes de Ethereum (bytecode EVM)
• Binarios ELF de Linux (x86, x86_64, aarch64 y ARMv7)
• Módulos WASM

Instalación

Nota: Recomendamos instalar Manticore en un entorno virtual para evitar conflictos con otros proyectos o paquetes

Opción 1: Instalación desde PyPI:

pip install manticore

Opción 2: Instalación desde PyPI, con dependencias adicionales necesarias para ejecutar binarios nativos:

pip install "manticore[native]"

Opción 3: Instalación de una compilación de desarrollo nocturna:

pip install --pre "manticore[native]"

Opción 4: Instalación desde la rama master:

git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"

Opción 5: Instalación mediante Docker:

docker pull trailofbits/manticore

Una vez instalado, la herramienta CLI de manticore y la API de Python estarán disponibles.

Para una instalación de desarrollo, consulte nuestra wiki.

Uso

CLI

Manticore tiene una interfaz de línea de comandos que puede realizar un análisis simbólico básico de un binario o contrato inteligente. Los resultados del análisis se colocarán en un directorio de espacio de trabajo que comienza con mcore_. Para obtener información sobre el espacio de trabajo, consulte la wiki.

EVM

La CLI de Manticore detecta automáticamente que estás intentando probar un contrato si (por ejemplo) el contrato tiene una extensión .sol o .vy. Vea una 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

Se proporciona una herramienta CLI alternativa que simplifica las pruebas de contratos y permite escribir métodos de propiedades en el mismo lenguaje de alto nivel que utiliza el contrato. Consulte la documentación de manticore-verifier. Vea una 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 proporciona una interfaz de programación Python que se puede utilizar para implementar potentes análisis personalizados.

EVM

Para contratos inteligentes de Ethereum, la API se puede utilizar para la verificación detallada de propiedades arbitrarias del contrato. Los usuarios pueden establecer las condiciones iniciales, ejecutar transacciones simbólicas y luego revisar los estados descubiertos para asegurar que se mantengan los invariantes de un 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)))

Nativo

También es posible utilizar la API para crear herramientas de análisis personalizadas para binarios de Linux. Ajustar el estado inicial ayuda a evitar los problemas de explosión de estados que ocurren comúnmente al usar la 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 también puede evaluar funciones de WebAssembly sobre entradas simbólicas para validación de propiedades o análisis general.

from manticore.wasm import ManticoreWASM

m = ManticoreWASM("collatz.wasm")