Cómo usar Echidna para probar contratos inteligentes

Solidity

contratos inteligentes

seguridad

pruebas

fuzzing

Avanzado

Trailofbits

Building secure contracts

10 de abril de 2020

14 minutos de lectura

Instalación

Echidna se puede instalar a través de Docker o usando el 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 último comando ejecuta eth-security-toolbox en un contenedor de Docker que tiene acceso a su directorio actual. Puede cambiar los archivos desde su host y ejecutar las herramientas en los archivos desde 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, que describimos en nuestras publicaciones 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 muy conocida en la comunidad de seguridad. Consiste en generar 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 conocidos por ser herramientas eficientes para encontrar errores.

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

Obtener retroalimentación de cada ejecución y guiar la generación usándola. 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 comprobación (checksum), tendrá sentido dejar que el fuzzer genere entradas que validen la suma de comprobación.
Usar 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 su generación desde cero. Estas generalmente se denominan semillas (seeds).

Fuzzing basado en propiedades

Echidna pertenece a una familia específica de fuzzers: el fuzzing basado en propiedades, fuertemente inspirado en QuickCheck (opens in a new tab). A diferencia de los fuzzers clásicos que intentarán encontrar fallos (crashes), Echidna intentará romper invariantes definidos por el usuario.

En los contratos inteligentes, los invariantes son funciones de Solidity que pueden representar cualquier estado incorrecto o inválido que el contrato pueda alcanzar, 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 causar un desbordamiento inferior (underflow) 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.sol (opens in a new tab):

contract Token{
  mapping(address => uint) public balances;
  function airdrop() public{
      balances[msg.sender] = 1000;
  }
  function consume() public{
      require(balances[msg.sender]>0);
      balances[msg.sender] -= 1;
  }
  function backdoor() public{
      balances[msg.sender] += 1;
  }
}

Haremos la suposición de que este token debe tener las siguientes propiedades:

Cualquiera puede tener como máximo 1000 tokens
El token no se puede transferir (no es un token ERC-20)

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 comience 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 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 el llamador no tiene más de 1000 tokens:

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

Use la herencia para separar su contrato de sus propiedades:

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

token.sol (opens 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 múltiples contratos, puede especificar el objetivo:

echidna-test contract.sol --contract MyContract

Resumen: Probar una propiedad

Lo siguiente resume la ejecución de Echidna en nuestro ejemplo:

contract TestToken is Token{
    constructor() public {}
        function echidna_balance_under_1000() public view returns(bool){
          return balances[msg.sender] <= 1000;
        }
  }

echidna-test testtoken.sol --contract TestToken
...

echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()

...

Echidna descubrió 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 se les hará fuzzing. El objetivo es el siguiente contrato inteligente:

contract C {
  bool state1 = false;
  bool state2 = false;
  bool state3 = false;
  bool state4 = false;

  function f(uint x) public {
    require(x == 12);
    state1 = true;
  }

  function g(uint x) public {
    require(state1);
    require(x == 8);
    state2 = true;
  }

  function h(uint x) public {
    require(state2);
    require(x == 42);
    state3 = true;
  }

 function i() public {
    require(state3);
    state4 = true;
  }

  function reset1() public {
    state1 = false;
    state2 = false;
    state3 = false;
    return;
  }

  function reset2() public {
    state1 = false;
    state2 = false;
    state3 = false;
    return;
  }

  function echidna_state4() public returns (bool) {
    return (!state4);
  }
}

Este pequeño ejemplo obliga a Echidna a encontrar una cierta secuencia 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 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 reinicio (reset1 y reset2) establecerán todas las variables de estado en false. Sin embargo, podemos usar una característica especial de Echidna para poner en la lista negra la función de reinicio o para poner en la lista blanca solo las funciones f, g, h y i.

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

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

Otro enfoque para filtrar funciones es enumerar las funciones en la lista blanca. Para hacer eso, podemos usar este archivo de configuración:

filterBlacklist: false
filterFunctions: ["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 falsificar la propiedad casi de inmediato.

Resumen: Filtrar funciones

Echidna puede poner en la lista negra o en la lista blanca las funciones a llamar durante una campaña de fuzzing usando:

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

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

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

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

En este breve tutorial, vamos a mostrar cómo usar Echidna para probar la comprobación de aserciones en contratos. Supongamos que tenemos un contrato como este:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    // tmp <= counter
    return (counter - tmp);
  }
}

Escribir una aserció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 necesitaremos almacenar el valor de tmp en algún lugar. En su lugar, podríamos usar una aserción como esta:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    assert (tmp <= counter);
    return (counter - tmp);
  }
}

Ejecutar Echidna

Para habilitar la prueba de fallos de aserción, cree un archivo de configuración de Echidna (opens in a new tab) config.yaml:

checkAsserts: 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

Como puede ver, Echidna informa de algún fallo de aserción en la función inc. Es posible agregar más de una aserción por función, pero Echidna no puede decir qué aserción falló.

Cuándo y cómo usar aserciones

Las aserciones se pueden usar 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. Agregar aserciones después de algún código obligará a que la comprobación ocurra inmediatamente después de que se ejecutó:

function f(..) public {
    // algún código complejo
    ...
    assert (condition);
    ...
}

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

function echidna_assert_after_f() public returns (bool) {
    f(..);
    return(condition);
}

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 Regehr (opens in a new tab) sobre cómo usar aserciones:

No fuerce ningún efecto secundario durante la comprobación de la aserción. Por ejemplo: assert(ChangeStateAndReturn() == 1)
No afirme 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

Lo siguiente resume la ejecución de Echidna en nuestro ejemplo:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    assert (tmp <= counter);
    return (counter - tmp);
  }
}

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

Echidna descubrió 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.sol (opens in a new tab):

contract C {
  bool value_found = false;
  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
    require(magic_1 == 42);
    require(magic_2 == 129);
    require(magic_3 == magic_4+333);
    value_found = true;
    return;
  }

  function echidna_magic_values() public returns (bool) {
    return !value_found;
  }

}

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 Manticore (opens in a new tab)). Podemos ejecutar Echidna para verificar esto:

echidna-test magic.sol
...

echidna_magic_values: passed! 🎉

Seed: 2221503356319272685

Sin embargo, todavía podemos usar Echidna para recopilar un corpus al ejecutar esta campaña de fuzzing.

Recopilar un corpus

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

mkdir corpus-magic

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

coverage: true
corpusDir: "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 recopiló. Por ejemplo, uno de estos archivos fue:

[
  {
    "_gas'": "0xffffffff",
    "_delay": ["0x13647", "0xccf6"],
    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
    "_value": "0x0",
    "_call": {
      "tag": "SolCall",
      "contents": [
        "magic",
        [
          {
            "contents": [
              256,
              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
            ],
            "tag": "AbiUInt"
          },
          {
            "contents": [256, "334"],
            "tag": "AbiUInt"
          },
          {
            "contents": [
              256,
              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
            ],
            "tag": "AbiUInt"
          },
          {
            "tag": "AbiUInt",
            "contents": [256, "332"]
          }
        ]
      ]
    },
    "_gasprice'": "0xa904461f1"
  }
]

Claramente, esta entrada no desencadenará el fallo en nuestra propiedad. Sin embargo, en el siguiente paso, veremos cómo modificarla para eso.

Sembrar un corpus

Echidna necesita algo de 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

Esta vez, descubrió que la propiedad se viola de inmediato.

Encontrar transacciones con alto consumo de gas

Veremos cómo encontrar las transacciones con alto consumo de gas con Echidna. El objetivo es el siguiente contrato inteligente:

contract C {
  uint state;

  function expensive(uint8 times) internal {
    for(uint8 i=0; i < times; i++)
      state = state + i;
  }

  function f(uint x, uint y, uint8 times) public {
    if (x == 42 && y == 123)
      expensive(times);
    else
      state = 0;
  }

  function echidna_test() public returns (bool) {
    return true;
  }

}

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:

echidna-test gas.sol
...
echidna_test: ¡aprobado! 🎉

Semilla: 2320549945714142710

Medir el consumo de gas

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

estimateGas: 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:

seqLen: 2
estimateGas: true

Ejecutar Echidna

Una vez que hayamos 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

El gas mostrado es una estimación proporcionada por HEVM (opens in a new tab).

Filtrar llamadas que reducen el gas

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

contract C {
  address [] addrs;
  function push(address a) public {
    addrs.push(a);
  }
  function pop() public {
    addrs.pop();
  }
  function clear() public{
    addrs.length = 0;
  }
  function check() public{
    for(uint256 i = 0; i < addrs.length; i++)
      for(uint256 j = i+1; j < addrs.length; j++)
        if (addrs[i] == addrs[j])
          addrs[j] = address(0x0);
  }
  function echidna_test() public returns (bool) {
      return true;
  }
}

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

echidna-test pushpop.sol --config config.yaml
...
pop usó un máximo de 10746 de gas
...
check usó un máximo de 23730 de gas
...
clear usó un máximo de 35916 de gas
...
push usó un máximo de 40839 de gas

Eso es porque el costo depende del tamaño de addrs y las llamadas aleatorias tienden a dejar la matriz casi vacía. Sin embargo, poner en la lista negra pop y clear nos da resultados mucho mejores:

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

echidna-test pushpop.sol --config config.yaml
...
push usó un máximo de 40839 de gas
...
check usó un máximo de 1484472 de gas

Resumen: Encontrar transacciones con alto consumo de gas

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

estimateGas: 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 termine la campaña de fuzzing.