Hasta ahora, en los capítulos anteriores, hemos escrito reglas para verificar el comportamiento de métodos específicos y su impacto en el estado de un contrato. Por ejemplo:
- En el Capítulo 2, escribimos una regla para verificar que llamar a
increment()aumenta el valor decounten uno. - En el Capítulo 3, escribimos una regla para comprobar que llamadas secuenciales a
increment()ydecrement()deberían dar como resultado un valor decountsin cambios.
Pero, ¿qué pasa si queremos razonar sobre propiedades que deberían mantenerse verdaderas independientemente de qué función se llame? Por ejemplo, considere las siguientes propiedades:
- En un contrato de votación simple, el número total de votos siempre debe ser igual a la suma de los votos a favor y los votos en contra.
- En un contrato ERC-20, el saldo de un usuario nunca debe exceder el suministro total (total supply) del token.
En este capítulo, aprenderemos cómo escribir lo que se conoce como reglas paramétricas: reglas que nos permiten verificar formalmente propiedades que se espera que se mantengan verdaderas, independientemente de la función que se llame.
Introducción a las Reglas Paramétricas
En CVL, una regla estándar a menudo verifica las transiciones de estado después de la llamada a una función específica. Por lo general, se define qué transiciones de estado están permitidas usando un patrón como:
rule any_general_rule{
require <setup conditions>;
mySpecificFunction(arg1, arg2);
assert <expected outcome>;
}
Una regla paramétrica funciona de manera similar pero generaliza este concepto. En lugar de centrarse en una function(args), una regla paramétrica verifica que una propiedad se mantiene verdadera después de que cualquier función se llame con cualquier argumento válido.
Cómo maneja CVL “Cualquier Función, Cualquier Argumento”
Para expresar esta idea de “cualquier función con cualquier argumento válido”, CVL proporciona dos tipos especiales:
method: Representa cualquier función pública o externa dentro del contrato que está verificando. Declarar una variable de tipomethodsignifica que la regla puede referenciar y ejecutar dinámicamente cualquier función en el contrato.calldataarg: Representa los argumentos para una llamada a una función. Dado que diferentes funciones necesitan diferentes entradas,calldataarggarantiza que se proporcionen automáticamente argumentos válidos para cualquiera que sea la función (method) que se esté probando.
La Sintaxis de la Llamada Paramétrica
Estos dos tipos especiales nos permiten crear lo que llamamos una llamada paramétrica, la cual permite que una regla acceda y llame a cada método público o externo del contrato bajo verificación, utilizando la siguiente sintaxis:
rule someParametricRule() {
env e;
method f;
calldataarg args;
f(e,args)
//Any assert statement should go here
assert <property_1>;
assert <property_2>;
}
La línea f(e, args) se llama llamada paramétrica. Nos permite probar todas las funciones públicas o externas en el contrato en lugar de elegir una manualmente. Así es como funciona:
frepresenta cualquier función en el contrato. En lugar de especificar una función en particular, esta variable asegura que todas las funciones se prueben una por una.argsrepresenta un conjunto de valores de entrada válidos. Dado que diferentes funciones tienen diferentes parámetros, args asegura que se proporcione el tipo y número correctos de entradas para cada función.e: Proporciona el contexto ambiental necesario (como la dirección del remitente, el número de bloque) para la simulación de la llamada a la función.
Esencialmente, la línea f(e, args); le dice al Certora Prover: “Para cada función f en este contrato, ejecútala con argumentos válidos args en un entorno simulado e.”
Al colocar las declaraciones assert después de la línea f(e, args);, definimos propiedades que deben mantenerse verdaderas universalmente, una vez que finaliza cualquier llamada a una función. Esto hace que las reglas paramétricas sean ideales para verificar invariantes centrales y propiedades generales de seguridad de los contratos inteligentes.
Identificando Invariantes en ERC-20
Apliquemos lo que hemos aprendido para verificar formalmente un invariante de una implementación ERC-20 que se muestra a continuación:
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract RareToken {
uint8 public immutable decimals = 18;
uint256 public immutable totalSupply;
mapping(address => uint256) private balances;
mapping(address => mapping(address => uint256)) private allowances;
event Transfer(address indexed from, address indexed to, uint256 value);
event Approval(address indexed owner, address indexed spender, uint256 value);
constructor(uint256 _initialSupply) {
require(_initialSupply > 0, "Invalid initial supply");
totalSupply = _initialSupply * 10 ** uint256(decimals);
balances[msg.sender] = totalSupply;
emit Transfer(address(0), msg.sender, totalSupply);
}
function balanceOf(address account) public view returns (uint256) {
return balances[account];
}
function transfer(address recipient, uint256 amount) public returns (bool) {
require(recipient != address(0), "ERC20: transfer to zero address");
require(balances[msg.sender] >= amount, "Insufficient balance");
balances[msg.sender] -= amount;
balances[recipient] += amount;
emit Transfer(msg.sender, recipient, amount);
return true;
}
function approve(address spender, uint256 amount) public returns (bool) {
require(spender != address(0), "ERC20: approve to zero address");
allowances[msg.sender][spender] = amount;
emit Approval(msg.sender, spender, amount);
return true;
}
function allowance(address owner_, address spender) public view returns (uint256) {
return allowances[owner_][spender];
}
function transferFrom(
address sender,
address recipient,
uint256 amount
) public returns (bool) {
require(recipient != address(0), "ERC20: transfer to zero address");
require(balances[sender] >= amount, "Insufficient balance");
uint256 currentAllowance = allowances[sender][msg.sender];
require(currentAllowance >= amount, "ERC20: insufficient allowance");
if (currentAllowance != type(uint256).max) {
allowances[sender][msg.sender] = currentAllowance - amount;
}
balances[sender] -= amount;
balances[recipient] += amount;
emit Transfer(sender, recipient, amount);
return true;
}
}
Como hemos aprendido, el propósito de escribir reglas paramétricas es verificar propiedades de los contratos inteligentes que siempre deberían mantenerse verdaderas a través de diferentes llamadas a funciones. En el caso de nuestro contrato RareToken, un invariante clave es: La Estabilidad del Suministro Total.
Dado que el contrato no incluye funcionalidad de mint o burn, el suministro total se inicializa una vez en el despliegue y debe permanecer constante durante toda la vida útil del contrato. En otras palabras, ninguna función debería modificar jamás el valor devuelto por totalSupply().
Veamos cómo podemos escribir una regla paramétrica para verificar la integridad del suministro total.
Verificando Formalmente la Consistencia del Suministro Total
Una vez que hemos identificado los invariantes clave del contrato que queremos verificar, siga estos pasos para escribir una regla paramétrica:
1. Definir la Regla
Use la palabra clave rule, seguida de un nombre descriptivo para la regla:
rule totalSupplyIsConstant() { }
2. Declarar el Entorno de Ejecución
Defina una variable env para representar el entorno de ejecución de la función:
rule totalSupplyIsConstant() {
env e;
}
3. Capturar el Estado Previo a la Llamada
Dado que necesitamos comparar el valor de totalSupply antes y después de la ejecución de la función, almacenamos su estado inicial:
rule totalSupplyIsConstant() {
env e;
mathint beforeSupply = totalSupply(e);
}
4. Modelar la Ejecución de la Función
Declare una variable method para representar cualquier llamada a una función y defina los arguments que podrían pasarse:
rule totalSupplyIsConstant() {
env e;
mathint beforeSupply = totalSupply(e);
method f;
calldataarg args;
f(e, args); // Execute the function call with the given arguments
}
5. Capturar el Estado Posterior a la Llamada
Después de ejecutar la función, almacenaremos el valor actualizado de totalSupply:
rule totalSupplyIsConstant() {
env e;
mathint beforeSupply = totalSupply(e);
method f;
calldataarg args;
f(e, args);
mathint afterSupply = totalSupply(e);
}
6. Imponer la Consistencia del Suministro Total
En el caso de nuestro contrato RareToken, queremos asegurarnos de que la variable totalSupply nunca cambie después de la ejecución de ninguna función. Usamos la declaración assert (assert beforeSupply == afterSupply) para imponer explícitamente esta condición:
rule totalSupplyIsConstant() {
env e;
mathint beforeSupply = totalSupply(e);
method f;
calldataarg args;
f(e, args);
mathint afterSupply = totalSupply(e);
assert beforeSupply == afterSupply;
}
Ejecutando la Verificación
Para ver los resultados de nuestra regla paramétrica, aplique lo que aprendió en los capítulos anteriores: coloque el contrato RareToken y la especificación correspondiente en el entorno del Certora Prover.
Una vez que la configuración esté completa, inicie el proceso de verificación. Si el contrato cumple con todas las condiciones definidas por la regla, el Certora Prover confirmará una ejecución de verificación exitosa sin violaciones detectadas, como se muestra en la imagen a continuación:
Los resultados de la verificación confirman que todas las funciones en el contrato RareToken fueron probadas contra la regla totalSupplyIsConstant(). Las marcas de verificación verdes (✅) junto a cada función indican que la regla se cumple para cada ejecución posible, asegurando que la variable totalSupply permanezca sin cambios bajo cualquier llamada a una función.
Entendiendo el Alcance de una Regla Paramétrica
Una cosa importante a entender sobre una regla paramétrica es que está diseñada para analizar el efecto de solo una llamada a la función a la vez. Eso significa que el Prover no está comprobando lo que sucede después de una serie de llamadas; solo se ocupa de una única llamada a una función y de cómo se ve el estado del contrato inmediatamente después de eso.
Esto es lo que sucede cuando el Prover evalúa una regla paramétrica:
- Comienza desde un estado inicial del contrato: este es el estado antes de que se haya llamado a cualquier función.
- Selecciona una función del contrato y comprueba si —bajo las precondiciones dadas— existe alguna entrada válida que pudiera llevar a una violación de las aserciones de la regla.
- Este proceso se repite para cada función en el contrato.
- La regla pasa la verificación (✅) solo si ninguna de las funciones, bajo ninguna entrada válida, causa que falle una aserción.
Para comprender más claramente el proceso de evaluación de una regla paramétrica, considere el contrato Counter. Incluye dos funciones externas: increment(), que aumenta el count, y transferOwnership(), que actualiza la dirección del propietario. La funcionalidad relacionada con la propiedad se incluye simplemente para introducir funciones adicionales, de modo que podamos observar cómo se comporta una regla paramétrica cuando se aplica a través de una variedad de tipos de funciones.
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Counter {
uint256 public count;
address public owner;
// Define custom errors
error Unauthorized();
error InvalidAddress();
// Emit events for important state changes
event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);
event CountUpdated(uint256 newCount);
constructor() {
owner = msg.sender;
emit OwnershipTransferred(address(0), msg.sender);
}
modifier onlyOwner() {
if (msg.sender != owner) revert Unauthorized();
_;
}
function increment() external {
count += 1;
emit CountUpdated(count);
}
function transferOwnership(address _newOwner) external onlyOwner {
if (_newOwner == address(0)) revert InvalidAddress();
emit OwnershipTransferred(owner, _newOwner);
owner = _newOwner;
}
}
Ahora considere la especificación a continuación que define una regla paramétrica llamada counterParametricCall().
rule counterParametricCall() {
env e;
require count(e) == 0;
method f;
calldataarg args;
f(e,args);
satisfy count(e) == 2 ;
}
Dado que nuestra regla counterParametricCall() incluye la declaración satisfy satisfy count(e) == 2;, le estamos preguntando al Prover si hay al menos una forma posible de alcanzar un estado donde count es 2, comenzando desde un estado inicial donde count es 0.
Pero hay más que eso: la regla también incluye una llamada a función paramétrica (f(e, args)) entre las declaraciones require y satisfy. Esto cambia la pregunta de una comprobación de alcanzabilidad general a una consulta más enfocada:
“¿Existe alguna función individual f en el contrato tal que, cuando se ejecuta una vez con algunos argumentos válidos args__, transicione el estado directamente de count == 0 a count == 2?”
En el caso de nuestro contrato Counter, la única función disponible es increment(), la cual aumenta el contador en 1 por llamada. Dado que ninguna función puede aumentar el contador en 2 en una sola ejecución, el Prover no puede encontrar ninguna función que satisfaga la condición count(e) == 2.
Por lo tanto, la regla fallará la verificación, lo cual es el resultado esperado y correcto, como se ilustra a continuación:
Es muy crucial tener en cuenta que una regla paramétrica solo analiza el efecto de una llamada a una función externa de forma aislada. No examina secuencias de llamadas o interacciones complejas dentro de una sola transacción. Por ejemplo, mientras que la regla anterior demuestra que ninguna llamada individual puede hacer que count == 2, es posible llegar a count == 2 dentro de una transacción si otro contrato inteligente llamara a la función increment() dos veces en secuencia. Ese escenario implica múltiples llamadas a funciones iniciadas dentro de una sola transacción, lo cual está fuera del alcance de este capítulo.
Sin embargo, incluso si relajáramos la regla para comprobar satisfy count(e) == 1 en lugar de satisfy count(e) == 2, la regla aún no pasaría, como se muestra a continuación:
Esto sucedió porque, internamente, al evaluar una regla paramétrica, el Prover crea una instancia de la regla para cada función en el contrato. Prueba cada una de estas instancias de regla individualmente contra las aserciones. La regla pasa la verificación si y solo si cada instancia de la función satisface todas las condiciones especificadas por las declaraciones assert y satisfy. Si incluso una función no cumple con los criterios, toda la regla falla.
En el contrato Counter, solo la función increment() modifica la variable count, convirtiéndola en el único candidato que potencialmente puede satisfacer la condición satisfy (por ejemplo, count == 1). Por el contrario, transferOwnership() y las funciones getter count() y owner() no afectan a count en absoluto. Cuando el Prover evalúa la regla para estas funciones, encuentra que ninguna de ellas puede producir el cambio de estado requerido. Como resultado, sus instancias de regla fallan, y como todas las instancias deben pasar para que la regla tenga éxito, toda la regla falla la verificación.
Resumen
Así es como podemos usar una regla paramétrica para verificar propiedades de los contratos inteligentes que se espera que se mantengan verdaderas en todas las ejecuciones de funciones. Sin embargo, hay casos en los que podríamos querer excluir ciertas funciones de la regla o manejarlas de manera diferente. En el próximo capítulo, aprenderemos cómo ajustar finamente las reglas paramétricas para imponer restricciones selectivamente basadas en llamadas a funciones específicas.
Este artículo es parte de una serie sobre verificación formal usando el Certora Prover