En el capítulo anterior, cubrimos cómo razonar sobre funciones dependientes del entorno en CVL centrándonos en msg.sender en contextos no payable. En esos ejemplos, el control de acceso dependía de la dirección del llamador. También explicamos cómo manejar los reverts causados por un msg.value distinto de cero inesperado.

En este capítulo cubriremos cómo:

• escribir reglas para funciones que esperan un pago distinto de cero (es decir, funciones marcadas como payable)
• cómo hacer aserciones sobre los saldos de las cuentas
• cómo obtener el saldo del contrato actual, de manera similar a address(this).balance en Solidity

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

Considera un contrato de listas blancas (whitelisting) donde los usuarios se registran llamando a la función register(), la cual está marcada como payable, y envían al menos 0.05 ETH. Una vez registrados, la dirección del llamador (msg.sender) se marca como whitelisted (en la lista blanca) estableciendo su valor en true dentro del mapping whitelisted:

Copy
/// Solidity

contract PayableWhitelist {
    mapping(address => bool) public whitelisted;

    function register() external payable {
        require(msg.value >= 0.05 ether, "whitelist fee is 0.05 eth");
        require(!whitelisted[msg.sender], "already whitelisted");

        whitelisted[msg.sender] = true;
    }

    function isWhitelisted(address _account) external view returns (bool) {
        return whitelisted[_account];
    }
}

Verificaremos formalmente la propiedad: “el llamador puede llamar con éxito a register() si y solo si paga al menos 0.05 ETH”. Para verificar esto, escribimos la siguiente regla en CVL:

Copy
rule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    register@withrevert(e);
    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

Nota: La exponenciación en CVL usa ^__, mientras que Solidity usa **__.

Como sabemos, dado que estamos utilizando el operador bicondicional, tenemos que descartar otros casos de revert mediante la precondición. Agregamos require(!isWhitelisted(e.msg.sender)) como precondición para descartar el caso en el que msg.sender no está inicialmente en la lista blanca.

Ahora, para la aserción bicondicional:

assert !lastReverted <=> e.msg.value >= 5 * 10^16.

Dado que descartamos el caso donde el remitente está en la lista blanca (require !isWhitelisted(e.msg.sender)), esperamos que esto sea VERIFIED, lo que significa que la función no hará revert solo si e.msg.value >= 5 * 10^16.

Sin embargo, como suele ser el caso en la verificación formal, surge un contraejemplo furtivo que causa una violación. Ocurre cuando el saldo de ETH del remitente es menor que la cantidad prevista a enviar o tiene un saldo insuficiente:

Esto se puede solucionar agregando require(nativeBalances[e.msg.sender] >= e.msg.value) a la precondición, descartando el saldo insuficiente como causa de revert.

nativeBalances en CVL

nativeBalances[address] es una función incorporada en CVL que recupera el saldo actual de ETH de una dirección dada. A continuación, requerimos que nativeBalances para el remitente sea al menos tan grande como el msg.value:

Copy
rule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

Ahora, la regla es VERIFIED:

Ejecución del Prover: link

Verificando el Estado de la Lista Blanca

Ahora que hemos verificado que “el llamador puede llamar con éxito a register() si y solo si paga al menos 0.05 ETH”, mejoremos el alcance de la regla afirmando también que el llamador se encuentra isWhitelisted después de una llamada exitosa.

Aquí está la propiedad actualizada para verificar formalmente: “la transacción tiene éxito si y solo si el llamador envía al menos 0.05 ETH y es agregado a la lista blanca.” Para lograr esto, podemos reutilizar la regla anterior y agregar una aserción adicional: isWhitelisted.

Aquí está la regla CVL actualizada:

Copy
rule register_payEthToWhitelist_modified(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16 && isWhitelisted(e.msg.sender);
}

La regla anterior significa que la transacción no hace revert (!lastReverted) si y solo si el remitente envía al menos 0.05 ETH (e.msg.value >= 5 * 10^16) y es agregado a la lista blanca (isWhitelisted(e.msg.sender)).

En otras palabras, si !lastReverted es true (la transacción tuvo éxito), ambas condiciones —ETH suficiente y estar en la lista blanca— deben cumplirse.

Aquí está el informe del Prover y es VERIFIED:

Ejecución del Prover: link

Relajando Precondiciones Con => En Lugar De <=>

Otro enfoque es usar el operador de implicación. Si tu objetivo es simplemente comprobar que la función hace revert cuando se envía un msg.value incorrecto, la siguiente regla es suficiente. Esta regla no excluye otras causas de revert, como que el remitente no tenga suficiente saldo. Solo dice que si se envían menos de 0.05 ether, entonces definitivamente hará revert.

Copy
rule register_payEthToWhitelist_implication(env e) {
    register@withrevert(e);
    assert e.msg.value < 5 * 10^16 => lastReverted;
}

Si usamos esta regla, vemos que es VERIFIED:

Ejecución del Prover: link

Verificando Transferencias De Saldo De ETH Y El Caso Límite De Auto-Transferencia

Supongamos que queremos verificar formalmente las actualizaciones de saldo donde el saldo de msg.sender disminuye en msg.value y el saldo del contrato aumenta en la misma cantidad.

A continuación se muestra la regla CVL, la cual será explicada en la siguiente sección:

Copy
rule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

El currentContract

En la regla anterior, recuperamos el saldo previo de ETH (balanceBefore) y el saldo final (balanceAfter) del currentContract. currentContract es una variable incorporada que se refiere al contrato que se está verificando. Al pasar esta variable a nativeBalances[currentContract] se recupera el saldo de dicho contrato. Entre estas llamadas de recuperación, se invoca la función register(), por lo que esperamos que el saldo aumente en una cantidad igual a msg.value.

Un contraejemplo inesperado hará que esta regla falle. El Prover generará un contraejemplo donde msg.sender == currentContract. El Prover explora todos los escenarios posibles, incluyendo casos en los que el contrato se llama a sí mismo.

Esto indica que el contrato se envió ETH a sí mismo en lugar de recibir nuevo ETH de un remitente externo. Como resultado, el saldo realmente no aumentó como se esperaba (ya que enviarse ETH a sí mismo no cambia el saldo total), provocando que la aserción balanceAfter == balanceBefore + e.msg.value falle.

Para resolver el problema, dado que msg.sender no debería ser el propio contrato (currentContract), necesitamos filtrar las auto-transferencias al verificar cambios en el saldo de ETH agregando una precondición: require(e.msg.sender != currentContract).

Sin embargo, hay una advertencia: en proyectos reales, asegúrate de que el contrato no pueda llamar a sus propias funciones, ya que ciertos casos aún pueden conducir a auto-llamadas. Si no se verifica adecuadamente, esto podría ocultar un bug.

Aquí está la regla corregida y el informe del Prover. Como se esperaba, esto es VERIFIED:

Copy
rule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];

    require e.msg.sender != currentContract;
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

Ejecución del Prover: link

Verificando Todos Los Casos De Revert Usando <=> y ||

Supongamos que queremos verificar que se contabiliza explícitamente cada posible motivo para hacer revert. Podemos expresar la aserción como un bicondicional (<=>) y enumerar de forma disyuntiva (usando ORs ||) todos los casos de revert.

La regla a continuación establece que los únicos motivos posibles para hacer revert son los siguientes:

• el remitente ya está en la lista blanca
• el saldo del remitente es insuficiente
• el remitente no transfirió fondos suficientes

Si register() hace revert por cualquier otra razón, obtendríamos una violación de aserción.

Aquí está la regla:

Copy
rule register_allRevertCases(env e) {
    bool wasWhitelisted = isWhitelisted(e.msg.sender);
    mathint balanceBefore = nativeBalances[e.msg.sender];

    register@withrevert(e);

    assert lastReverted <=> (
        wasWhitelisted ||              // sender already whitelisted
        balanceBefore < e.msg.value || // sender's balance insufficient
        e.msg.value < 5 * 10^16        // sender's transfer amount insufficient 
    );
}

Como se esperaba, la regla es VERIFIED:

Ejecución del Prover: link

Resumen

• En CVL, la variable de entorno e.msg.value se utiliza para expresar y verificar si una función payable debe tener éxito o hacer revert, generalmente mediante la aserción de una cantidad mínima o exacta requerida.
• nativeBalances[address] es una función incorporada que recupera el saldo actual de ETH de una dirección dada y puede usarse para verificar transferencias comprobando los cambios en el saldo.
• currentContract es una variable incorporada que se refiere al contrato que se está verificando.
• Las auto-llamadas son incluidas en los casos de prueba por el Prover, así que en nuestro ejemplo, las descartamos agregando require(e.msg.sender != currentContract) para evitar falsos contraejemplos; ten precaución, ya que las auto-llamadas pueden ser plausibles y revelar bugs reales en contratos del mundo real.

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