Cómo usar Manticore para encontrar errores en contratos inteligentes

El objetivo de este tutorial es mostrar cómo se usa Manticore para encontrar errores automáticamente en los contratos inteligentes.

Instalación

Manticore requiere >= python 3.6. Se puede instalar a través de pip o usando Docker.

Manticore a través de Docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

El comando anterior ejecuta eth-security-toolbox en un Docker que tiene acceso a su directorio actual. Puede cambiar los archivos desde su host y ejecutar las herramientas en los archivos desde el Docker

Dentro de Docker, ejecute:

solc-select 0.5.11
cd /home/trufflecon/

Manticore a través de pip

pip3 install --user manticore

Se recomienda solc 0.5.11.

Ejecutar un script

Para ejecutar un script de Python con Python 3:

python3 script.py

Introducción a la ejecución simbólica dinámica

Ejecución simbólica dinámica en pocas palabras

La ejecución simbólica dinámica (DSE) es una técnica de análisis de programas que explora un espacio de estados con un alto grado de conciencia semántica. Esta técnica se basa en el descubrimiento de «rutas del programa», representadas como fórmulas matemáticas llamadas path predicates. Conceptualmente, esta técnica opera en predicados de ruta en dos pasos:

1. Se construyen usando restricciones en la entrada del programa.
2. Se usan para generar entradas de programa que harán que se ejecuten las rutas asociadas.

Este enfoque no produce falsos positivos, en el sentido de que todos los estados del programa identificados pueden activarse durante la ejecución concreta. Por ejemplo, si el análisis encuentra un desbordamiento de enteros, se garantiza que es reproducible.

Ejemplo de predicado de ruta

Para hacerse una idea de cómo funciona la DSE, considere el siguiente ejemplo:

1function f(uint a){
2
3  if (a == 65) {
4      // Hay un error
5  }
6
7}
Copiar

Como f() contiene dos rutas, una DSE construirá dos predicados de ruta diferentes:

• Ruta 1: a == 65
• Ruta 2: Not (a == 65)

Cada predicado de ruta es una fórmula matemática que puede darse a un llamado resolutor SMTopens in a new tab, que intentará resolver la ecuación. Para la Ruta 1, el resolutor dirá que la ruta se puede explorar con a = 65. Para la Ruta 2, el resolutor puede dar a a cualquier valor que no sea 65, por ejemplo, a = 0.

Verificación de propiedades

Manticore permite un control total sobre toda la ejecución de cada ruta. Como resultado, le permite añadir restricciones arbitrarias a casi cualquier cosa. Este control permite la creación de propiedades en el contrato.

Considere el siguiente ejemplo:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // sin protección contra desbordamientos
3  return c;
4}
Copiar

Aquí solo hay una ruta para explorar en la función:

• Ruta 1: c = a + b

Con Manticore, puede comprobar si hay desbordamiento y añadir restricciones al predicado de ruta:

• c = a + b AND (c < a OR c < b)

Si es posible encontrar una valoración de a y b para la cual el predicado de ruta anterior sea factible, significa que ha encontrado un desbordamiento. Por ejemplo, el resolutor puede generar la entrada a = 10, b = MAXUINT256.

Si considera una versión corregida:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
Copiar

La fórmula asociada con la comprobación de desbordamiento sería:

• c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

Esta fórmula no puede resolverse; en otras palabras, es una prueba de que en safe_add, c siempre aumentará.

Por lo tanto, la DSE es una potente herramienta que puede verificar restricciones arbitrarias en su código.

Ejecución en Manticore

Veremos cómo explorar un contrato inteligente con la API de Manticore. El objetivo es el siguiente contrato inteligente example.solopens in a new tab:

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
Mostrar todo
Copiar

Ejecutar una exploración independiente

Puede ejecutar Manticore directamente en el contrato inteligente con el siguiente comando (project puede ser un archivo de Solidity o un directorio de proyecto):

$ manticore project

Obtendrá una salida de casos de prueba como esta (el orden puede cambiar):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Mostrar todo

Sin información adicional, Manticore explorará el contrato con nuevas transacciones simbólicas hasta que ya no explore nuevas rutas en el contrato. Manticore no ejecuta nuevas transacciones después de una que falle (p. ej., después de una reversión).

Manticore enviará la información a un directorio mcore_*. Entre otras cosas, encontrará en este directorio:

• global.summary: cobertura y advertencias del compilador
• test_XXXXX.summary: cobertura, última instrucción, saldos de cuenta por caso de prueba
• test_XXXXX.tx: lista detallada de transacciones por caso de prueba

Aquí Manticore encuentra 7 casos de prueba, que corresponden a (el orden de los nombres de archivo puede cambiar):

Resumen de exploración: f(!=65) denota que se llamó a f con cualquier valor distinto de 65.

Como puede observar, Manticore genera un caso de prueba único para cada transacción exitosa o revertida.

Use el indicador --quick-mode si desea una exploración rápida del código (desactiva los detectores de errores, el cómputo de gas, etc.).

Manipular un contrato inteligente a través de la API

Esta sección describe los detalles para manipular un contrato inteligente a través de la API de Python de Manticore. Puede crear un nuevo archivo con la extensión de Python *.py y escribir el código necesario agregando los comandos de la API (cuyos fundamentos se describirán a continuación) en este archivo y luego ejecutarlo con el comando $ python3 *.py. También puede ejecutar los comandos siguientes directamente en la consola de Python; para ejecutar la consola, use el comando $ python3.

Creación de cuentas

Lo primero que debe hacer es iniciar una nueva cadena de bloques con los siguientes comandos:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Copiar

Se crea una cuenta que no es de contrato mediante m.create_accountopens in a new tab:

1user_account = m.create_account(balance=1000)
Copiar

Se puede desplegar un contrato de Solidity mediante m.solidity_create_contractopens in a new tab:

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Iniciar el contrato
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Mostrar todo
Copiar

Resumen

• Puede crear cuentas de usuario y de contrato con m.create_accountopens in a new tab y m.solidity_create_contractopens in a new tab.

Ejecución de transacciones

Manticore admite dos tipos de transacción:

• Transacción sin procesar: se exploran todas las funciones
• Transacción con nombre: solo se explora una función

Transacción sin procesar

Una transacción sin formato se ejecuta usando m.transactionopens in a new tab:

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
Copiar

El llamador, la dirección, los datos o el valor de la transacción pueden ser concretos o simbólicos:

• m.make_symbolic_valueopens in a new tab crea un valor simbólico.
• m.make_symbolic_buffer(size)opens in a new tab crea una matriz de bytes simbólica.

Por ejemplo:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
Copiar

Si los datos son simbólicos, Manticore explorará todas las funciones del contrato durante la ejecución de la transacción. Será útil ver la explicación de la función fallback en el artículo Hands on the Ethernaut CTFopens in a new tab para comprender cómo funciona la selección de funciones.

Transacción con nombre

Las funciones pueden ejecutarse a través de su nombre. Para ejecutar f(uint var) con un valor simbólico, desde user_account y con 0 ether, use:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
Copiar

Si el valor de la transacción no se especifica, es 0 por defecto.

Resumen

• Los argumentos de una transacción pueden ser concretos o simbólicos
• Una transacción sin formato explorará todas las funciones
• La función puede ser llamada por su nombre

Espacio de trabajo

m.workspace es el directorio utilizado como directorio de salida para todos los archivos generados:

1print("Results are in {}".format(m.workspace))
Copiar

Finalizar la exploración

Para detener la exploración, use m.finalize()opens in a new tab. No se deben enviar más transacciones cuando se llama a este método, y Manticore genera casos de prueba para cada una de las rutas exploradas.

Resumen: Ejecución en Manticore

Reuniendo los pasos previos, obtenemos:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # detener la exploración
Mostrar todo
Copiar

Puede encontrar todo el código anterior en example_run.pyopens in a new tab

Obtención de las rutas que fallan

Ahora generaremos entradas específicas para las rutas que generan una excepción en f(). El objetivo es el siguiente contrato inteligente example.solopens in a new tab:

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Copiar

Uso de la información de estado

Cada ruta ejecutada tiene su estado de la cadena de bloques. Un estado está listo o está terminado, lo que significa que llega a una instrucción THROW o REVERT:

• m.ready_statesopens in a new tab: la lista de estados que están listos (no ejecutaron una REVERT/INVALID)
• m.killed_statesopens in a new tab: la lista de estados que están terminados
• m.all_statesopens in a new tab: todos los estados

1for state in m.all_states:
2    # hacer algo con el estado
Copiar

Puede acceder a la información de estado. Por ejemplo:

• state.platform.get_balance(account.address): el saldo de la cuenta
• state.platform.transactions: la lista de transacciones
• state.platform.transactions[-1].return_data: los datos devueltos por la última transacción

Los datos devueltos por la última transacción son una matriz, que se puede convertir en un valor con ABI.deserialize, por ejemplo:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
Copiar

Cómo generar un caso de prueba

Use m.generate_testcase(state, name)opens in a new tab para generar el caso de prueba:

1m.generate_testcase(state, 'BugFound')
Copiar

Resumen

• Puede iterar sobre el estado con m.all_states
• state.platform.get_balance(account.address) devuelve el saldo de la cuenta
• state.platform.transactions devuelve la lista de transacciones
• transaction.return_data son los datos devueltos
• m.generate_testcase(state, name) genera entradas para el estado

Resumen: Obtención de la ruta de lanzamiento

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Comprobar si una ejecución finaliza con REVERT o INVALID
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Throw found {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Mostrar todo
Copiar

Puede encontrar todo el código anterior en example_run.pyopens in a new tab

Tenga en cuenta que podríamos haber generado un script mucho más simple, ya que todos los estados devueltos por terminated_states tienen REVERT o INVALID en su resultado: este ejemplo solo tenía la intención de demostrar cómo manipular la API.

Adición de restricciones

Veremos cómo restringir la exploración. Asumiremos que la documentación de f() establece que la función nunca se llama con a == 65, por lo que cualquier error con a == 65 no es un error real. El objetivo es el siguiente contrato inteligente example.solopens in a new tab:

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Copiar

Operadores

El módulo Operatorsopens in a new tab facilita la manipulación de restricciones; entre otros, proporciona:

• Operators.AND,
• Operators.OR,
• Operators.UGT (mayor que sin signo),
• Operators.UGE (mayor o igual que sin signo),
• Operators.ULT (menor que sin signo),
• Operators.ULE (menor o igual que sin signo).

Para importar el módulo, use lo siguiente:

1from manticore.core.smtlib import Operators
Copiar

Operators.CONCAT se usa para concatenar una matriz a un valor. Por ejemplo, el return_data de una transacción necesita cambiarse a un valor para ser comprobado contra otro valor:

1last_return = Operators.CONCAT(256, *last_return)
Copiar

Restricciones

Puede usar restricciones globalmente o para un estado específico.

Restricción global

Use m.constrain(constraint) para agregar una restricción global. Por ejemplo, puede llamar a un contrato desde una dirección simbólica y restringir esta dirección a valores específicos:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
Copiar

Restricción de estado

Use state.constrain(constraint)opens in a new tab para añadir una restricción a un estado específico. Se puede usar para restringir el estado después de su exploración para comprobar alguna propiedad en él.

Comprobación de restricciones

Use solver.check(state.constraints) para saber si una restricción sigue siendo factible. Por ejemplo, lo siguiente restringirá symbolic_value para que sea diferente de 65 y comprobará si el estado sigue siendo factible:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # el estado es factible
Copiar

Resumen: Adición de restricciones

Al añadir una restricción al código anterior, se obtiene:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Comprobar si una ejecución finaliza con REVERT o INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # no consideramos la ruta donde a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Error encontrado, los resultados están en {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'No se encontró ningún error')
Mostrar todo
Copiar

Puede encontrar todo el código anterior en example_run.pyopens in a new tab

Última actualización de la página: 26 de abril de 2024

lopens in a new tab

nopens in a new tab

ropens in a new tab

+5

Ver colaboradores