Este artículo describe cómo Certora verificó formalmente el contrato Initializable.sol de OpenZeppelin. Asumimos que el lector ya está familiarizado con el uso de este contrato. Si no es así, consulte nuestro artículo sobre Contratos Inicializables.

En los contratos actualizables, no se utiliza el constructor. En su lugar, después del despliegue, el desplegador llama a initialize(...) y esto establece las variables de estado en sus condiciones iniciales. La función initialize(...) debe poder llamarse solo una vez.

Para permitir que las variables de almacenamiento se establezcan en otro valor en un momento posterior (como si un token ERC-20 cambia su nombre o totalSupply), estos cambios deben realizarse a través de la función reinitialize. No es necesario que las funciones externas se llamen “initializer” y “reinitializer”, pero sí necesitan que se les aplique el modificador initializer() y reinitializer() de la biblioteca OpenZeppelin a esas funciones.

Por motivos de seguridad, los contratos actualizables deben tener las siguientes propiedades con respecto a los inicializadores:

1. Una vez que se llama al inicializador, no debería poder llamarse nunca más (todas las llamadas deberían revertirse).
2. No debería ser posible llamar al inicializador en el contrato de implementación. Solo debería poder llamarse al inicializador en el proxy, ya que todo el estado se mantiene en el contrato proxy. Es por esto que los contratos lógicos de los patrones proxy llaman a _disableInitializers() en el constructor.
3. Una vez que el inicializador y el reinicializador están deshabilitados, deben permanecer deshabilitados de forma permanente.
4. Si llamamos a la función reinitializer, debemos incrementar la versión con respecto a una anterior. La versión se almacena como una variable uint64.

Tenga en cuenta que el control de acceso al inicializador y al reinicializador está fuera del alcance de este contrato. El contrato ni siquiera impone cómo se llaman esas funciones, solo asegura que la funcionalidad de los modificadores sea correcta.

Cubriremos la mayor parte, pero no la totalidad, del archivo Initializable.spec de OpenZeppelin, ya que parte del contenido se basa en técnicas que aún no hemos cubierto. Sin embargo, la mayoría del contenido debería ser comprensible en base a lo que hemos cubierto hasta ahora en el curso.

Aquí está la primera regla que examinamos:

Copy
rule cannotInitializeTwice() {
    require isInitialized();

    initialize@withrevert();

    assert lastReverted, "contract must only be initialized once";
}

Esto dice que si el contrato está inicializado, entonces llamar a initialize() se revertirá. Esta regla no dice que si el contrato no está inicializado, entonces llamar a initialize() no se revertirá, o en otras palabras, que un contrato no inicializado puede inicializarse. La declaración require establece el alcance de la regla para cubrir únicamente los casos en los que el inicializador ya ha sido llamado.

La especificación de que un contrato no inicializado puede inicializarse está cubierta por la siguiente regla:

Copy
rule initializeEffects() {
    requireInvariant notInitializing();

    bool isUninitializedBefore = isUninitialized();

    initialize@withrevert();
    bool success = !lastReverted;

    assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts";
    assert success => version() == 1,         "initialize must set version() to 1";
    
}

La regla dice que initialize tiene éxito si y solo si el contrato no ha sido inicializado antes. Si la inicialización tiene éxito, entonces la versión debe establecerse en 1. La sintaxis requireInvariant no es algo que hayamos cubierto todavía, la revisaremos en un tutorial posterior.

La regla de que el reinicializador no puede anular el estado de deshabilitación se explica en gran medida por sí misma:

Copy
rule cannotReinitializeOnceDisabled() {
    require isDisabled();

    uint64 n;
    reinitialize@withrevert(n);

    assert lastReverted, "contract is disabled";
}

En otras palabras, si el contrato está deshabilitado, cualquier llamada a reinitialize provoca una reversión.

Cuando se llama al reinicializador, se debe establecer una nueva versión, y esa versión debe ser mayor que la versión anterior. La siguiente regla dice que si la nueva versión es la versión pasada en el argumento, y si la transacción no se revirtió, esa nueva versión es mayor que la anterior.

Copy
rule reinitializeEffects() {
    requireInvariant notInitializing();

    uint64 versionBefore = version();

    uint64 n;
    reinitialize@withrevert(n);
    bool success = !lastReverted;

    assert success <=> versionBefore < n, "can only reinitialize to a later versions";
    assert success => version() == n,     "reinitialize must set version() to n";
}

La regla final que examinamos establece que si el contrato no está en el “estado de inicialización” (el contrato está estableciendo actualmente las variables de almacenamiento o reinicializando), entonces llamar a disable siempre tiene éxito.

Copy
rule disableEffect() {
    requireInvariant notInitializing();

    disable@withrevert();
    bool success = !lastReverted;

    assert success,      "call to _disableInitializers failed";
    assert isDisabled(), "disable state not set";
}

Resumen

Las reglas que mostramos aquí son extremadamente fáciles de entender, pero las revisamos para demostrar que la verificación formal no siempre tiene que ser compleja. Las reglas que mostramos aquí podrían lograrse con una prueba unitaria, pero la verificación formal es más exhaustiva y de alta garantía.

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