Introducción

En este capítulo, verificamos formalmente la implementación de ERC-20 de Solmate, la cual incluye lo siguiente:

• Funciones estándar que cambian el estado: transfer(), approve(), transferFrom()
• Funciones de vista estándar: totalSupply(), balanceOf(), allowance()
• Funciones internas extendidas: _mint(), _burn()

Ten en cuenta que, aunque la implementación de ERC-20 de Solmate incluye una función permit(), la omitimos intencionalmente porque la verificación formal de firmas criptográficas aún no se cubre en esta serie.

Lo que hace interesante al token ERC-20 de Solmate es su uso de bloques unchecked para ahorrar gas durante las modificaciones del total supply (oferta total) y los saldos. Dado que los bloques unchecked omiten las comprobaciones de desbordamiento (overflow) integradas en Solidity, la verificación formal es esencial para demostrar matemáticamente que no pueden ocurrir desbordamientos.

Aquí está la implementación simplificada del ERC-20 de Solmate , con solo la función permit() eliminada:

Copy
// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity >=0.8.0;

/// @notice Modern and gas efficient ERC20 + EIP-2612 implementation.
/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol)
/// @author Modified from Uniswap (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol)
/// @dev Do not manually set balances without updating totalSupply, as the sum of all user balances must not exceed it.
abstract contract ERC20 {
    /*//////////////////////////////////////////////////////////////
                                 EVENTS
    //////////////////////////////////////////////////////////////*/

    event Transfer(address indexed from, address indexed to, uint256 amount);

    event Approval(address indexed owner, address indexed spender, uint256 amount);

    /*//////////////////////////////////////////////////////////////
                            METADATA STORAGE
    //////////////////////////////////////////////////////////////*/

    string public name;

    string public symbol;

    uint8 public immutable decimals;

    /*//////////////////////////////////////////////////////////////
                              ERC20 STORAGE
    //////////////////////////////////////////////////////////////*/

    uint256 public totalSupply;

    mapping(address => uint256) public balanceOf;

    mapping(address => mapping(address => uint256)) public allowance;

    /*//////////////////////////////////////////////////////////////
                               CONSTRUCTOR
    //////////////////////////////////////////////////////////////*/

    constructor(
        string memory _name,
        string memory _symbol,
        uint8 _decimals
    ) {
        name = _name;
        symbol = _symbol;
        decimals = _decimals;
    }

    /*//////////////////////////////////////////////////////////////
                               ERC20 LOGIC
    //////////////////////////////////////////////////////////////*/

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        allowance[msg.sender][spender] = amount;

        emit Approval(msg.sender, spender, amount);

        return true;
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        balanceOf[msg.sender] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(msg.sender, to, amount);

        return true;
    }

    function transferFrom(
        address from,
        address to,
        uint256 amount
    ) public virtual returns (bool) {
        uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.

        if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

        balanceOf[from] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(from, to, amount);

        return true;
    }

    /*//////////////////////////////////////////////////////////////
                        INTERNAL MINT/BURN LOGIC
    //////////////////////////////////////////////////////////////*/

    function _mint(address to, uint256 amount) internal virtual {
        totalSupply += amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(address(0), to, amount);
    }

    function _burn(address from, uint256 amount) internal virtual {
        balanceOf[from] -= amount;

        // Cannot underflow because a user's balance
        // will never be larger than the total supply.
        unchecked {
            totalSupply -= amount;
        }

        emit Transfer(from, address(0), amount);
    }
}

La implementación de ERC-20 anterior es un contrato abstracto, lo que requiere un contrato que lo herede para hacerlo concreto. También necesitamos exponer _mint() y _burn() a través de funciones externas para que el Prover pueda invocarlas durante la verificación. Para abordar ambos requisitos, utilizamos un contrato harness.

Un contrato harness hereda del contrato bajo verificación para hacer que las funciones internas sean accesibles para el Prover envolviéndolas como funciones externas. También puede definir funciones de ayuda de tipo view o pure que proporcionen consultas de estado y cálculos de utilidad para simplificar la lógica de las reglas y los invariantes.

Para esta especificación, el harness es un contrato mínimo que hereda la implementación abstracta de ERC-20 tanto para proporcionar un contrato concreto como para hacer que sus funciones internas (_mint() y _burn()) sean accesibles para la verificación.

Aquí está el contrato harness:

Copy
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.25; 

import "src/Solmate/ERC20.sol";

contract ERC20Harness is ERC20 {    
    constructor (
        string memory _name, 
        string memory _symbol, 
        uint8 _decimals
    ) ERC20(_name, _symbol, _decimals) {}
    
    /// Left without access controls; integrators are expected to implement their own.
    function mint(address _to, uint256 _amount) external {
        _mint(_to, _amount);
    }
	
    /// Left without access controls; integrators are expected to implement their own.
    function burn(address _from, uint256 _amount) external {
        _burn(_from, _amount);
    }
}

Enfoque secuenciado para verificar formalmente las propiedades del ERC-20

En este capítulo, tomamos un enfoque secuenciado para verificar formalmente las propiedades del contrato ERC-20. El esquema es el siguiente:

• ¿Cuál es la intención? ¿Qué quiere el usuario que suceda?
  • ¿Qué función(es) cumple(n) con esta intención?
    • Si la llamada tiene éxito, ¿cómo se refleja el cambio de estado previsto?
    • Si la llamada tiene éxito, ¿qué efectos secundarios no deseados o cambios de estado para las partes no involucradas no deben ocurrir?
    • Si la llamada se revierte, ¿qué causa la reversión?
• ¿Qué invariantes deben mantenerse siempre?
• ¿Qué acciones no autorizadas (por parte de funciones o llamadores) no deben permitirse?

El proceso se ilustra en el siguiente diagrama:

A continuación, revisamos cada paso mostrado en la secuencia numerada a continuación:

1. Verificación de la corrección de funciones (las llamadas tienen éxito o se revierten)

transfer()

Comencemos con la intención de enviar tokens: verificamos que cuando un remitente transfiere tokens, el receptor recibe la cantidad exacta especificada. Esto se logra mediante la función transfer().

Aquí está la implementación de la función transfer():

Copy
function transfer(address to, uint256 amount) public virtual returns (bool) {
    balanceOf[msg.sender] -= amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(msg.sender, to, amount);

    return true;
}

Aquí está la regla de CVL que verifica tanto que el saldo del remitente disminuye como que el saldo del receptor aumenta en la cantidad exacta:

Copy
rule transfer_effectOnBalances(env e) {
    address receiver;
    uint256 amount;

    require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256; // will be replaced by an invariant
    
    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

Expliquemos esta regla con más detalle.

La precondición restringe al Prover de asignar saldos cuya suma exceda el límite max_uint256 como se ve a continuación:

Copy
require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256; // will be replaced by an invariant

Esto es necesario porque la función transfer() utiliza un bloque unchecked cuando añade la cantidad de la transferencia a balanceOf[address], lo que hace que el Prover trate los desbordamientos como “posibles” y reporte falsos positivos.

Sin embargo, como esta precondición restringe los valores a max_uint256, el Prover no puede probar condiciones de desbordamiento que realmente podrían ocurrir, lo que puede ocultar errores de desbordamiento. Por lo tanto, debe descartarse formalmente con un invariante verificado, el cual abordaremos en la sección "requireInvariant”.

Después de la precondición, procedemos con los siguientes pasos:

• Registrar los saldos del remitente y del receptor antes de la llamada a transfer().
• Invocar la llamada a transfer().
• Registrar los saldos del remitente y del receptor nuevamente después de la llamada. Usaremos estos valores en la afirmación para razonar sobre los cambios de saldo tanto para el remitente como para el receptor.

Copy
mathint senderBalanceBefore = balanceOf(e.msg.sender);
mathint receiverBalanceBefore = balanceOf(receiver);

transfer(e, receiver, amount);

mathint senderBalanceAfter = balanceOf(e.msg.sender);
mathint receiverBalanceAfter = balanceOf(receiver);

Ahora, las afirmaciones:

• Si el remitente y el receptor son diferentes, afirmamos que:
  • El saldo del remitente disminuye en amount.
  • El saldo del receptor aumenta en amount.
• Si el remitente es el mismo que el receptor, afirmamos que los saldos permanecen sin cambios:

Copy
if (receiver != e.msg.sender) {
    assert senderBalanceAfter == senderBalanceBefore - amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
} 
else {
    assert senderBalanceAfter == senderBalanceBefore;
    assert receiverBalanceAfter == receiverBalanceBefore;
}

La afirmación confirma la transferencia directa de valor sin deducciones, como se muestra en esta ejecución del Prover.

Reversiones de transfer()

Acabamos de cubrir la ruta de transferencia exitosa. A continuación, verificamos que transfer() se revierte bajo condiciones de fallo.

La siguiente regla de CVL tiene en cuenta todas las condiciones de reversión en las afirmaciones. Utiliza el operador bicondicional (<=>) para establecer que se produce una reversión si y solo si una de las condiciones enumeradas es verdadera. Estas condiciones son:

• El remitente no tiene saldo suficiente.
• Se envía ETH junto con una llamada a una función que es non-payable.

Copy
rule transfer_reverts(env e) {
    address receiver;
    uint256 amount;

    mathint senderBalance = balanceOf(e.msg.sender);

    transfer@withrevert(e, receiver, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        senderBalance < amount || // sender doesn't have enough balance
        e.msg.value != 0 // sending ETH with a call to transfer (non-payable)
    );
}

Para esta regla, no definimos ninguna precondición, por lo que pasamos directamente a registrar el estado antes de la llamada a la transferencia. La siguiente línea captura el valor antes de la llamada a la transferencia:

Copy
mathint senderBalance = balanceOf(e.msg.sender);

Para la afirmación, solo se enumeran dos escenarios como causas de reversión. El primero es cuando el saldo del remitente es menor que la cantidad a transferir, ya que un remitente no debería poder enviar más tokens de los que posee:

Copy
assert isLastReverted <=> (
    senderBalance < amount || // not enough balance
    e.msg.value != 0
);

El segundo caso (e.msg.value != 0) resulta en una reversión porque la función es non-payable. Cualquier msg.value distinto de cero hace que falle. Esta es una condición de reversión para funciones non-payable y aparecerá frecuentemente durante la verificación formal del ERC-20.

La afirmación utiliza un operador bicondicional para garantizar que la función se revierta si y solo si ocurre cualquiera de los dos casos. Esto significa que ninguna otra condición debería causar la reversión de la función. Aquí está la ejecución del Prover.

transferFrom()

Aquí, verificamos que cuando un gastador (spender) autorizado transfiere tokens en nombre de un titular (holder), el receptor recibe la cantidad exacta especificada. Esto se hace utilizando la función transferFrom() como se muestra en la implementación de Solidity a continuación. El cambio en el allowance de esta transferencia se analizará en una sección posterior.

Copy
function transferFrom(
    address from,
    address to,
    uint256 amount
) public virtual returns (bool) {
    uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.

    if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

    balanceOf[from] -= amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(from, to, amount);

    return true;
}

La siguiente regla es casi idéntica a la regla transfer_effectOnBalances — la única diferencia es que invoca a transferFrom(). Hace lo siguiente:

• Precondiciones: Restringe la suma de los saldos del titular y del receptor para que permanezca dentro de max_uint256 para evitar que el Prover explore escenarios de desbordamiento en el bloque unchecked.
• Estados previos y posteriores a la llamada: Registra los saldos de ambas cuentas antes y después de la llamada a transferFrom() para que podamos verificar los cambios de saldo exactos en las afirmaciones.
• Afirmaciones:
  • Si receiver != holder, afirmar que sus saldos difieren por amount.
  • Si receiver == holder, afirmar que el saldo permanece sin cambios.

Copy
rule transferFrom_effectOnBalances(env e) {
    address holder;
    address receiver;
    uint256 amount;
    
    require balanceOf(holder) + balanceOf(receiver) <= max_uint256; // will be formally verified later

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

Ver la ejecución del Prover.

Reversiones de transferFrom()

El patrón de la regla de reversión de transferFrom() también es similar a la regla de transfer(), excepto por un caso adicional que involucra al gastador. Como se muestra a continuación, si el gastador carece del allowance suficiente (es decir, si spenderAllowance < amount), la transacción se revierte:

Copy
rule transferFrom_reverts(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint holderBalance = balanceOf(holder);
    mathint spenderAllowance = allowance(holder, e.msg.sender); 
 
 

    transferFrom@withrevert(e, holder, receiver, amount); // spender is the msg.sender
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        holderBalance < amount || 
        spenderAllowance < amount || 
        e.msg.value != 0 
    );
}

Todos los demás escenarios de reversión son los mismos que en la regla de transfer(). Aquí está la ejecución del Prover.

Cambio en el allowance

Cuando una llamada a transferFrom() tiene éxito, el allowance aprobado del titular para el gastador cambia. La implementación de transferFrom() incluye este condicional:

Copy
if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

Esto significa que si el allowance actual no está establecido en el valor máximo de uint256, la cantidad gastada se deduce de él. Si el allowance está establecido en el máximo, se comporta como un allowance infinito y permanece sin cambios.

Este comportamiento es capturado en la sección de afirmaciones de la regla de CVL que se muestra a continuación:

Copy
rule transferFrom_allowanceChange(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint spenderAllowanceBefore = allowance(holder, e.msg.sender);

    transferFrom(e, holder, receiver, amount);
    mathint spenderAllowanceAfter = allowance(holder, e.msg.sender);

    if (spenderAllowanceBefore != max_uint256) {
        assert spenderAllowanceAfter == spenderAllowanceBefore - amount;
    }
    else {
        assert spenderAllowanceAfter == spenderAllowanceBefore;
    }
}

Ejecución del Prover: enlace

approve()

Los allowances se deducen dentro de la función transferFrom(), pero la aprobación real del allowance se establece en la función approve(). A continuación se muestra su implementación:

Copy
function approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount;

    emit Approval(msg.sender, spender, amount);

    return true;
}

La variable allowance es un mapping público y anidado. Por lo tanto, Solidity genera automáticamente una función getter, lo que permite que sea invocada directamente en CVL (allowance(e.msg.sender, spender)):

Copy
rule approve_spenderAllowance(env e) {
    address spender;
    uint256 amount;

    approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;

    mathint approvedAmountAfter = allowance(e.msg.sender, spender);

    assert !isReverted => approvedAmountAfter == amount;
    assert isReverted <=> e.msg.value != 0;
}

Ejecución del Prover: enlace

Para mayor concisión, la regla anterior combina los casos de éxito y de reversión, utilizando la implicación y el operador bicondicional en lugar de crear reglas separadas para cada uno o usar un bloque if/else.

La función approve() debe ser invocada dentro del contexto de env e porque depende de variables de entorno globales como msg.sender y msg.value. Específicamente, la función utiliza msg.sender para determinar qué dirección está estableciendo el allowance para el spender:

Copy
function approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount; // relies on msg.sender
    ...
}

Ahora, para la afirmación:

• Si la llamada a la función tiene éxito, el allowance se establece en la cantidad especificada.
• La función se revierte si y solo si e.msg.value es distinto de cero, lo que significa que se envió ETH con la llamada a la función approve.

Copy
assert !isReverted => approvedAmountAfter == amount;
assert isReverted <=> e.msg.value != 0;

transfer(), transferFrom() y approve() devuelven true en una llamada exitosa

Aparte de sus operaciones que cambian el estado, transfer(), transferFrom() y approve() deben devolver true en una ejecución exitosa, según lo requiere el estándar ERC-20.

Las siguientes reglas llaman a sus respectivas funciones con @withrevert para capturar si se revierten, almacenan el resultado en isLastReverted, y afirman que si la llamada no se revirtió, debe devolver true:

Copy
rule transfer_successReturnsTrue(env e) {
    address receiver;
    uint256 amount;

    bool retVal = transfer@withrevert(e, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule transferFrom_successReturnsTrue(env e) {
    address holder;
    address receiver;
    uint256 amount;

    bool retVal = transferFrom@withrevert(e, holder, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule approve_successReturnsTrue(env e) {
    address spender;
    uint256 amount;

    bool retVal = approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;
    
    assert !isReverted => (retVal == true);
}

Ejecución del Prover: enlace

Estas reglas verifican que transfer(), transferFrom() y approve() devuelvan true en llamadas exitosas.

mint()

Aumentar el total supply es la intención del minting (acuñación). Al mismo tiempo, los tokens recién acuñados se asignan a un receptor, aumentando su saldo. La implementación de Solidity a continuación muestra cómo tanto totalSupply como balanceOf[to] se incrementan en amount:

Copy
function _mint(address to, uint256 amount) internal virtual {
    totalSupply += amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }
    ...
}

El incremento a balanceOf[address] ocurre dentro de un bloque unchecked, mientras que el incremento a totalSupply sucede fuera del bloque unchecked y está protegido por las comprobaciones de desbordamiento del compilador de Solidity.

Debido al bloque unchecked, el Prover explora la posibilidad de un desbordamiento de saldo, aunque esto realmente no puede ocurrir dado que los saldos aumentan al mismo ritmo que totalSupply. Para evitar falsos positivos, agregamos la precondición require totalSupply() >= balanceOf(receiver).

Aquí está la regla de CVL que captura tanto el aumento en el total supply como el aumento correspondiente en el saldo del receptor:

Copy
rule mint_increasesTotalSupplyAndBalance() {
    address receiver;
    uint256 amount;

    require totalSupply() >= balanceOf(receiver); // will be replaced by an invariant

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}

Ejecución del Prover: enlace

Siguiendo el patrón establecido, capturamos el estado antes y después de la llamada al método mint():

Copy
mathint totalSupplyBefore = totalSupply();
mathint receiverBalanceBefore = balanceOf(receiver);

mint(receiver, amount);

mathint totalSupplyAfter = totalSupply();
mathint receiverBalanceAfter = balanceOf(receiver);

Y ahora la afirmación, donde tanto el aumento en el total supply como el aumento correspondiente en el saldo del receptor son iguales a amount:

Copy
assert totalSupplyAfter == totalSupplyBefore + amount;
assert receiverBalanceAfter == receiverBalanceBefore + amount;

Reversiones de mint()

La función mint() se revierte si y solo si la suma del total supply y la cantidad a acuñar excede max_uint256. Esto representa un escenario de desbordamiento. Aquí está la regla de CVL que captura este comportamiento:

Copy
rule mint_reverts() {
    address receiver;
    uint256 amount;

    mathint totalSupply = totalSupply();

    mint@withrevert(receiver, amount);
    bool isReverted = lastReverted;

    assert isReverted <=> totalSupply + amount > max_uint256;
}

Ejecución del Prover: enlace

burn()

Mientras que el minting aumenta el total supply, la intención de la quema (burning) es reducirlo. Cada operación de quema disminuye tanto el total supply como el saldo del propietario del token.

Aquí está la implementación:

Copy
function _burn(address from, uint256 amount) internal virtual {
    balanceOf[from] -= amount;

    // Cannot underflow because a user's balance
    // will never be larger than the total supply.
    unchecked {
        totalSupply -= amount;
    }

    emit Transfer(from, address(0), amount);
}

Aquí está la regla que captura tanto la disminución en el total supply como la disminución en el saldo del propietario del token:

Copy
rule burn_decreasesTotalSupplyAndBalance() {
    address holder;
    uint256 amount;
			
	require totalSupply() >= balanceOf(holder); // will be replaced by an invariant
		
    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Ejecución del Prover: enlace

En la función _burn(), la operación totalSupply -= amount está dentro de un bloque unchecked. Por lo tanto, el Prover explora la posibilidad de un desbordamiento negativo (underflow), aunque realmente no puede ocurrir. Para evitar esto, agregamos la precondición require totalSupply() >= balanceOf(holder) en la regla.

Para el resto del código, el patrón es similar a mint(), excepto que tanto el saldo como el total supply disminuyen en la cantidad especificada, como se espera al quemar.

Reversiones de burn()

La función burn() se revierte si y solo si el saldo del titular es menor que la cantidad a quemar. Esta es una comprobación de seguridad impuesta por Solidity que desencadena una reversión cuando balanceOf[from] -= amount (ejecutado fuera de un bloque unchecked) intenta restar más del saldo disponible.

Aquí está la regla de CVL que verifica este comportamiento:

Copy
rule burn_reverts(env e) {
	address holder;
	uint256 amount;

	mathint holderBalance = balanceOf(holder);

	burn@withrevert(holder, amount);
	bool isReverted = lastReverted;

	assert isReverted <=> holderBalance < amount;
}

Ejecución del Prover: enlace

2. Efectos secundarios no deseados de transfer, transferFrom, mint y burn

Habiendo verificado que las funciones se comportan correctamente en escenarios tanto de éxito como de reversión, ahora verificamos que no haya efectos secundarios no deseados ni cambios de estado para las partes no involucradas.

Una función puede causar cambios involuntarios en el almacenamiento para cuentas que no están involucradas en la operación. Para este contrato, verificamos formalmente que el saldo de ninguna cuenta no involucrada sea modificado por transfer(), transferFrom(), mint() o burn().

Cada regla sigue el mismo patrón: designamos una dirección como no involucrada (a través de sentencias require), capturamos su saldo antes de la operación, ejecutamos la función, y luego afirmamos que el saldo permanece sin cambios. Esto demuestra que solo las cuentas pasadas explícitamente como argumentos se ven afectadas:

Copy
rule noUninvolvedBalancesAreAffectedByDirectTransfer(env e) {
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != e.msg.sender;

    mathint otherBalanceBefore = balanceOf(other);
    transfer(e, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByTransferFrom(env e) {
    address holder;
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != holder;

    mathint otherBalanceBefore = balanceOf(other);
    transferFrom(e, holder, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByMint() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    mint(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByBurn() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    burn(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

Ejecución del Prover: enlace

3. Invariantes

Ahora que hemos verificado tanto las rutas exitosas como las de reversión, y que no ocurren efectos secundarios no deseados, podemos pasar a los invariantes: condiciones que deben mantenerse siempre, independientemente de qué función se llame, qué argumentos se utilicen o cuántas llamadas válidas se realicen en secuencia.

La suma de los saldos debe ser igual al total supply

Bajo ninguna circunstancia debe la suma de todos los saldos diferir del total supply, porque cualquier divergencia indica que se han creado o destruido tokens fuera de mint() o burn(), ya sea dando a los usuarios más tokens de los que realmente existen o provocando que los tokens desaparezcan del sistema. La siguiente especificación de CVL verifica formalmente este invariante:

Copy
ghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

hook Sload uint256 balance balanceOf[KEY address account] { 
    require g_sumOfBalances >= balance;
}

invariant totalSupplyEqualsSumOfBalances()
	to_mathint(totalSupply()) == g_sumOfBalances;

Ejecución del Prover: enlace

Discutámoslo con más detalle.

El primer bloque declara una variable ghost g_sumOfBalances como un mathint y la inicializa a cero. Sin esta inicialización, el Prover asigna valores iniciales arbitrarios, lo que podría llevar a violaciones de falsos positivos:

Copy
ghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

Ahora, aquí está el hook Sstore donde se usa la variable ghost g_sumOfBalances para almacenar y rastrear cambios en los saldos totales de las cuentas:

Copy
hook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

El hook Sload a continuación restringe las lecturas de saldo para evitar que el Prover asigne valores mayores a la suma rastreada de los saldos:

Copy
hook Sload uint256 balance balanceOf[KEY address account] { 
    require g_sumOfBalances >= balance;
}

Finalmente, verificamos formalmente que el total supply sea igual a la suma de todos los saldos:

Copy
invariant totalSupplyEqualsSumOfBalances()
	to_mathint(totalSupply()) == g_sumOfBalances;

requireInvariant — el invariante como precondición

El invariante totalSupplyEqualsSumOfBalances no solo es útil como propiedad universal, sino que también dependemos de él como una suposición probada en lugar de precondiciones.

Más allá del significado obvio de que el total supply equivale a la suma de todos los saldos, el invariante totalSupply() == g_sumOfBalances también implica:

• El total supply es siempre mayor o igual a cualquier saldo individual.
• Tanto el total supply como la suma de los saldos permanecen dentro de max_uint256.

Recuerda que las reglas anteriores de transfer y transferFrom incluían una precondición que requería que los saldos permanecieran dentro de max_uint256. Esto podría haber ocultado un error de desbordamiento porque la precondición asumía y restringía los saldos, lo que pudo haber filtrado involuntariamente estados donde el error podría aparecer.

Por lo tanto, usar el invariante verificado totalSupplyEqualsSumOfBalances como la precondición es más seguro, porque garantiza que la regla se ejecute con una propiedad que se mantiene en “todos” los estados alcanzables.

Ahora reemplazamos las sentencias require con requireInvariant totalSupplyEqualsSumOfBalances, como se muestra a continuación:

Copy
rule transfer_effectOnBalances_requireInvariant(env e) {
    address receiver;
    uint256 amount;

    // previously: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();
    
    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

rule transferFrom_effectOnBalances_requireInvariant(env e) {
    address holder;
    address receiver;
    uint256 amount;

    // previously: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

Además, las reglas de burn y mint incluyen una precondición que requiere que el total supply sea mayor o igual a los saldos del titular y del receptor, respectivamente. Esta precondición require es una restricción asumida, y para estar seguros, la reemplazamos con un invariante probado.

Dado que el invariant totalSupplyEqualsSumOfBalances también implica que el total supply es mayor o igual a todos los saldos individuales, podemos reemplazar la precondición require con requireInvariant totalSupplyEqualsSumOfBalances:

Copy
rule mint_increasesTotalSupplyAndBalance_requireInvariant() {
    address receiver;
    uint256 amount;

    // previously: `require totalSupply() >= balanceOf(receiver)`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}


rule burn_decreasesTotalSupplyAndBalance_requireInvariant() {

    address holder;
    uint256 amount;

    // previously: `require totalSupply() >= balanceOf(holder)`
    requireInvariant totalSupplyEqualsSumOfBalances(); 

    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Ejecución del Prover: enlace

4. Acciones no autorizadas — métodos y llamadores que no tienen permitido cambiar el estado

Esto verifica que ciertos cambios de estado o acciones no deben ocurrir fuera de las funciones o llamadores explícitamente permitidos.

Solo ciertos métodos pueden cambiar el almacenamiento / estado

Comencemos con la propiedad: “Solo mint() y burn() pueden cambiar el total supply.”

La regla a continuación es una regla paramétrica (ver el capítulo “Introduction to Parametric Rules”) donde las funciones pueden ser llamadas arbitrariamente (vía f(e, args)), pero solo mint() y burn() tienen permitido cambiar el totalSupply. Esto es impuesto por la afirmación donde totalSupplyAfter != totalSupplyBefore implica (=>) que solo estas dos funciones pueden causar tal cambio:

Copy
rule onlyMethodsCanChangeTotalSupply(env e, method f, calldataarg args) {
    mathint totalSupplyBefore = totalSupply();

    f(e, args);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter != totalSupplyBefore => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:burn(address,uint256).selector
    );
}

Si bien esto afirma qué funciones tienen permitido modificar el totalSupply, también implica que todas las demás funciones no están autorizadas a hacerlo.

Las reglas restantes en esta categoría se muestran a continuación y siguen el mismo patrón:

• Solo mint(), burn(), transfer() y transferFrom() pueden cambiar los saldos de las cuentas:

  Copy
  rule onlyMethodsCanChangeAccountBalances(env e, method f, calldataarg args) {
      address account;
      mathint balanceBefore = balanceOf(account);
      
      f(e, args);
      mathint balanceAfter = balanceOf(account);
  
      assert balanceBefore != balanceAfter => (
          f.selector == sig:transfer(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector ||
          f.selector == sig:mint(address,uint256).selector ||
          f.selector == sig:burn(address,uint256).selector
      );
  }
  

• Solo approve() y transferFrom() pueden cambiar los allowances:

  Copy
  rule onlyMethodsCanChangeAllowance(env e, method f, calldataarg args) {
      address holder;
      address spender;
  
      mathint allowanceBefore = allowance(holder, spender);
  
      f(e, args);
      mathint allowanceAfter = allowance(holder, spender);
  
      assert allowanceAfter != allowanceBefore => (
          f.selector == sig:approve(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector
      );
  }
  

Ahora que hemos escrito las reglas que verifican qué métodos pueden modificar el estado, podemos escribir la regla que verifica qué llamadores están autorizados para reducir el saldo de un titular.

Solo los titulares y los gastadores pueden reducir el saldo de un titular

Otra acción no autorizada es reducir un saldo cuando el llamador no es el titular ni un gastador aprobado. La siguiente regla verifica esta propiedad:

Copy
rule onlyHolderAndSpenderCanReduceHolderBalance(env e, method f, calldataarg args) filtered {
	// `burn()` is excluded since permission checks are left to the integrator / developer
    f -> f.selector != sig:burn(address,uint256).selector                                                   
} {
    requireInvariant totalSupplyEqualsSumOfBalances(); 

    address account;

    mathint spenderAllowanceBefore = allowance(account, e.msg.sender);
	mathint holderBalanceBefore = balanceOf(account);
    
    f(e, args);
	mathint holderBalanceAfter = balanceOf(account);

    assert (holderBalanceAfter < holderBalanceBefore) => (
        e.msg.sender == account ||
        holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
    );
}

La línea a continuación establece que estamos excluyendo la función burn() en las llamadas paramétricas:

Copy
f -> f.selector != sig:burn(address,uint256).selector

burn() se filtra porque, como se mencionó anteriormente, se deja intencionalmente sin comprobaciones de permisos. Incluirlo en la regla causaría que falle, ya que cualquier llamador podría reducir el saldo de un titular, lo que frustraría la intención de la regla.

Ya cubrimos requireInvariant en la sección de invariantes, y estamos familiarizados con registrar el estado antes y después de una llamada a un método de las secciones anteriores, así que podemos saltar directamente a la afirmación.

La afirmación a continuación significa que si el saldo del titular disminuye, debe ser debido a una de dos razones:

• e.msg.sender == account

  El titular inició la acción, o

• holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)

  La reducción cae dentro de los límites de un allowance aprobado, lo que también significa que el llamador es un gastador aprobado con un allowance distinto de cero.

Copy
assert (holderBalanceAfter < holderBalanceBefore) => (
    e.msg.sender == account ||
    holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
);

Esta regla específica es una versión modificada de onlyAuthorizedCanTransfer de OpenZeppelin. El cambio es que en la regla original, sig:burn(address,uint256).selector estaba en la afirmación, mientras que en esta regla onlyHolderAndSpenderCanReduceHolderBalance lo hemos filtrado con filtered.

Aquí está la ejecución del Prover para todas las reglas en esta sección.

Especificación completa de CVL para ERC-20

Aquí está la especificación completa de CVL y la ejecución del Prover.

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