Introducción

En este capítulo, introducimos la variable env en CVL, la cual nos permite crear reglas para funciones que dependen de msg.sender, msg.value y otras variables globales en Solidity como block y tx.

Nos centraremos en las dos primeras, a las que se puede acceder desde la variable de CVL env e como e.msg.sender y e.msg.value.

En nuestros ejemplos anteriores, las ignoramos porque las funciones que verificamos no dependían de variables de entorno. Por lo tanto, etiquetamos estas funciones como envfree en el bloque methods. Esto le indica al Prover que las trate como lógica pura e ignore las variables de entorno (globales) para simplificar el análisis.

Sin embargo, en la práctica, las transacciones dependen en gran medida de estas variables de entorno (env), y aquí exploraremos cómo crear reglas con msg.sender y msg.value.

e.msg.sender y e.msg.value (non-payable)

Consideremos un contrato de contador simple controlado por un propietario, donde solo se le permite al propietario incrementar un contador:

Copy
contract OwnerCounter {
    uint256 public counter;
    address public owner;

    constructor(address _owner) {
        owner = _owner;
    }

    function increment() public {
        require(msg.sender == owner, "not owner");
        counter++;
    }
}

La función increment() tiene una declaración require que causará un revert si el llamador no es el propietario. Por lo tanto, nuestra regla necesita depender de msg.sender.

Para verificar la propiedad: “Solo el propietario puede llamar con éxito a increment()”, escribimos la siguiente regla de CVL:

Copy
methods {
  function owner() external returns (address) envfree;
  function counter() external returns (uint256) envfree;
}

rule increment_onlyOwnerCanCallIncrement(env e) {
    address current = owner();

    increment@withrevert(e);
    assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

En el bloque methods, las funciones owner() y counter() están marcadas como envfree porque son funciones view de las variables de almacenamiento y no dependen de variables de entorno o env.

Sin embargo, la función increment() depende del entorno (de ahí el parámetro e). Las funciones no necesitan ser declaradas explícitamente en el bloque methods si se asume que dependen del entorno. Por lo tanto, no incluimos increment() en el bloque methods.

En el bloque de la regla, la declaración env e puede colocarse como un parámetro o dentro del bloque de la regla. Ambas son válidas y son simplemente preferencias de estilo de código:

Copy
rule increment_onlyOwnerCanCallIncrement(env e) {
    ...
}

rule increment_onlyOwnerCanCallIncrement() {
    env e;
    ...
}

Ahora, cuando invocamos una función de Solidity que depende del entorno, debemos incluir el argumento e:

Copy
increment@withrevert(e);

Omitir (e) resultaría en un error del compilador, forzándote a declarar la función como envfree en el bloque methods. Sin embargo, si sigues esto ciegamente y la declaras como envfree, ocurrirán violaciones, y el Prover indicará que la función depende del entorno.

Ahora, finalmente, pasemos a la aserción:

Copy
assert !lastReverted <=> e.msg.sender == current, "access control failed";

Esto comprueba que increment() no hace revert si y solo si msg.sender == owner. Si la aserción falla, significa que el Prover encontró un contraejemplo: o bien se bloqueó al propietario correcto al intentar llamar a increment(), o un no propietario pudo llamarla con éxito.

Cuando ejecutamos esta regla, sin embargo, nos encontramos con un caso de revert inesperado: cuando msg.value != 0. Esto ocurre porque increment() es una función non-payable, lo que significa que no puede aceptar Ether.

En Solidity, un contrato puede recibir Ether a través de una llamada de función, pero solo si la función está explícitamente marcada como payable; de lo contrario, la transacción hará revert. La cantidad de Ether enviada se almacena en la variable global msg.value, que contiene el valor en wei (la denominación más pequeña de Ether).

Dado que increment() no está marcada como payable, cualquier msg.value distinto de cero causa un revert, como se muestra en el informe a continuación:

Para resolver esto, necesitamos colocar e.msg.value == 0 como una precondición.

Luego, ocurre otro revert inesperado cuando counter == max_uint256. Dado que max_uint256 es el valor máximo que puede contener el contador, intentar counter++ causará un revert por desbordamiento (overflow) (ten en cuenta que estamos llamando a la función con la etiqueta withrevert):

Para resolver esto, necesitamos agregar otra precondición require(counter() < max_uint256) para evitar que el contador se desborde.

Con estos dos casos inesperados de revert identificados, ambas condiciones deben incluirse como precondiciones. A continuación se muestra la regla corregida y el informe del Prover. Como se esperaba, la verificación pasa:

Copy
rule increment_onlyOwnerCanCallIncrement(env e) {
    address current = owner();

   require e.msg.value == 0;
   require counter() < max_uint256;  

   increment@withrevert(e);

   assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

Ejecución del Prover: link

Relajando precondiciones con => en lugar de <=>

La regla que creamos anteriormente dice “la función hace revert si y solo si el llamador no es el propietario”. Dado que existen otras condiciones válidas de revert, concretamente msg.value != 0 y counter() == max_uint256, tuvimos que eliminar esas posibilidades en la precondición para que “la función hace revert si y solo si el llamador no es el propietario” fuera cierta.

Si en cambio quisiéramos afirmar, “si un no propietario llama a la función, la transacción hace revert”, podemos usar el operador de implicación sin precondiciones. Otros casos de revert (es decir, msg.value != 0 y que el contador esté en el máximo) no causan una violación. Solo nos importa que si un no propietario llama a la función, esta haga revert.

Dicho esto, aquí está la propiedad a verificar formalmente: “si el llamador no es el propietario, la función debe hacer revert”. A continuación se muestra la regla para ello —una más simple— y como era de esperar, esta regla pasa:

Copy
rule increment_notOwnerCannotCallIncrement(env e) {
    address current = owner();

    increment@withrevert(e);
    assert e.msg.sender != current => lastReverted, "access control failed";
}

Ejecución del Prover: link

Ahora, entendemos cómo escribir reglas para funciones que dependen del entorno. El Prover usa e.msg.sender para razonar sobre la ejecución basada en el llamador y e.msg.value para razonar sobre las transferencias de ETH. En el próximo capítulo, exploraremos ambos conceptos más a fondo.

Resumen

• La variable env en CVL permite razonar sobre funciones que dependen de msg.sender, msg.value y otras variables globales.
• Dichas funciones deben incluir env e, ya sea como un parámetro de la regla o dentro del bloque de la regla.
• Estas funciones dependientes del entorno no necesitan ser declaradas en el bloque methods, mientras que las funciones envfree deben ser declaradas explícitamente y marcadas como envfree.
• Si una función dependiente del entorno no se implementa correctamente como tal, de igual modo compilará y se ejecutará en el Prover, pero producirá violaciones y advertencias.
• Si no se tiene en cuenta adecuadamente msg.value, el Prover generará violaciones y contraejemplos derivados de ello.

Este artículo es parte de una serie sobre verificación formal usando el Certora Prover