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 su directorio actual. Puede cambiar los archivos desde su host y correr las herramientas dentro de los archivos desde el docker.

Dentro de docker, ejecute:

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 al fuzzing basado en propiedades

Echidna es un fuzzer basado en propiedades; está descrito en nuestras entradas de blog anteriores (1(opens in a new tab), 2(opens in a new tab), 3(opens in a new tab)).

Fuzzing

El fuzzing(opens in a new tab) es una técnica conocida en la comunidad de la seguridad. Consiste en la generación de entradas que son más o menos aleatorias para encontrar errores en el programa. Los fuzzers para software tradicional (como AFL(opens in a new tab) o LibFuzzer(opens in a new tab)) son herramientas eficaces para encontrar errores.

Más allá de la generación de entradas puramente aleatorias, existen muchas técnicas y estrategias para generar buenas entradas, que incluyen:

• Obtener feedback de cada ejecución y guiar la generación usándolo. Por ejemplo, si una entrada recién generada conduce al descubrimiento de una nueva ruta, puede tener sentido generar nuevas entradas cercanas a ella.
• Generar la entrada respetando una restricción estructural. Por ejemplo, si su entrada contiene un encabezado con una suma de control o checksum, tendrá sentido dejar que el fuzzer genere una entrada que valide la suma de control.
• Usar entradas conocidas para generar nuevas entradas: si tiene acceso a un gran conjunto de datos de entrada válidos, el 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 inspirado en gran medida en QuickCheck(opens in a new tab). En contraste a un fuzzer clásico que intentará encontrar crashes, Echidna intentará romper invariantes definidas por el usuario.

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

• Control de acceso incorrecto: el atacante se convirtió en el propietario del contrato.
• Máquina de estado incorrecta: los tokens se pueden transferir mientras el contrato está en pausa.
• Aritmética incorrecta: el usuario puede desbordar su saldo y obtener tokens gratis ilimitados.

Probar una propiedad con Echidna

Veremos cómo probar un contrato inteligente con Echidna. El objetivo es el siguiente contrato inteligente 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 este token debe tener las siguientes propiedades:

• Cualquier persona puede tener como máximo 1000 tokens
• El token no puede transferirse (no es un token ERC20)

Escribir una propiedad

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

• No debe tener ningún argumento.
• Devolver true si hay éxito.
• Su nombre debe comenzar con echidna.

Echidna:

• Generará automáticamente transacciones arbitrarias para probar la propiedad.
• Reportará cualquier transacción que haga que una propiedad devuelva false o arroje 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 invocante no tenga más de 1000 tokens:

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

Use herencia para separar su contrato de sus 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 del contrato.

Iniciar un contrato

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

Hay algunas direcciones específicas en Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72, que 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.

Ejecutar Echidna

Echidna se inicia con:

echidna-test contract.sol

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

echidna-test contract.sol --contract MyContract

Resumen: probar 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 de fuzzing

Veremos cómo filtrar las funciones a fuzzear. El objetivo es el siguiente contrato inteligente.

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

Filtrar funciones

Echidna tiene problemas para encontrar la secuencia correcta para probar este contrato porque las dos funciones de restablecimiento (reset1 y reset2) establecerán todas las variables de estado a false. Sin embargo, podemos usar una función especial de Echidna para poner en la lista negra la función de restablecimiento o para poner en la lista blanca solo las funciones f, g, h e i.

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

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

Otro enfoque para filtrar funciones es incluir funciones en la lista blanca. 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 tiene f() y f(uint256), el filtro "f" coincidirá con ambas funciones.

Ejecutar 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: filtrado de funciones

Echidna puede incluir funciones en una lista negra o lista blanca 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 colocando en la lista negra f1, f2 y f3 o solo los invocándolas según el valor del booleano 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

Escriba 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

Ejecutar Echidna

Para habilitar la prueba de falla de afirmaciones, cree 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 puede 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 qué afirmación falló.

Cómo y cuándo utilizar afirmaciones

Las afirmaciones pueden usarse como alternativas a las 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 algo 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 habrá una verificación. 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 fuerce ningún efecto secundario durante la verificación de afirmaciones. Por ejemplo: assert(ChangeStateAndReturn() == 1)
• No haga afirmaciones obvias. Por ejemplo assert(var >= 0), donde var se declara como uint.

Por último, no utilice require en lugar de assert, ya que Echidna no podrá detectarlo (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 afirmació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 contrato inteligente 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

Este pequeño ejemplo 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 al ejecutar esta campaña de fuzzing.

Recolección de un corpus

Para habilitar la recolección de un corpus, cree 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 recopilado. 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.

Sembrar un corpus

Echidna necesita ayuda para lidiar con la función magic. Vamos a copiar y modificar la entrada para usar 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.

Buscar 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 contrato inteligente.

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 alto consumo de gas.

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

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

Medir el consumo de gas

Para habilitar el consumo de gas con Echidna, cree 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

Ejecutar 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).

Filtrar llamadas de reducción de gas

El tutorial sobre filtrado de funciones 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. Considere 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 array casi vacío. Sin embargo, incluir pop y clear en una lista negra 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: buscar 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.