Cómo utilizar Echidna para probar contratos inteligentes

Instalación

Echidna se puede instalar a través de docker o por medio del binario precompilado.

Echidna 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

Dentro de docker, ejecuta:

solc-select 0.5.11
cd /home/training

Binario

https://github.com/crytic/echidna/releases/tag/v1.4.0.0(opens in a new tab)

Introducción a las auditorías de seguridad basadas en propiedades

Echidna es un auditor basado en propiedades, está descrito en nuestros blogposts anteriores (1(opens in a new tab), 2(opens in a new tab), 3(opens in a new tab)).

Fuzzing (auditoría de seguridad)

Fuzzing(opens in a new tab) es una técnica conocida en la comunidad de la seguridad. Esta consiste en la generación de entradas que son más o menos aleatorias para encontrar errores en el programa. Se sabe que software tradicional (como AFL(opens in a new tab) o LibFuzzer(opens in a new tab)) son herramientas eficientes para encontrar errores.

Más allá de la generación de insumos aleatorios, existen muchas técnicas y estrategias para generar insumos validos, que incluyen:

• Obtener retroalimentación de cada ejecución y generación de guías usándola. Por ejemplo, si una entrada recién generada conduce al descubrimiento de una nueva ruta, puede tener sentido generar nuevas entradas más cercanas a ella.
• Generando la entrada respetando una restricción estructural. Por ejemplo, si su entrada contiene un encabezado con una suma de control, tendrá sentido dejar que el fuzzer genere una entrada que valide la suma de control.
• Uso de entradas conocidas para generar nuevas entradas: si tienes acceso a un gran conjunto de datos de entrada válida, tu fuzzer puede generar nuevas entradas a partir de ellos, en lugar de comenzar la generación desde cero. Estas se conocen usualmente como seeds.

Fuzzing basado en propiedades

Echidna pertenece a una familia específica de fuzzer: fuzzing basado en propiedades inspiradas en QuickCheck(opens in a new tab). En contraste a un fuzzer de legado que intentará encontrar bloqueos, Echidna intentará romper invariantes definidas por el usuario.

En smart contracts, las invariantes son funciones de Solidity, que pueden representar cualquier estado incorrecto o inválido al que el contrato pueda llegar, incluyendo:

• Control de acceso erróneo: el atacante se convierte en el propietario del contrato.
• Estado de máquina incorrecto: fichas pueden ser transferidas mientras el contrato está en pausa.
• Aritmética incorrecta: el usuario puede rebasar su saldo y obtener fichas gratis ilimitadas.

Probando una propiedad con Echidna

Veremos cómo probar un smart contract con Echidna. El objetivo es el siguiente smart contract token.sol(opens in a new tab):

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
Mostrar todo
 Copiar

Supondremos que esta ficha debe tener las siguientes propiedades:

• Cualquier persona puede tener como máximo 1000 fichas
• La ficha no puede ser transferida (no es una ficha ERC20)

Escribe una propiedad

Las propiedades de Echidna son funciones de Solidity. Una propiedad debe:

• No tener ningún argumento
• Devolver true si es exitosa
• Que su nombre comience con echidna

Echidna va a:

• Automáticamente generar transacciones arbitrarias para probar la propiedad.
• Reportar cualquier transacción que lleve a una propiedad a devolver false o arrojar un error.
• Descartar efectos secundarios al llamar a una propiedad (es decir, si la propiedad cambia una variable de estado, se descarta después de la prueba)

La siguiente propiedad comprueba que el llamador no tenga más de 1000 fichas:

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}
 Copiar

Usa herencia para separar tu contrato de tus propiedades:

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }
 Copiar

token.sol(opens in a new tab) implementa la propiedad y hereda de la ficha.

Inicia un contrato

Echidna necesita un constructor sin argumento. Si tu contrato necesita una inicialización específica, debes hacerlo en el constructor.

Hay algunas direcciones específicas en Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 la cual llama al constructor.
• 0x10000, 0x20000, y 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 que llama de forma aleatoria a las otras funciones.

No necesitamos ninguna inicialización en particular en nuestro ejemplo actual, como resultado, nuestro constructor está vacío.

Ejecuta Echidna

Echidna se inicial con:

echidna-test contract.sol

Si contract.sol contiene varios contratos, puedes especificar el objetivo:

echidna-test contract.sol --contract MyContract

Resumen: Probando una propiedad

A continuación se resume la ejecución de echidna en nuestro ejemplo:

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }
 Copiar

echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
Mostrar todo

Echidna descubrió que la propiedad se viola si se llama a backdoor.

Filtrado de funciones para llamar durante una campaña fuzzing

Veremos cómo filtrar las funciones a ser "fuzzed". El objetivo es el siguiente smart contract:

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
Mostrar todo
 Copiar

Este pequeño ejemplo obliga a Echidna a encontrar una secuencia determinada de transacciones para cambiar una variable de estado. Esto es difícil para un fuzzer (se recomienda utilizar una herramienta de ejecución simbólica como Manticore(opens in a new tab)). Podemos ejecutar Echidna para verificar esto:

echidna-test multi.sol
...
echidna_state4: passed! 🎉
Seed: -3684648582249875403

Filtrando funciones

Echidna tiene problemas para encontrar la secuencia correcta para probar este contrato porque las dos funciones de reinicio (reset1 y reset2) establecerán todas las variables de estado a false. Sin embargo, podemos usar una función especial de Echidna para crear un blacklist de la función de reinicio o para crear un whitelist con las funciones f, g, h y i.

Para incluir funciones en la blacklist, podemos usar este archivo de configuración:

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

Otro enfoque para filtrar funciones es enumerar las funciones incluidas en la whitelist. Para ello, podemos utilizar este archivo de configuración:

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]

• filterBlacklist es true de forma predeterminada.
• El filtrado se realizará únicamente por nombre (sin parámetros). Si tienes f() y f(uint256), el filtro "f" coincidirá con ambas funciones.

Ejecuta Echidna

Para ejecutar Echidna con un archivo de configuración blacklist.yaml:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

Echidna encontrará la secuencia de transacciones para falsificar la propiedad casi de inmediato.

Resumen: Filtrando funciones

Echidna puede incluir funciones en una blacklist o una whitelist para llamar durante una campaña de fuzzing utilizando:

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]

echidna-test contract.sol --config config.yaml
...

Echidna comienza una campaña de fuzzing, ya sea "blacklisting" f1, f2 y f3 o solo los llama, según al valor del booleano (tipo de dato lógico) filterBlacklist.

Cómo probar la afirmación de Solidity con Echidna

En este breve tutorial, mostraremos cómo usar Echidna para probar la verificación de afirmaciones en contratos. Supongamos que tenemos un contrato como este:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
Mostrar todo
 Copiar

Escribe una afirmación

Queremos asegurarnos de que tmp sea menor o igual que counter después de devolver su diferencia. Podríamos escribir una propiedad de Echidna, pero tendremos que almacenar el valor tmp en algún lugar. En su lugar, podríamos usar una afirmación como esta:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Mostrar todo
 Copiar

Ejecuta Echidna

Para habilitar la prueba de fracaso de la afirmación, crea un archivo de configuración de Echidna(opens in a new tab) config.yaml:

1checkAsserts: true

Al ejecutar este contrato en Echidna obtenemos los resultados esperados:

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Mostrar todo

Como puedes ver, Echidna informa de un error de afirmación en la función inc. Es posible agregar más de una afirmación por función, pero Echidna no puede distinguir cual afirmación falló.

Cómo y cuándo utilizar afirmaciones

Las afirmaciones pueden usarse como alternativas a propiedades explícitas, especialmente si las condiciones a verificar están directamente relacionadas con el uso correcto de alguna operación f. Agregar afirmaciones luego de un poco de código hará que la verificación suceda inmediatamente después de la ejecución:

1function f(..) public {
2    // some complex code
3    ...
4    assert (condition);
5    ...
6}
7
 Copiar

Por el contrario, el uso de una propiedad explícita de echidna ejecutará transacciones de forma aleatoria y no hay una manera fácil de asegurar exactamente cuándo esta se comprobará. Es posible utilizar esta alternativa:

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}
 Copiar

Sin embargo, existen algunos problemas:

• Falla si f se declara como internal o external.
• No está claro qué argumentos deben usarse para llamar a f.
• Si f se revierte, la propiedad fallará.

En general, recomendamos seguir la recomendación de John Regehr(opens in a new tab) sobre cómo utilizar las afirmaciones:

• No forces ningún efecto secundario durante la verificación de afirmaciones. Por ejemplo: assert(ChangeStateAndReturn() == 1)
• No hagas afirmaciones obvias. Por ejemplo assert(var >= 0) donde var es declarado como uint.

Por último, no utilices require en lugar de assert, ya que Echidna no podrá detectarlo (pero el contrato se revertirá de todos modos).

Resumen: verificación de afirmaciones

A continuación, se resume la ejecución de echidna en nuestro ejemplo:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Mostrar todo
 Copiar

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Mostrar todo

Echidna descubrió que la aserción en inc puede fallar si se llama a esta función varias veces con argumentos grandes.

Recolectar y modificar un corpus de Echidna

Veremos cómo recopilar y utilizar un corpus de transacciones con Echidna. El objetivo es el siguiente smart contract magic.sol(opens in a new tab):

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
Mostrar todo
 Copiar

El ejemplo a continuación obliga a Echidna a encontrar ciertos valores para cambiar una variable de estado. Esto es difícil para un fuzzer (se recomienda utilizar una herramienta de ejecución simbólica como Manticore(opens in a new tab)). Podemos ejecutar Echidna para verificar esto:

echidna-test magic.sol
...
echidna_magic_values: passed! 🎉
Seed: 2221503356319272685

Sin embargo, aún podemos usar Echidna para recolectar el corpus cuando ejecutemos esta campaña de fuzzing.

Recolectando un corpus

Para habilitar la recolección de un corpus, crea un directorio de corpus:

mkdir corpus-magic

Y un archivo de configuración de Echidna(opens in a new tab) config.yaml:

1coverage: true
2corpusDir: "corpus-magic"

Ahora podemos ejecutar nuestra herramienta y verificar el corpus recopilado:

echidna-test magic.sol --config config.yaml

Echidna aún no puede encontrar los valores mágicos correctos, pero podemos ver el corpus que recopiló. Por ejemplo, uno de estos archivos era:

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
Mostrar todo
 Copiar

Claramente, esta entrada no provocará la falla en nuestra propiedad. Sin embargo, en el siguiente paso veremos cómo modificarla para ello.

Sembrando un corpus

Echidna necesita ayuda para lidiar con la función magic. Vamos a copiar y modificar la entrada para usar los parámetros adecuados para ella:

cp corpus/2712688662897926208.txt corpus/new.txt

Modificaremos new.txt para llamar a magic (42,129,333,0). Ahora, podemos volver a ejecutar Echidna:

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: failed!💥
  Call sequence:
    magic(42,129,333,0)
Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537
Mostrar todo

En esta ocasión, encontró que la propiedad es violada inmediatamente.

Encontrando transacciones con alto consumo de gas

Veremos cómo encontrar las transacciones con un alto consumo de gas utilizando Echidna. El objetivo es el siguiente smart contract:

1contract C {
2  uint state;
3
4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
Mostrar todo
 Copiar

Aquí expensive puede tener un gran consumo de gas.

Actualmente, Echidna siempre necesita una propiedad para probar: aquí echidna_test siempre devuelve true. Podemos ejecutar Echidna para verificar:

1echidna-test gas.sol
2...
3echidna_test: passed! 🎉
4
5Seed: 2320549945714142710

Midiendo el consumo de gas

Para activar el consumo de gas con Echidna, creamos un archivo de configuración config.yaml:

1estimateGas: true

En este ejemplo, también reduciremos el tamaño de la secuencia de la transacción para que los resultados sean más fáciles de entender:

1seqLen: 2
2estimateGas: true

Ejecuta Echidna

Una vez que tenemos el archivo de configuración creado, podemos ejecutar Echidna así:

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉
f used a maximum of 1333608 gas
  Call sequence:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2
Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325
Mostrar todo

• El gas que se muestra es una estimación proporcionada por HEVM(opens in a new tab).

Filtrando llamadas de reducción de gas

El tutorial sobre funciones de filtrado para llamar durante una campaña de fuzzing anterior muestra cómo eliminar algunas funciones de sus pruebas.
Esto puede ser fundamental para obtener una estimación precisa del gas. Considera el siguiente ejemplo:

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}
Mostrar todo
 Copiar

Si Echidna puede llamar a todas las funciones, no encontrará fácilmente transacciones con un alto costo de gas:

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
Mostrar todo

Eso es porque el costo depende del tamaño de addrs y las llamadas aleatorias tienden a dejar el vector casi vacío. Sin embargo, incluir pop y clear en un blacklist nos da mejores resultados:

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]

1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

Resumen: Buscando transacciones con alto consumo de gas

Echidna puede encontrar transacciones con un alto consumo de gas utilizando la opción de configuración estimateGas:

1estimateGas: true

echidna-test contract.sol --config config.yaml
...

Echidna reportará una secuencia con el consumo máximo de gas para cada función, una vez finalizada la campaña de fuzzing.