manticore
Manticore 0.3.7
Este proyecto ya no se desarrolla ni se mantiene internamente. Sin embargo, nos complace revisar y aceptar solicitudes de extracción pequeñas y bien escritas por parte de la comunidad. Sólo consideraremos correcciones de errores y mejoras menores.
Cualquier problema o debate nuevo o actualmente abierto será respondido y apoyado por la comunidad.
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 manticoreOpción 2: Instalación desde PyPI, con dependencias adicionales necesarias para ejecutar archivos binarios nativos:
pip install " manticore[native] "Opción 3: instalar una compilación de desarrollo nocturno:
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: instalar a través de Docker:
docker pull trailofbits/manticore Una vez instalada, la herramienta CLI 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 contrato binario o inteligente. Los resultados del análisis se colocarán en un directorio del espacio de trabajo que comienza con mcore_ . Para obtener información sobre el espacio de trabajo, consulte la wiki.
Manticore CLI detecta automáticamente que está intentando probar un contrato si (por ejemplo) el contrato tiene una extensión .sol o .vy . Ver una demostración.
$ 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_gsncmlgxSe proporciona una herramienta CLI alternativa que simplifica las pruebas del contrato y permite escribir métodos de propiedades en el mismo lenguaje de alto nivel que utiliza el contrato. Consulte la documentación del verificador de mantícora. Ver una demostración
$ 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 proporciona una interfaz de programación Python que se puede utilizar para implementar potentes análisis personalizados.
Para los contratos inteligentes de Ethereum, la API se puede utilizar para una verificación detallada de propiedades de contratos arbitrarios. Los usuarios pueden establecer las condiciones iniciales, ejecutar transacciones simbólicas y luego revisar los estados descubiertos para garantizar invariantes para la retención 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 archivos binarios de Linux. Adaptar el estado inicial ayuda a evitar problemas de explosión de estado que ocurren comúnmente cuando se usa 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 a través de 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 su $PATH .crytic-compile directamente en su código para que sea más fácil identificar cualquier problema. Manticore se basa en un solucionador externo que admite smtlib2. Actualmente, Z3, Yices y CVC4 son compatibles y se pueden seleccionar mediante la línea de comandos o mediante ajustes de configuración. Si Yices está disponible, Manticore lo usará de forma predeterminada. De lo contrario, volverá a Z3 o CVC4. Si desea elegir manualmente qué solucionador usar, puede hacerlo así: manticore --smt.solver Z3
Para obtener más detalles, visite https://cvc4.github.io/. De lo contrario, simplemente obtenga el binario y úselo.
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 flojo #manticore en Empire Hacking para obtener ayuda para usar o ampliar Manticore.
La documentación está disponible en varios lugares:
La wiki contiene información sobre cómo comenzar con Manticore y cómo contribuir.
La referencia de API tiene documentación más completa y detallada sobre nuestra API.
El directorio de ejemplos tiene algunos pequeños ejemplos que muestran las características de la API.
El repositorio de ejemplos de mantícora tiene algunos ejemplos más complicados, incluidos algunos problemas reales de CTF.
Si desea presentar un informe de error o una solicitud de función, utilice nuestra página de problemas.
Si tiene preguntas y aclaraciones, visite la página de discusión.
Manticore tiene licencia y se distribuye bajo la licencia AGPLv3. Contáctenos si está buscando una excepción a los términos.
Si está utilizando Manticore en trabajos académicos, considere postularse al Premio de Investigación Crytic de $10k.
