Cómo usar Manticore para encontrar errores en contratos inteligentes

soliditycontratos Inteligentesseguridadespruebasverificación formal

Advanced

Trailofbits

Desarrollando smart contracts(opens in a new tab)

13 de enero de 2020

12 minuto leído minute read

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 de arriba ejecuta eth-security-toolbox en un docker que tiene acceso a tu directorio actual. Puedes cambiar los archivos desde tu host y correr las herramientas dentro de los archivos desde docker

Al estar en el 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.

Ejecutando un script

Ejecutando un script python con python 3:

python3 script.py

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

Descripción breve de la ejecución simbólica dinámica

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 con fórmulas matemáticas denominadas path predicates. Conceptualmente, esta técnica opera en predicados de ruta en dos pasos:

1. Contruyéndolos con restricciones sobre la entrada del programa.
2. Usándolos para generar entradas del programa para ejecutar las rutas asociadas.

Este enfoque previene falsos positivos porque todos los estados de programa identificados se pueden activar durante la ejecución concreta. Por ejemplo, si el análisis encuentra un desbordamiento de enteros, se garantiza que sea reproducible.

Ejemplo de predicado de ruta

Para conocer el funcionamiento de la DSE, considere el siguiente ejemplo:

1function f(uint a){
2
3  if (a == 65) {
4      // A bug is present
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 ser dada a un resolutor de SMT(opens in a new tab), que intentará resolver la ecuación. En Path 1, el resolutor dirá que la ruta puede ser explorada con a = 65. En Path 2, el resolutor puede dar a a cualquier valor distinto de 65, por ejemplo, a = 0.

Verificación de propiedades

Manticore permite control pleno sobre toda la ejecución de cada ruta. Como resultado, 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 de desbordamiento
3  return c;
4}
 Copiar

Aquí solo hay un camino para explorar en la función:

• Ruta 1: c = a + b

Usando Manticore se 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 un valor de a y b donde el predicado de ruta de arriba sea factible, significa que se ha encontrado un desbordamiento. Por ejemplo, el solucionador 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 se puede resolver; en otro estadio esto es una prueba de que en safe_add, c siempre aumentará.

DSE es una potente herramienta que puede verificar restricciones arbitrarias en el código.

Ejecutando bajo Mantícora

Veamos cómo explorar un contrato inteligente con la API Manticore. El objetivo es el siguiente smart contract example.sol(opens 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

Ejecute una exploración independiente

Ejecute Manticore directamente en el contrato inteligente con el siguiente comando (project que puede ser un Solidity File o un roject directory):

$ 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...
Mostrar todo

Sin información adicional, Manticore va a explorar el contrato con nuevas transacciones simbólicas hasta que no haya nuevas rutas en el contrato. Manticore no ejecutará nuevas transacciones después de una fallida (por ejemplo: después de una reversión).

Manticore mostrará la información en un directorio mcore_*. Entre otros, encontrará en este directorio:

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

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

Resumen de exploración f(!=65) muestra f llamada con cualquier valor diferente a 65.

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

Use la marca --quick-mode si desea una exploración rápida de código (deshabilita los detectores de errores, el cálculo de gas, ...)

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 Manticore Python. Se puede crear un nuevo archivo con la extensión python *.py y escribir el código necesario agregando los comandos API (los básicos que se describen a continuación) en este archivo y luego ejecutarlo con el comando $ python3 *.py. También puede ejecutar los siguientes comandos directamente en la consola python, ejecutando el comando $ python3.

Creación de cuentas

Lo primero es iniciar un nuevo blockchain con los siguientes comandos:

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

Se crea una cuenta sin contrato con m.create_account(opens in a new tab):

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

Se despliega un Solidity contract usando m.solidity_create_contract(opens 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# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Mostrar todo
 Copiar

Resumen

• Puedes crear cuentas de usuario y contratos con m.create_account(opens in a new tab) y m.solidity_create_contract(opens in a new tab).

Ejecución de transacciones

Manticore admite dos tipos de transacción:

• Transacción en bruto (raw): se exploran todas las funciones
• Transacción con nombre: solo se explora una función

Transacción en bruto

La transacción en bruto se ejecuta usando m.transaction(opens in a new tab):

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

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

• m.make_symbolic_value(opens in a new tab) crea un valor simbólico.
• m.make_symbolic_buffer(size)(opens in a new tab) crea un array de bytes simbólico.

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. Es útil ver la explicación de la función Fallback en el artículo Hands on the Ethernaut CTF(opens in a new tab) para entender 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, de 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 value 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 en bruto explorará todas las funciones
• La función puede ser llamada por su nombre

Workspace

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

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

Terminar 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: ejecutar con 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() # stop the exploration
Mostrar todo
 Copiar

Todo el código de arriba que encuentra en example_run.py(opens in a new tab)

Obtener throwing paths

Ahora generaremos entradas específicas para las rutas que plantean una excepción en f(). El objetivo sigue siendo el contrato inteligente example.sol(opens 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 información de estado

Cada ruta ejecutada tiene un estado en la cadena de bloques. Un estado está listo o es aniquilado, lo que significa que alcanza una instrucción THROW o REVERT:

• m.ready_states(opens in a new tab): la lista de estados que están listos (no ejecutaron un REVERT/INVALID)
• m.killed_states(opens in a new tab): lista de estados aniquilados
• m.all_states(opens in a new tab): todos los estados

1for state in m.all_states:
2    # do something with state
 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 un array que puede convertirse en un valor con ABI.deserialize, por ejemplo:

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

Cómo generar testcase

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

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

Resumen

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

Resumen: obtener Throwing Path

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

Todo el código anterior que puede encontrar en el example_run.py(opens in a new tab)

Note que podríamos haber generado un script mucho más simple, ya que todos los estados devueltos por terminated_state tienen REVERT o INVALID en su resultado: este ejemplo solo estaba destinado a demostrar cómo manipular la API.

Adición de restricciones

Veremos cómo restringir la exploración. Supondremos que la documentación de f() indica que la función nunca es llamada con a == 65, así que cualquier error con a == 65 no es un error real. El objetivo sigue siendo este contrato inteligente example.sol(opens 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 sobre Operadores(opens in a new tab) facilita la manipulación de restricciones y provee, entre otras cosas:

• Operators.AND,
• Operators.OR,
• Operators.UGT (sin firma mayores que),
• Operators.UGE (sin firma mayores que o iguales a),
• Operators.ULT (sin firma menores que),
• Operators.ULE (sin firma menores o iguales a).

Para importar el módulo, use:

1operadores de importación desde manticore.core.smtlib
 Copiar

Operators.CONCAT se usa para concatenar un array 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 = Operadors.CONCAT(256, *last_return)
 Copiar

Restricciones

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

Restricción global

Use m.constran(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 para que sean valores específicos:

1symbolic_address = m.make_symbolic_value()
2m.restricint(Operators.OR(simbólico == 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 verificar alguna propiedad en él.

Restricción de verificación

Use solver.check(state.restricints) para saber si una restricción todavía es viable. Por ejemplo, esto restringirá symbolic_value para que sea diferente de 65 y comprobará si el estado es todavía viable:

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

Resumen: adición de restricciones

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

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver. nstance()
5
6m = ManticoreEVM()
7
8con open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m. reate_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m. ake_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Comprueba si una ejecución termina con un REVERT o un INVALID
20para el estado en m. erminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx. esult en ['REVERT', 'INVALID']:
23        # no consideramos que la ruta sea un == 65
24        condición = symbolic_var ! 65
25        si m. enerate_testcase(state, name="BugFound", only_if=condition):
26            print(f'error encontrado, los resultados están en {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No se encontró error')
Mostrar todo
 Copiar

Todo el código anterior que se puede encontrar en example_run.py(opens in a new tab)