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 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/training

Binario

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

Introducción al fuzzing basado en propiedades

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

Fuzzing

Fuzzingopens in a new tab es una técnica muy conocida en la comunidad de la seguridad. Consiste en generar entradas que son más o menos aleatorias para encontrar errores en el programa. Los fuzzers para software tradicional (como AFLopens in a new tab o LibFuzzeropens in a new tab) son conocidos por ser herramientas eficientes 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 una cabecera con una suma de verificación (checksum), tendrá sentido dejar que el fuzzer genere una entrada que valide la suma de verificación.
• Utilizar entradas conocidas para generar nuevas entradas: si tiene acceso a un gran conjunto de datos de entradas válidas, su fuzzer puede generar nuevas entradas a partir de ellas, en lugar de comenzar la generación desde cero. Estas se suelen llamar seeds.

Fuzzing basado en propiedades

Echidna pertenece a una familia específica de fuzzer: el fuzzing basado en propiedades, muy inspirado en QuickCheckopens in a new tab. A diferencia del fuzzer clásico, que intentará encontrar fallos, Echidna intentará romper las invariantes definidas por el usuario.

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

• Control de acceso incorrecto: el atacante se convirtió en el propietario del contrato.
• Máquina de estado incorrecta: los tokens pueden transferirse mientras el contrato está en pausa.
• Aritmética incorrecta: el usuario puede provocar un subdesbordamiento en 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.solopens 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

Asumiremos que este token debe tener las siguientes propiedades:

• Cualquiera puede tener un máximo de 1000 tokens
• El token no se puede transferir (no es un token ERC20)

Escribir una propiedad

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

• No tener argumentos
• Devolver true si tiene éxito
• Tener un nombre que empiece con echidna

Echidna hará lo siguiente:

• Generar automáticamente transacciones arbitrarias para probar la propiedad.
• Informar de cualquier transacción que lleve a una propiedad a devolver false o a lanzar un error.
• Descartar los 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 quien realiza la llamada no tiene más de 1000 tokens:

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

Utilice la 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.solopens in a new tab implementa la propiedad y hereda del token.

Iniciar un contrato

Echidna necesita un constructor sin argumentos. 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 llaman aleatoriamente a las otras funciones.

No necesitamos ninguna inicialización 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 encontró que la propiedad se viola si se llama a backdoor.

Filtrar funciones para llamar durante una campaña de fuzzing

Veremos cómo filtrar las funciones a las que aplicar fuzzing. 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 usar una herramienta de ejecución simbólica como Manticoreopens in a new tab). Podemos ejecutar Echidna para verificar esto:

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

Filtrado de funciones

Echidna tiene problemas para encontrar la secuencia correcta para probar este contrato porque las dos funciones de reseteo (reset1 y reset2) establecerán todas las variables de estado a false. Sin embargo, podemos usar una característica especial de Echidna para incluir en la lista negra la función de reseteo o para incluir 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 listar las funciones incluidas en la lista blanca. Para ello, podemos usar este archivo de configuración:

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

• filterBlacklist es true por defecto.
• El filtrado se realizará solo 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 falsear la propiedad casi de inmediato.

Resumen: Filtrado de funciones

Echidna puede incluir funciones en una lista negra o en una lista blanca para llamar durante una campaña de fuzzing usando:

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

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

Echidna inicia una campaña de fuzzing, ya sea incluyendo en la lista negra a f1, f2 y f3 o solo llamando a estas, según el valor del booleano filterBlacklist.

Cómo probar el assert de Solidity con Echidna

En este breve tutorial, vamos a mostrar cómo usar Echidna para probar la comprobación de aserciones en los 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

Escribir una aserción

Queremos asegurarnos de que tmp es menor o igual que counter después de devolver su diferencia. Podríamos escribir una propiedad de Echidna, pero necesitaremos almacenar el valor tmp en algún lugar. En su lugar, podríamos usar una aserció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 fallos de aserción, cree un archivo de configuración de Echidnaopens in a new tab config.yaml:

1checkAsserts: true

Cuando ejecutamos 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 fallo de aserción en la función inc. Es posible añadir más de una aserción por función, pero Echidna no puede decir qué aserción ha fallado.

Cuándo y cómo usar aserciones

Las aserciones se pueden utilizar como alternativas a las propiedades explícitas, especialmente si las condiciones a comprobar están directamente relacionadas con el uso correcto de alguna operación f. Añadir aserciones después de un código forzará que la comprobación se produzca inmediatamente después de que se haya ejecutado:

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

Por el contrario, usar una propiedad explícita de Echidna ejecutará transacciones aleatoriamente y no hay una forma fácil de forzar exactamente cuándo se comprobará. Aún es posible usar esta solución:

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

Sin embargo, hay algunos problemas:

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

En general, recomendamos seguir la recomendación de John Regehropens in a new tab sobre cómo usar las aserciones:

• No fuerce ningún efecto secundario durante la comprobación de la aserción. Por ejemplo: assert(ChangeStateAndReturn() == 1)
• No asegure declaraciones obvias. Por ejemplo, assert(var >= 0) donde var se declara como uint.

Finalmente, por favor, no use require en lugar de assert, ya que Echidna no podrá detectarlo (pero el contrato se revertirá de todos modos).

Resumen: comprobación de aserciones

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 encontró que la aserción en inc puede fallar si esta función se llama varias veces con argumentos grandes.

Recopilar y modificar un corpus de Echidna

Veremos cómo recopilar y usar un corpus de transacciones con Echidna. El objetivo es el siguiente contrato inteligente magic.solopens 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 usar una herramienta de ejecución simbólica como Manticoreopens 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 recopilar un corpus al ejecutar esta campaña de fuzzing.

Recopilando un corpus

Para habilitar la recopilación del corpus, cree un directorio de corpus:

mkdir corpus-magic

Y un archivo de configuración de Echidnaopens in a new tab config.yaml:

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

Ahora podemos ejecutar nuestra herramienta y comprobar el corpus recopilado:

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

Echidna todavía no puede encontrar los valores mágicos correctos, pero podemos echar un vistazo al corpus que ha 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 activará el fallo en nuestra propiedad. Sin embargo, en el siguiente paso veremos cómo modificarlo 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

Esta vez, encontró que la propiedad es violada inmediatamente.

Encontrar 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 gran 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

Medición del 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 transacciones para que los resultados sean más fáciles de entender:

1seqLen: 2
2estimateGas: true

Ejecutar Echidna

Una vez que hemos creado el archivo de configuración, podemos ejecutar Echidna de esta manera:

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 HEVMopens in a new tab.

Filtrar llamadas que reducen el gas

El tutorial anterior sobre el filtrado de funciones a las que llamar durante una campaña de fuzzing 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 coste 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

Esto se debe a que el coste depende del tamaño de addrs y las llamadas aleatorias tienden a dejar el array casi vacío. Sin embargo, incluir en la lista negra pop y clear nos da resultados mucho mejores:

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: Encontrar transacciones con alto consumo de gas

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

1estimateGas: true

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

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

Última actualización de la página: 21 de octubre de 2025

popens in a new tab

popens in a new tab

nopens in a new tab

+8

Ver colaboradores