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

Dentro del 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.

Ejecución de un script

Para ejecutar un script de 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; // no overflow protection
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 por consiguiente una potente herramienta que puede verificar restricciones arbitrarias en el código.

Ejecutar con Manticore

Veamos cómo explorar un contrato inteligente con la API de Manticore. El objetivo es el siguiente contrato inteligente 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

Ejecutar una exploración independiente

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

$ manticore project

Obtendrá la salida o resultado de casos de prueba como este (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 no explore nuevas rutas en el contrato. Manticore no ejecuta 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 otras cosas, encontrará en este directorio:

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

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

Resumen de exploración f(!=65) muestra que f llamó 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, 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 (los aspectos básicos 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 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 sin contrato con m.create_account(opens in a new tab):

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

Se puede implementar un contrato de Solidity 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

• Puede 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.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## Check if an execution ends with a REVERT or INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, '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 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

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:

1from manticore.core.smtlib import Operators
 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 = Operators.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.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 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.constraints):
3    # state is feasible
 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.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## Check if an execution ends with a REVERT or INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # we do not consider the path were a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
Mostrar todo
 Copiar

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