Ownable es un contrato abstracto que proporciona control de acceso basado en un propietario. Cuando se hereda, restringe funciones específicas al propietario mediante el modificador onlyOwner. Tiene tres mecanismos principales, cada uno implementado a través de las siguientes funciones:

• onlyOwner()

  Este modificador restringe el acceso a funciones específicas permitiendo que solo el propietario las llame.

• renounceOwnership()

  Esta función pública está protegida por el modificador onlyOwner, permitiendo que solo el propietario la llame. Al ejecutarse, establece al propietario en la dirección cero (address(0)). Después de la renuncia, todas las funciones restringidas por onlyOwner se vuelven permanentemente inaccesibles.

• transferOwnership(address)

  Esta también es una función pública y, al igual que renounceOwnership(), está restringida por el modificador onlyOwner. Cuando se llama con una dirección de argumento válida (no address(0)), actualiza la propiedad del contrato a esa dirección, incluso si es la misma que la del propietario actual.

A continuación se muestra el contrato Ownable de OpenZeppelin, proporcionado como referencia mientras se explica su enfoque para la verificación formal:

Copy
// SPDX-License-Identifier: MIT
// OpenZeppelin Contracts (last updated v5.0.0) (access/Ownable.sol)

pragma solidity ^0.8.20;

import {Context} from "../utils/Context.sol";

/**
 * @dev Contract module which provides a basic access control mechanism, where
 * there is an account (an owner) that can be granted exclusive access to
 * specific functions.
 *
 * The initial owner is set to the address provided by the deployer. This can
 * later be changed with {transferOwnership}.
 *
 * This module is used through inheritance. It will make available the modifier
 * `onlyOwner`, which can be applied to your functions to restrict their use to
 * the owner.
 */
abstract contract Ownable is Context {
    address private _owner;

    /**
     * @dev The caller account is not authorized to perform an operation.
     */
    error OwnableUnauthorizedAccount(address account);

    /**
     * @dev The owner is not a valid owner account. (eg. `address(0)`)
     */
    error OwnableInvalidOwner(address owner);

    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);

    /**
     * @dev Initializes the contract setting the address provided by the deployer as the initial owner.
     */
    constructor(address initialOwner) {
        if (initialOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(initialOwner);
    }

    /**
     * @dev Throws if called by any account other than the owner.
     */
    modifier onlyOwner() {
        _checkOwner();
        _;
    }

    /**
     * @dev Returns the address of the current owner.
     */
    function owner() public view virtual returns (address) {
        return _owner;
    }

    /**
     * @dev Throws if the sender is not the owner.
     */
    function _checkOwner() internal view virtual {
        if (owner() != _msgSender()) {
            revert OwnableUnauthorizedAccount(_msgSender());
        }
    }

    /**
     * @dev Leaves the contract without owner. It will not be possible to call
     * `onlyOwner` functions. Can only be called by the current owner.
     *
     * NOTE: Renouncing ownership will leave the contract without an owner,
     * thereby disabling any functionality that is only available to the owner.
     */
    function renounceOwnership() public virtual onlyOwner {
        _transferOwnership(address(0));
    }

    /**
     * @dev Transfers ownership of the contract to a new account (`newOwner`).
     * Can only be called by the current owner.
     */
    function transferOwnership(address newOwner) public virtual onlyOwner {
        if (newOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(newOwner);
    }

    /**
     * @dev Transfers ownership of the contract to a new account (`newOwner`).
     * Internal function without access restriction.
     */
    function _transferOwnership(address newOwner) internal virtual {
        address oldOwner = _owner;
        _owner = newOwner;
        emit OwnershipTransferred(oldOwner, newOwner);
    }
}

Especificaciones CVL de Ownable de OZ

Aquí está el enlace a la especificación CVL para el contrato Ownable: Especificación CVL de Ownable.

Para simplificar, hicimos modificaciones menores colocando las siguientes definiciones directamente en el archivo de especificación, en lugar de importarlas de IOwnable.spec y helpers.spec:

• function owner() external returns (address) envfree (colocada dentro del bloque methods)
• definition nonpayable(env e) returns bool = e.msg.value == 0

Esta versión modificada a continuación es funcionalmente equivalente a la original y se utilizará para la discusión:

Copy
methods {
    function restricted() external;
    function owner() external returns (address) envfree; // taken from the import IOwnable.spec
}


definition
 nonpayable(env e) returns bool = e.msg.value == 0; // taken from the helpers.spec

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: transferOwnership changes ownership                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferOwnership(env e) {
    require nonpayable(e);

    address newOwner;
    address current = owner();

    transferOwnership@withrevert(e, newOwner);
    bool success = !lastReverted;

    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
    assert success => owner() == newOwner, "current owner changed";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: renounceOwnership removes the owner                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

    renounceOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => owner() == 0, "owner not cleared";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Access control: only current owner can call restricted functions                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

    calldataarg args;
    restricted@withrevert(e, args);

    assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: ownership can only change in specific ways                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

    method f; calldataarg args;
    f(e, args);

    address newCurrent = owner();

    // If owner changes, must be either transferOwnership or renounceOwnership
    assert oldCurrent != newCurrent => (
        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
    );
}

Observe el uso de la palabra clave definition. Declara lógica reutilizable para expresiones comunes utilizadas en toda la especificación y se invoca en la mayoría de las reglas:

Copy
definition nonpayable(env e) returns bool = e.msg.value == 0;

El nonpayable(env e) devuelve true cuando la llamada se realiza sin enviar Ether, es decir, cuando msg.value == 0.

También vale la pena mencionar que la especificación invoca una función llamada restricted(), que no es parte del contrato Ownable. En cambio, está implementada en el contrato harness que hereda del contrato abstracto Ownable.

Cuando ejecutamos la verificación, estamos verificando el contrato harness. A menudo, el harness hace más que eso, pero ese es un tema para otro capítulo. Por ahora, lo que importa es que agregamos una función restricted() y aplicamos el modificador onlyOwner.

A continuación se muestra la implementación del contrato harness:

Copy
/// OwnableHarness.sol

import {Ownable} from "src/Ownable/Ownable.sol"; // import path: modify as necessary

contract OwnableHarness is Ownable {
    constructor(address initialOwner) Ownable(initialOwner) {}

    function restricted() external onlyOwner {}
}

Control de Acceso

Comenzamos con la regla más fundamental: onlyCurrentOwnerCanCallOnlyOwner(). Esta regla verifica que el modificador onlyOwner impida que los no propietarios llamen a funciones restringidas:

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Access control: only current owner can call restricted functions                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

    calldataarg args;
    restricted@withrevert(e, args);

    assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

La línea require nonpayable(e) significa que el resto de la regla solo se evaluará para transacciones que no envíen Ether (e.msg.value == 0); todas las demás entradas se excluyen del análisis.

La línea address current = owner() recupera la dirección actual del propietario, que luego se utiliza en la aserción.

Ahora considere las siguientes líneas, que necesitan un poco más de explicación:

Copy
calldataarg args;
restricted@withrevert(e, args);

La línea calldataarg args pasa argumentos arbitrarios a la llamada a la función restricted@withrevert(e, args). Sin embargo, esto puede simplificarse a:

Copy
restricted@withrevert(e);

porque el Prover asigna automáticamente valores arbitrarios a las entradas por defecto, haciendo que calldataarg sea innecesario en este caso (además, restricted() no tiene un parámetro). Ambas formas son válidas y reflejan la preferencia del autor de la especificación.

Ahora, la siguiente pregunta es si debería incluirse en el bloque methods:

Copy
methods {
    function restricted() external;
    ...
}

La especificación de OpenZeppelin la incluye. Sin embargo, hacerlo produce una advertencia (incluso si esta regla se verifica):

“La declaración del método para OwnableHarness.restricted() no es envfree, optional, ni está resumida, por lo que no tiene efecto.”

Como se discutió en nuestro capítulo anterior, si una función depende del entorno y se trata como tal, no necesita incluirse en el bloque methods. En este caso, podemos simplificar eliminando la línea function restricted() external del bloque methods.

Ahora, finalmente, la aserción:

Copy
assert !lastReverted <=> e.msg.sender == current, "access control failed";

Esto significa "la llamada tiene éxito si y solo si el llamante es la dirección current". En todos los demás casos, la función debe revertirse. Por supuesto, la función puede revertirse si se envía con Ether, pero excluimos explícitamente ese caso en esta regla utilizando la declaración require nonpayable(e).

Renunciar a la Propiedad

Esta regla verifica que solo el propietario puede renunciar a la propiedad y, si tiene éxito, la dirección del propietario se establece en address(0). Aquí está la regla:

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: renounceOwnership removes the owner                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

    renounceOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => owner() == 0, "owner not cleared";
}

A simple vista, la regla establece !lastReverted en success, lo que se utiliza en ambas aserciones.

La primera aserción:

Copy
assert success <=> e.msg.sender == current, "unauthorized caller";

confirma la misma lógica que la última regla: “la llamada tiene éxito si y solo si el llamante es el propietario actual”.

La segunda aserción:

Copy
assert success => owner() == 0, "owner not cleared";

es una implicación. Significa que "si la llamada tiene éxito, entonces el propietario debe ser eliminado (es decir, establecido en address(0))". En otras palabras, se debe renunciar a la propiedad.

Transferir la Propiedad

Esta regla verifica que si la llamada tiene éxito, el llamante debe ser el propietario actual y la nueva dirección debe ser válida (es decir, no address(0)).

Ahora veamos la regla para transferOwnership():

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: transferOwnership changes ownership                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferOwnership(env e) {
    require nonpayable(e);

    address newOwner;
    address current = owner();

    transferOwnership@withrevert(e, newOwner);
    bool success = !lastReverted;

    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
    assert success => owner() == newOwner, "current owner changed";
}

Al igual que las reglas anteriores, esta aserción:

Copy
assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";

Se basa en la premisa de que la llamada tiene éxito si y solo si el llamante es el propietario actual y newOwner es una dirección válida (distinta de cero). La condición newOwner != 0 es necesaria porque eliminarla violaría la comprobación interna de la función de Solidity y resultaría en un revert (y por lo tanto en una violación).

Copy
/// Ownable.sol

function transferOwnership(address newOwner) public virtual onlyOwner {
    if (newOwner == address(0)) { // this line will cause a revert if newOwner is zero
        revert OwnableInvalidOwner(address(0));
    }
    _transferOwnership(newOwner);
}

Ahora, para la última aserción de esta regla:

Copy
assert success => owner() == newOwner, "current owner changed";

esto significa que si la llamada tiene éxito, el propietario debe actualizarse a newOwner.

Reglas Paramétricas

Ahora que las tres características principales del contrato Ownable han sido verificadas formalmente, queda una última regla: una regla paramétrica que verifica los cambios de propiedad. La regla afirma que si el propietario cambia, debe ocurrir a través de:

• transferOwnership() que resulta en un nuevo propietario distinto de cero o
• renounceOwnership() que resulta en la dirección cero como el nuevo propietario

Aquí está la regla:

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: ownership can only change in specific ways                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

    method f; calldataarg args;
    f(e, args);

    address newCurrent = owner();

    // If owner changes, must be either transferOwnership or renounceOwnership
    assert oldCurrent != newCurrent => (
        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
    );
}

Esta es una regla paramétrica, como lo evidencia la presencia de la llamada f(e, args). En las líneas anteriores y posteriores a la llamada al método f(e, args), recuperamos oldCurrent y newCurrent utilizando owner(). Está claro que estamos rastreando los cambios en el estado de la propiedad. Con f(e, args) colocado entre estas dos llamadas, estamos permitiendo la ejecución de funciones arbitrarias y comprobando si esto causa un cambio en la propiedad.

Ahora la aserción:

Copy
assert oldCurrent != newCurrent => (
    (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
    (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
);

Si el propietario ha cambiado (oldCurrent != newCurrent), entonces el cambio debe haber ocurrido de una de dos maneras válidas:

- `e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector)`

    
Esto significa que el llamante debe ser el propietario actual, el nuevo propietario no es la dirección cero, y la función que desencadenó el cambio es `transferOwnership()`.
    

- `e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)`

    
Esto significa que el llamante sigue siendo el propietario actual, pero el nuevo propietario es la dirección cero, y la función utilizada debe haber sido `renounceOwnership()`.

Estos son los dos únicos caminos legítimos para cambiar la propiedad según la regla.

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