Los nonces, cuyo nombre proviene de “number used once” (número usado una vez), se utilizan en esquemas de firmas digitales para prevenir ataques de repetición (replay attacks). Para los propósitos de este artículo, asumimos que el lector ya está familiarizado con lo que son los nonces y cómo se usan.

La biblioteca OpenZeppelin nonces.sol rastrea los nonces de los firmantes utilizando un contador que se incrementa para cada dirección. Aquí está la biblioteca completa (con los comentarios omitidos para mayor brevedad):

Copy
abstract contract Nonces {

    error InvalidAccountNonce(address account, uint256 currentNonce);

    mapping(address account => uint256) private _nonces;

    function nonces(address owner) public view virtual returns (uint256) {
        return _nonces[owner];
    }

    function _useNonce(address owner) internal virtual returns (uint256) {
        unchecked {
            return _nonces[owner]++;
        }
    }

    function _useCheckedNonce(address owner, uint256 nonce) internal virtual {
        uint256 current = _useNonce(owner);
        if (nonce != current) {
            revert InvalidAccountNonce(owner, current);
        }
    }
}

Aquí está el contrato en resumen:

• nonces(address owner) es una función view que devuelve el nonce actual para owner.
• _useNonce(address owner) incrementa el nonce para el propietario y devuelve el valor del nonce antes del incremento. Por ejemplo, si el nonce de Alice era 2 y llamamos a _useNonce para su cuenta, entonces _useNonce devuelve 2, pero su nonce actual se convierte en 3 después de que se ejecuta la función.
• _useCheckedNonce(address owner, uint256 nonce) incrementa el nonce, pero revierte a menos que el argumento nonce sea igual al nonce actual. Por ejemplo, si el nonce actual de Alice es 15, entonces proporcionar cualquier valor distinto de 15 para el argumento nonce causará un revert. Después de la llamada a la función, el nonce de Alice se convertirá en 16.

Esto no es muy diferente de nuestro ejemplo recurrente de Counter de una parte anterior de nuestro tutorial, por lo que las reglas que Certora escribió para esta biblioteca serán fáciles de explicar.

Aquí hay algunas de las propiedades que se probarán:

• El nonce solo se incrementa
• Incrementar un nonce nunca falla
• Incrementar un nonce no tiene efecto sobre otros nonces

Especificación de Nonces.sol

Aquí está la especificación que Certora escribió para nonces.sol.

Función auxiliar

La especificación incluye una función CVL auxiliar para verificar que el nonce no sea el valor máximo de uint256. En la práctica, un contador no puede llegar tan alto:

Copy
function nonceSanity(address account) returns bool {
    return nonces(account) < max_uint256;
}

El nonce solo se incrementa

Comenzaremos con la regla más fácil, ya que vimos algo similar en el capítulo sobre reglas paramétricas:

Copy
// address account in the argument is equivalent to
// declaring it inside the function body
rule nonceOnlyIncrements(
address account)
 {
    require nonceSanity(account);

    mathint nonceBefore = nonces(account);

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

    mathint nonceAfter = nonces(account);

    assert nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1, "nonce only increments";
}

Esta regla dice que “todas las transacciones dan como resultado que el nonce no cambie o que aumente exactamente en 1”.

Regla useNonce

La regla useNonce hace dos afirmaciones:

• llamar a useNonce() nunca revierte
• incrementar el nonce en una account A no afecta a las demás cuentas, es decir, su nonce no cambia.

Copy
rule useNonce(address account) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    mathint nonceUsed = useNonce@withrevert(account);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    // liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

Expliquemos esto pieza por pieza:

Copy
require nonceSanity(account);

Este código asegura que el prover no pruebe el caso (imposible) cuando el nonce es type(uint256).max.

Copy
address other;

Este other es la forma en que obtenemos una referencia a “cualquier otra cuenta” además de la account especificada en el argumento de la regla. Ten en cuenta que la regla no requiere account != other como una precondición — esto se maneja más adelante.

Copy
mathint nonceBefore = nonces(account);
mathint otherNonceBefore = nonces(other);

Esto lee los valores de los nonces de account y other antes de la transición de estado.

Copy
mathint nonceUsed = useNonce@withrevert(account);
bool success = !lastReverted;

mathint nonceAfter = nonces(account);
mathint otherNonceAfter = nonces(other);

El código mathint nonceUsed = useNonce@withrevert(account); es la línea clave, ya que el nonce se incrementa allí. Registramos el nuevo estado del nonce en nonceAfter y otherNonceAfter.

Ahora veamos las afirmaciones:

Copy
// liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";

Recuerda que la función useNonce devuelve el nonce que acaba de ser consumido, de ahí la afirmación nonceBefore == nonceUsed.

La afirmación final establece que ningún otro nonce fue cambiado. Su lógica puede derivarse utilizando la regla de la contrapositiva.

Por la regla contrapositiva de las implicaciones, si A → B, entonces !B → !A. Supongamos que A significa other ≠ account y B significa otherNonceBefore = otherNonceAfter. Podemos decir entonces que "si el other no es igual a account, entonces el nonce de other no cambió. Por lo tanto, podemos escribir que other ≠ account implica otherNonceBefore = otherNonceAfter, o en otras palabras A → B. Usando la regla de la contrapositiva, podemos decir que !B → !A o equivalentemente otherNonceBefore ≠ otherNonceAfter (ocurrió un cambio) implica other = account y esto es exactamente lo que establece la última afirmación.

Regla useCheckedNonce

La regla final reutiliza mucha lógica de los ejemplos anteriores, no la explicaremos aquí. La diferencia clave es la línea assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";. Recuerda que useCheckedNonce solo tiene éxito (no revierte) si el nonce que se le pasa es igual al nonce actual del usuario. Por lo tanto, el operador bicondicional codifica que “si el nonce coincide, se garantiza que la transacción tendrá éxito. Si no, se garantiza que revertirá.”

Copy
rule useCheckedNonce(address account, uint256 currentNonce) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    useCheckedNonce@withrevert(account, currentNonce);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    //// SEE HERE ////
    // liveness
    // the to_mathint cast makes it explicit to have the same type on both sides
    assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";

    // effect
    assert success => nonceAfter == nonceBefore + 1, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

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