Hasta ahora, nos hemos centrado en verificar el comportamiento de métodos individuales o secuencias de métodos — asegurando que una llamada de función específica o un conjunto de llamadas, dadas ciertas entradas, produzca los cambios de estado correctos. Pero hay otro aspecto más universal de la verificación: los invariantes.
Los invariantes son condiciones que siempre deben ser verdaderas para el estado del contrato, sin importar qué función se llame o en qué orden. Si alguna ejecución — ya sea directa o a través de una secuencia de llamadas — viola un invariante, indica una falla fundamental en el diseño del contrato, exponiendo potencialmente un error o vulnerabilidad.
En este artículo, exploraremos cómo especificar formalmente y verificar tales propiedades utilizando el constructo invariant incorporado en CVL de Certora.
Definiendo invariantes en CVL
El constructo invariant incorporado de CVL es un mecanismo de especificación formal que permite a los desarrolladores definir propiedades universales (invariantes) que deben mantenerse a lo largo de la vida útil de un contrato inteligente, es decir, desde el momento en que se ejecuta el constructor hasta cualquier estado que el contrato pueda alcanzar en el futuro.
Los invariantes en CVL se definen utilizando la palabra clave invariant, seguida de un nombre único (identificador), parámetros opcionales y una expresión booleana que describe la condición que siempre debe ser verdadera, como se muestra a continuación:
invariant invariant_name(optional_parameter_1, optional_parameter_2, ...)
boolean_expression_in_CVL;
Se considera que un invariante se cumple y se reporta como verificado (✅) si su expresión booleana, definida en el invariante, se evalúa como true en cada estado alcanzable del contrato y para todos los valores posibles de sus parámetros. Exploraremos el proceso de verificación de invariantes con más detalle más adelante en este capítulo.
Cómo difieren los invariantes de las reglas
Una regla en CVL está diseñada para comprobar si una propiedad específica se cumple dentro de un escenario definido: comenzando desde un estado determinado, realizando ciertas acciones y luego verificando un resultado.
rule check_balance_updates(env e) {
// 1. Starting State
address user = e.msg.sender;
uint initial_balance = balanceOf(user);
// 2. Actions
uint amount;
deposit(amount); // Call the deposit function
// 3. Outcome Check
uint final_balance = balanceOf(user);
assert final_balance == initial_balance + amount, "Deposit did not correctly update balance";
}
En otras palabras, responde a la pregunta: “¿Esta acción en particular (o secuencia de acciones) conduce al resultado esperado?”
A diferencia de las reglas, que se centran en escenarios específicos, un invariante en CVL expresa una condición que siempre debe ser verdadera en cada estado alcanzable del contrato, independientemente de qué funciones se llamen o en qué orden.
A continuación se muestra un ejemplo de un invariante simple que establece que el valor de count nunca debe volverse negativo:
invariant count_cannot_be_negative()
count() >= 0;
En pocas palabras, responde a la pregunta: “¿Es esta condición universalmente verdadera, independientemente de cómo se use el contrato?"
Cuándo usar Invariantes vs. Reglas
Decidir si usar una regla o un invariante en CVL depende de la naturaleza de la propiedad que pretendemos verificar.
Cuándo usar una Regla: Verificando escenarios específicos
Opte por una regla cuando su objetivo sea verificar el comportamiento dentro de un contexto definido o una secuencia específica de operaciones. Por ejemplo:
- La función
withdraw(amount)debe deducir correctamente elamountdel saldo de quien llama y transferirlo, pero solo sibalanceOf(caller) >= amount. - Verificar que un intento de hacer
mintmás allá de un límite máximo de suministro se revierte (reverts) correctamente. - Comprobar que una función de administrador solo puede ser llamada con éxito por la dirección de administrador designada.
En esencia, las reglas son su método principal para responder: “¿Esta función (o secuencia de funciones) funciona correctamente en esta situación particular?”
Cuándo usar un Invariante: Imponiendo verdades fundamentales
Elija un invariante cuando desee verificar una propiedad que debe cumplirse en cada estado posible y en cada secuencia posible de llamadas a funciones. Por ejemplo:
- En una implementación de ERC-20, el
totalSupplysiempre debe ser igual a la suma de todos los saldos individuales de los usuarios. - En un protocolo de préstamos, el valor total del colateral siempre debe ser mayor o igual a un cierto porcentaje de la deuda total, asumiendo que las liquidaciones funcionan correctamente.
- En un contrato de tokens, el saldo de un usuario nunca puede volverse negativo.
Los invariantes proporcionan las garantías más sólidas sobre la integridad a largo plazo y la seguridad del estado de su contrato. Responden a la pregunta crítica: “¿Es inquebrantable esta propiedad fundamental de mi contrato, pase lo que pase?”
Alcance de la verificación: Rules vs Invariants
Al verificar una regla, el Prover comprueba si las aserciones se cumplen para el escenario específico definido en la regla — basado en el estado inicial, las acciones realizadas y cualquier suposición. Las reglas ofrecen flexibilidad para explorar rutas personalizadas o casos límite, pero solo verifican la corrección a lo largo de las rutas de ejecución construidas explícitamente en la especificación.
Por el contrario, un invariante debe cumplirse independientemente de qué funciones se llamen, con qué parámetros o en qué orden. El Prover debe asegurarse de que el invariante se mantenga en cada estado alcanzable del contrato. Esto se logra mediante un principio de demostración en dos partes basado en inducción matemática:
- Caso base: La propiedad debe cumplirse inmediatamente después del despliegue del contrato — es decir, debe ser establecida por el constructor.
- Paso inductivo: Para cada función pública o externa en el contrato, si la propiedad se cumple antes de que se llame a la función, debe seguir cumpliéndose después de la llamada a la función.
Si tanto el caso base como el paso inductivo son probados, el prover reporta el invariante como verificado (✅).
Escribiendo un Invariante en Certora
Para entender cómo funciona la verificación de invariantes en la práctica, veamos el contrato simple Voting de la documentación de Certora :
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
/// @title A simple voting contract
contract Voting {
// `hasVoted[user]` is true if the user voted.
mapping(address => bool) public hasVoted;
uint256 public votesInFavor; // keep the count of votes in favor
uint256 public votesAgainst; // keep the count of votes against
uint256 public totalVotes; // keep the count of total votes cast
/// @notice Allows a user to vote in favor of the proposal.
function voteInFavor() external {
// Ensure the user has not already voted
require(!hasVoted[msg.sender], "You have already voted.");
hasVoted[msg.sender] = true;
votesInFavor += 1;
totalVotes += 1;
}
/// @notice Allows a user to vote against the proposal.
function voteAgainst() external {
// Ensure the user has not already voted
require(!hasVoted[msg.sender], "You have already voted.");
hasVoted[msg.sender] = true;
votesAgainst += 1;
totalVotes += 1;
}
}
El contrato Voting anterior permite a los usuarios emitir un solo voto, ya sea a favor o en contra de una propuesta. Para evitar el doble voto, el contrato utiliza un mapping hasVoted que registra si una dirección ya ha participado. Rastrea los votos a través de tres contadores separados: votesInFavor, votesAgainst y totalVotes. Cuando un usuario emite un voto utilizando las funciones voteInFavor() o voteAgainst(), el contador apropiado se incrementa y el estado de hasVoted se actualiza.
Identificando el invariante clave en el contrato Voting
Dado que nuestro objetivo es verificar formalmente los invariantes de nuestro contrato Voting, primero necesitamos identificar sus propiedades clave. Al observar nuestro contrato Voting, uno de los invariantes cruciales es que el número total de votos siempre debe ser igual a la suma de los votos a favor y los votos en contra.
Con este invariante clave identificado, repasemos el proceso de especificarlo y verificarlo formalmente utilizando Certora.
Configurando el entorno de tu proyecto
Para comenzar a verificar nuestro invariante, primero necesitamos configurar la estructura y el entorno de nuestro proyecto. Para hacerlo, sigue las instrucciones a continuación:
- Crea un directorio vacío llamado
certora-invariants-examplesy navega hacia él. - Dentro del directorio de tu proyecto, crea un entorno virtual de Python para el proyecto ejecutando el siguiente comando.
virtualenv certora-env
- Activa el entorno virtual de Python que creaste ejecutando el comando a continuación.
source certora-env/bin/activate
- Ejecuta el comando a continuación para instalar Certora-CLI en tu entorno virtual.
pip3 install certora-cli
- Ejecuta el comando a continuación para instalar solc-select en tu entorno virtual.
pip3 install solc-select
- En el directorio de tu proyecto, crea tres subdirectorios llamados
contracts,specsyconfs. - En el directorio de tu proyecto, navega a la subcarpeta
contractsy crea un archivo llamadoVoting.sol. Luego, pega el contratoVotingdiscutido anteriormente en ese archivo.
Definiendo el invariante en un archivo de especificación
Una vez que el entorno del proyecto esté listo, el siguiente paso es crear un archivo de especificación donde definiremos nuestro invariante.
1. Crear un archivo de especificación: En el directorio de tu proyecto, navega a la subcarpeta specs y crea un archivo de especificación (p. ej., invariant.spec). Este archivo contendrá tus reglas de CVL, incluyendo los invariantes que deseas verificar.
2. Declarar el invariante: Dentro de tu archivo de especificación, usa la palabra clave invariant para definir un invariante. Asígnale un nombre descriptivo que exprese claramente qué comprueba la regla.
invariant totalVotesMatch()
3. Insertar la condición del invariante como una expresión de CVL: A continuación, especifica la condición que siempre debe ser verdadera. En el caso del contrato Voting, queremos asegurarnos de que el número total de votos siempre sea igual a la suma de los votos a favor y los votos en contra:
invariant totalVotesMatch()
to_mathint(totalVotes()) == votesInFavor() + votesAgainst();
Nota: to_mathint se usa para convertir el tipo uint256 de Solidity en enteros matemáticos de Certora para una comparación segura. No es necesario aplicarlo al lado derecho de la ecuación, porque en CVL, los resultados de todas las operaciones aritméticas son automáticamente de tipo mathint.
4. Agregar el bloque de métodos (Methods Block): A continuación, agreguemos un bloque de métodos en la parte superior de nuestra especificación con las entradas correctas.
methods {
function totalVotes() external returns(uint256);
function votesInFavor() external returns(uint256);
function votesAgainst() external returns(uint256);
}
invariant totalVotesMatch()
to_mathint(totalVotes()) == votesInFavor() + votesAgainst();
Declarar funciones como envfree: Dado que las funciones getter votesInFavor(), votesAgainst() y totalVotes() no dependen del entorno de ejecución (es decir, no leen de msg.sender, msg.value ni de ninguna otra variable global), podemos declararlas como envfree.
methods {
function totalVotes() external returns(uint256) envfree;
function votesAgainst() external returns(uint256) envfree;
function votesInFavor() external returns(uint256) envfree;
}
invariant totalVotesMatch()
to_mathint(totalVotes()) == votesInFavor() + votesAgainst();
Ejecutando la Verificación
Una vez que el directorio de tu proyecto esté configurado correctamente, sigue los pasos a continuación para ejecutar el Certora Prover y verificar tu invariante.
1. Crear un archivo de configuración: En la subcarpeta confs, crea un archivo de configuración (p. ej., invariant.conf) y pega el código a continuación en él.
{
"files": [
"contracts/Voting.sol:Voting"
],
"verify": "Voting:specs/invariant.spec",
"msg": "Testing Invariant"
}
2. Añadir la clave de acceso personal de Certora: En el directorio de tu proyecto, crea un archivo .profile, .bashrc o .zshenv (dependiendo de tu sistema operativo y shell) y añade la siguiente línea para configurar tu Certora Personal Access Key como una variable de entorno.
#certora access key
export CERTORAKEY=<add-your-certora-access-key-here>
3. Cargar la variable de entorno: Después de añadir la clave, carga las variables de entorno en tu sesión actual de terminal ejecutando el comando apropiado que se muestra a continuación.
# For bash users
source .profile
# For zsh users
source .zshenv
4. Añadir el compilador de Solidity: Antes de ejecutar el Prover, necesitamos añadir el compilador de Solidity correcto. Para añadir y usar la versión correcta del compilador de Solidity, ejecuta los comandos a continuación.
solc-select install 0.8.25
solc-select use 0.8.25
5. Ejecutar el Prover: Para verificar tu invariante, ejecuta el siguiente comando desde el directorio raíz de tu proyecto.
certoraRun confs/invariant.conf
Si el Prover compila tu contrato inteligente y el archivo de especificación correctamente — sin encontrar errores sintácticos o semánticos, generará un enlace al informe de verificación y lo imprimirá en la salida de tu terminal.
Para ver el resultado de la verificación, abre el enlace impreso en tu terminal utilizando un navegador. Los resultados deberían verse similares a la imagen a continuación:
Nota: Dependiendo de la complejidad de tu especificación y de la cola actual del Prover, puede tardar unos minutos para que el estado de tu trabajo cambie de Queued (En cola) a Executed (Ejecutado). Este retraso es normal, así que no te preocupes.
El resultado de verificación mostrado arriba confirma que el Prover ha validado exitosamente nuestro invariante. Esto significa que, basándose en el análisis, no se encontró ningún escenario donde el invariante pudiera romperse, indicando que se cumple consistentemente en todo el comportamiento del contrato.
Para entender mejor qué significa que un invariante sea “validado exitosamente”, examinemos cómo el Prover verifica los invariantes entre bastidores.
¿Cómo se verifican los invariantes?
Cuando se envía un invariante para su verificación, el Prover realiza dos comprobaciones esenciales para asegurar su corrección, que corresponden directamente al principio de demostración de dos partes (basado en inducción matemática) discutido anteriormente:
- Comprobación del estado inicial: Primero, el Prover verifica que el invariante se cumple inmediatamente después de que el constructor del contrato termine de ejecutarse. Este es el Caso base de nuestra demostración inductiva.
- Paso inductivo: A continuación, el Prover comprueba que cada método público y externo preserve el invariante a lo largo de su ejecución. Esto corresponde al Paso inductivo, asegurando que si la propiedad se cumple antes de la llamada a una función, continúa cumpliéndose después.
El resultado de ambas comprobaciones se puede ver expandiendo el invariante totalVotesMatch() en el panel izquierdo de la interfaz de usuario del Prover.
El resultado de la comprobación del estado inicial se muestra debajo de “Induction base: After the constructor”, confirmando que el contrato comienza en un estado válido donde el invariante se cumple.
El resultado del Paso inductivo se muestra debajo de “Induction step: after external (non-view) methods”. Esta parte de la prueba está diseñada para demostrar que todas las funciones públicas y externas preservan el invariante.
Entonces, ¿por qué el informe solo muestra métodos “non-view” (que cambian el estado)?
Esta es una optimización inteligente por parte del Prover. El compilador de Solidity garantiza que las funciones view y pure no cambian el estado del contrato. La lógica es la siguiente:
- Asumimos que el invariante se cumple antes de cualquier llamada a función (la hipótesis de inducción).
- Se llama a una función
view. - Dado que el estado del contrato permanece idéntico, el invariante debe seguir cumpliéndose después de la llamada.
Debido a que las funciones view y pure nunca cambian el estado del contrato, no hay necesidad de verificarlas nuevamente durante el paso inductivo. Su corrección ya está garantizada por la comprobación de la base de inducción que confirma que el contrato comienza en un estado válido. Omitir estas comprobaciones redundantes ayuda al Prover a ahorrar recursos de verificación y eliminar el desorden innecesario del informe.
La comprobación del paso inductivo, por lo tanto, se centra en los métodos que pueden cambiar el estado.
En nuestro caso, tanto voteAgainst() como voteInFavor() son analizados bajo esta comprobación. Las marcas de verificación verdes (✅) al lado de cada función indican que, cuando se invocan estos métodos, no violan el invariante. Esto confirma que la lógica del contrato preserva correctamente el invariante a través de todas las operaciones que cambian el estado.
Además de estas dos comprobaciones principales, el Prover también ejecuta una regla llamada envFreeFuncsStaticCheck, que verifica que todas las funciones marcadas como envfree en la especificación son verdaderamente independientes del entorno de ejecución, como msg.sender o msg.value.
Comprendiendo las comprobaciones adicionales en la interfaz de usuario del Prover
Si estás utilizando una versión más nueva de Certora Prover, es posible que notes entradas adicionales al expandir el resultado de un invariante en la interfaz de usuario del Prover, como rule_not_vacuous e invariant_not_trivial_postcondition, como se muestra a continuación:
Estas entradas adicionales son comprobaciones automáticas de cordura (sanity checks) añadidas por el propio Prover. No son algo que hayas escrito tú, y no significan que se estén verificando invariantes o reglas adicionales. Su propósito es asegurar que tu invariante sea genuinamente significativo y no se satisfaga de forma trivial.
Nota: A partir de la versión v8.1.0 de Certora Prover, las comprobaciones básicas de cordura se ejecutan de forma predeterminada (equivalente a establecer "rule_sanity": "basic"). Anteriormente, el valor predeterminado era "none". Puedes controlar este comportamiento utilizando la opción de línea de comandos (CLI) --rule_sanity o añadiendo "rule_sanity": "none" a tu archivo de configuración para desactivar estas comprobaciones. Para una explicación detallada de todas las comprobaciones de cordura disponibles, consulta la documentación de Rule Sanity Checks.
Qué verifican estas comprobaciones:
rule_not_vacuous: Confirma que el invariante se está evaluando realmente bajo condiciones realistas. Un resultado “vacuous” (vacío) significaría que el invariante se cumple solo porque las precondiciones nunca se satisfacen — esencialmente, nunca se prueba verdaderamente.invariant_not_trivial_postcondition: Asegura que la condición del invariante no es trivialmente verdadera independientemente del estado del contrato (por ejemplo, una expresión que siempre se evalúa comotrue).
Estas comprobaciones adicionales no alteran el proceso de verificación principal. El Prover sigue realizando la misma prueba inductiva en dos partes: verificando que el invariante se cumpla después del constructor (caso base) y que cada función que cambia el estado lo preserve (paso inductivo). Las comprobaciones de cordura simplemente proporcionan una confianza adicional de que tus resultados de verificación son significativos y no son artefactos de errores de especificación.
Conclusión
Los invariantes de contratos inteligentes son aserciones críticas sobre el estado de tu contrato que siempre deben mantenerse verdaderas. Verificar formalmente estos invariantes asegura que el contrato mantenga su comportamiento esperado y su corrección en todos los estados posibles y ejecuciones de métodos.
Este artículo es parte de una serie sobre verificación formal utilizando Certora Prover