trailofbits/manticoreHerramienta de ejecución simbólica
Este proyecto ya no se desarrolla ni mantiene internamente.
Manticore es una herramienta de ejecución simbólica para el análisis de contratos inteligentes y binarios.
Manticore puede analizar los siguientes tipos de programas:
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.
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.
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
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
$ 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 proporciona una interfaz de programación Python que se puede utilizar para implementar potentes análisis personalizados.
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)))
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()
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")
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 o pasando --ulimit stack=100000000:100000000 a docker runsolc en tu $PATH.crytic-compile directamente sobre tu código para facilitar la identificación de cualquier problema.Manticore depende de un solucionador externo que admita smtlib2. Actualmente, Z3, Yices y CVC4 son compatibles y se pueden seleccionar mediante la línea de comandos o la configuración. Si Yices está disponible, Manticore lo usará por defecto. Si no, recurrirá a Z3 o CVC4. Si deseas elegir manualmente qué solucionador usar, puedes hacerlo así:
manticore --smt.solver Z3
Para más detalles, visite https://cvc4.github.io/. De lo contrario, simplemente obtenga el binario y utilícelo.
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 es increíblemente rápido. Más detalles aquí https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
No dudes en pasar por nuestro canal de slack #manticore en Empire Hacking para obtener ayuda sobre cómo usar o extender Manticore.
La documentación está disponible en varios lugares:
La wiki contiene información sobre cómo empezar con Manticore y contribuir
La referencia de la API tiene documentación más exhaustiva y detallada sobre nuestra API
El directorio examples tiene algunos ejemplos pequeños que muestran las características de la API
El repositorio manticore-examples tiene algunos ejemplos más complejos, incluyendo algunos problemas reales de CTF
Si deseas informar un error o solicitar una función, utiliza nuestra página de issues.
Para preguntas y aclaraciones, visita la página de discusión.
Manticore está licenciado y distribuido bajo la licencia AGPLv3. Contáctenos si busca una excepción a los términos.
Si estás usando Manticore en trabajos académicos, considera postularte al Crytic $10k Research Prize.
