Cómo auditar un contrato sin jugar al checklist teatral

Imagina que tu equipo recibe un contrato de 300 líneas y una semana para revisarlo. La tentación es abrir el código por la primera función y anotar todo lo que "huele raro". Al final de la semana hay cuarenta notas y nadie sabe cuál importa. Este capítulo propone otro orden: primero decidir qué se protege y de quién, después escribir las propiedades que nunca deben romperse y, solo entonces, buscar la secuencia de llamadas que las rompe.

La documentación de ethereum.org lo dice sin rodeos: una auditoría es una ronda adicional de revisión, no una bala de plata, y no va a encontrar todos los errores. [1] Por eso el objetivo no es "aprobar" el contrato. El objetivo es dejar al equipo con hallazgos reproducibles, pruebas que sigan corriendo en CI y una lista honesta de lo que no se revisó.

Preguntas guía

• Si mañana alguien drena el contrato, ¿qué propiedad escrita habría fallado primero?
• ¿Qué cuentas tienen privilegios y qué pueden hacer con ellos en una sola transacción?
• ¿Cada hallazgo trae estado inicial, secuencia de llamadas y resultado observable?
• ¿Qué parte del sistema quedó fuera del alcance y quién la va a revisar?

Conexiones dentro de la serie

• Antes: Oráculos: datos externos con dientes, porque muchos hallazgos graves viven en supuestos de precio.
• Base de pruebas: Testing serio: unit, fork, fuzz e invariantes explica las herramientas que aquí se usan como método de auditoría.
• Patrones de fallo: Reentrancy y Access control son las dos familias que más aparecen en el ejemplo.
• Después: "Ethereum 2" ya no es el nombre: execution y consensus layer abre el bloque de consenso.

Antes de leer código: alcance, activos y quién gana

Empieza con una pregunta concreta: si este contrato guarda ETH de usuarios, ¿quién podría llevárselo? La respuesta define el alcance. Un alcance útil enumera tres cosas: los activos (ETH, tokens, permisos de mint, parámetros de comisión), los actores (usuario, admin, contrato externo, cualquiera que llame) y los commits exactos que se revisan. Si el commit cambia, la auditoría ya habla de otro código.

El modelo de amenazas, o threat model, es la lista de actores con un incentivo y una capacidad. "Un usuario cualquiera puede llamar a withdraw con un contrato propio" es una amenaza. "Un hacker podría hacer algo" no lo es, porque no dice qué llamada hace ni qué gana.

Las funciones public y external pueden ser llamadas por cualquier cuenta, sea una persona o un contrato. [1] Esa frase es la base del modelo: cada función externa es una puerta, y el auditor anota quién puede cruzarla y con qué argumentos. Las funciones protegidas por un rol se anotan aparte, junto con quién controla ese rol.

El resultado de esta fase cabe en una página. Si no cabe, el sistema es demasiado grande para una sola pasada y conviene partirlo.

Invariantes como tesis de auditoría

Una invariante es una afirmación sobre el estado que debe ser cierta después de cualquier secuencia de llamadas. Es la forma más corta de decir qué significa "seguro" para este contrato. Toma este vault mínimo, escrito para el ejercicio:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
 
/// Ejemplo didáctico para auditoría. No usar en producción.
contract MiniVault {
    mapping(address => uint256) public balanceOf;
    uint256 public totalDeposits;
 
    function deposit() external payable {
        balanceOf[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }
 
    function withdraw(uint256 amount) external {
        require(balanceOf[msg.sender] >= amount, "saldo insuficiente");
        balanceOf[msg.sender] -= amount;   // efecto antes de la interacción
        totalDeposits -= amount;
        (bool ok, ) = msg.sender.call{value: amount}("");
        require(ok, "envio fallido");
    }
}

La invariante de solvencia dice: el saldo en ETH del contrato es mayor o igual que totalDeposits. Fíjate en el "mayor o igual". La documentación de Solidity recuerda que un contrato no puede impedir que le envíen Ether: hay formas de moverlo sin una llamada a función, como selfdestruct o ser el destinatario de recompensas de bloque. [2] Una invariante con igualdad estricta fallaría por una razón que no es un bug del vault.

El orden de withdraw sigue el patrón Checks-Effects-Interactions: primero valida, después actualiza el estado y al final llama a la cuenta externa. [2] Si un auditor ve la llamada antes de la resta, ya tiene una hipótesis de reentrancy que probar, no una sospecha vaga.

Traza de ejecución de un hallazgo: de la propiedad al PoC

Escribir la invariante en código convierte la tesis en algo que una máquina intenta romper. La documentación de ethereum.org describe este enfoque como pruebas basadas en propiedades: el programa genera muchas entradas y busca una traza que viole la propiedad, en lugar de que el humano escriba cada caso. [3]

En Foundry, una función cuyo nombre empieza por invariant (o statefulFuzz) se trata como prueba de invariante. [4] El fuzzer llama en orden aleatorio a las funciones de los contratos objetivo y, después de cada llamada, comprueba la invariante. Con targetContract se le dice a qué contrato llamar. [5] El siguiente archivo compila con solc 0.8.30 contra forge-std; ejecútalo con forge test en un proyecto Foundry:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
 
import {Test} from "forge-std/Test.sol";
import {MiniVault} from "../src/MiniVault.sol";
 
/// El handler limita las acciones del fuzzer a secuencias con sentido.
contract Handler is Test {
    MiniVault public vault;
 
    constructor(MiniVault _vault) {
        vault = _vault;
    }
 
    function deposit(uint256 amount) external {
        amount = bound(amount, 0, 100 ether);
        vm.deal(address(this), amount);
        vault.deposit{value: amount}();
    }
 
    function withdraw(uint256 amount) external {
        amount = bound(amount, 0, vault.balanceOf(address(this)));
        vault.withdraw(amount);
    }
 
    receive() external payable {}
}
 
contract MiniVaultInvariants is Test {
    MiniVault internal vault;
    Handler internal handler;
 
    function setUp() public {
        vault = new MiniVault();
        handler = new Handler(vault);
        targetContract(address(handler));
    }
 
    /// Solvencia: el contrato siempre puede pagar lo que debe.
    function invariant_solvencia() public view {
        assertGe(address(vault).balance, vault.totalDeposits());
    }
}

El handler es un contrato intermedio que acota los argumentos con bound para que el fuzzer no pierda tiempo en llamadas que siempre revierten. Si alguien mueve la resta de withdraw después de la llamada externa, el fuzzer no llega solo a la reentrancy porque el handler no reentra. Ese es el trabajo del auditor: añadir un actor atacante al handler cuando el modelo de amenazas lo pide.

Figura 1

El ciclo de auditoría: de alcance a retest

Fuentes:

[3][1]

Cómo leer esta figura

Seis cajas en dos filas. Arriba, de izquierda a derecha: Alcance (activos, actores, permisos), Modelo de amenazas (quién gana si algo falla) e Invariantes (lo que nunca debe romperse). Una flecha baja desde Invariantes a Revisión manual más fuzz e invariantes. Abajo, de derecha a izquierda: Revisión manual, Hallazgo (estado, secuencia, PoC) y Corrección y retest (la prueba pasa a CI). Una flecha ocre vuelve desde Corrección y retest hasta Revisión manual con la etiqueta: cada diff nuevo vuelve a ejecutar las invariantes. Una nota al margen dice: si una propiedad no se puede escribir, el alcance está mal.

Descargar SVGDescargar .tex

Código TikZ

Abrir `.tex` en otra pestaña

Anatomía de un hallazgo y su severidad

Un hallazgo accionable responde cuatro preguntas: desde qué estado se parte, qué secuencia de llamadas ejecuta el atacante, qué propiedad se rompe y cuánto cuesta. Si falta la secuencia, es una sospecha. Si falta la propiedad, es una opinión de estilo.

La severidad combina impacto y probabilidad. No hay una escala universal; cada firma publica la suya. Como regla de razonamiento, una pérdida de fondos que cualquiera puede ejecutar sin permisos pesa más que la misma pérdida que exige comprometer la clave del admin. La segunda sigue siendo un hallazgo, pero el arreglo suele estar en la operación (multisig, timelock) y no en el código.

Riesgo operativo después del informe

La corrección también se audita. Una corrección típica de reentrancy es reordenar a Checks-Effects-Interactions o añadir un guard; OpenZeppelin ofrece ReentrancyGuard y una variante con almacenamiento transitorio, ReentrancyGuardTransient. [6] Añadir un guard sin entender qué función reentraba puede bloquear un flujo legítimo, así que el retest repite la prueba del hallazgo y todas las invariantes.

El informe caduca en cuanto cambia el código, los parámetros o una integración. Por eso las invariantes escritas durante la auditoría se quedan en el repositorio y corren en cada pull request. Lo que no se pudo convertir en prueba se anota como riesgo residual, con nombre y responsable.

Hay riesgos que el código no puede cerrar: una clave de admin en un portátil, un oráculo manipulable o una dependencia sin auditar. ethereum.org propone complementar las auditorías con programas de bug bounty, recompensas para quien reporte vulnerabilidades de forma responsable. [1] El auditor no los resuelve todos; sí debe nombrarlos para que no queden fuera por omisión.

Para practicar, reescribe withdraw como el contrato Victim de ethereum.org: lee el saldo del usuario, envía el ETH y solo después lo pone a cero. [1] Después añade al handler un actor atacante cuyo receive vuelva a llamar a withdraw.

Verás algo incómodo: si totalDeposits también se resta dos veces, saldo y total bajan a la vez y la invariante de solvencia sigue pasando. La lección es que una invariante debe comparar contra una contabilidad independiente. Guarda en el handler una variable fantasma (ghost) con lo que cada actor depositó y retiró, y compara el saldo del contrato con esa suma. Cuando esa prueba falle, tendrás tu primer hallazgo completo: precondición, secuencia, propiedad rota y corrección.