Introducción
Este capítulo es la parte final (5/5) del recorrido por el código de la especificación CVL del ERC-721 de OpenZeppelin que verifica formalmente las siguientes reglas:
-
supplyChangeEl suministro total cambia solo a través de operaciones de mint o burn, y exactamente en uno.
-
balanceChangeEl saldo de la cuenta cambia solo a través de operaciones de mint, burn o transferencia, y exactamente en uno.
-
ownershipChangeLa propiedad del token cambia solo a través de operaciones de mint, burn o transferencia.
-
approvalChangeLa aprobación por token cambia solo a través de la llamada a
approve()o como efecto secundario de las operaciones de burn o transferencia. -
approvedForAllChangeLa aprobación del operador cambia solo a través de la llamada a
setApprovalForAll().
Estas reglas utilizan un patrón de regla parcialmente paramétrica (que se discutirá en la siguiente sección), el cual se basa en el concepto de reglas paramétricas cubierto en el capítulo “Introducción a las reglas paramétricas” (Introduction to Parametric Rules).
Las propiedades de este capítulo difieren de las de capítulos anteriores. Anteriormente, verificamos comportamientos de métodos específicos: ¿mint() aumenta el suministro total? ¿transferFrom() actualiza los saldos como se espera? Esas propiedades probaron métodos individuales usando reglas ordinarias (no paramétricas).
Las propiedades aquí plantean una pregunta diferente: ¿qué métodos pueden cambiar un estado particular (como el suministro total o el saldo de una cuenta), y podemos confirmar que ningún otro método lo hace? Las reglas ordinarias no pueden responder a esto porque prueban un método a la vez. Incluso con una regla por método por propiedad, no podemos verificar que los métodos no enumerados no causen cambios.
Uno podría preguntarse si los invariantes de CVL podrían servir para el mismo propósito. Sin embargo, los invariantes de CVL no son adecuados aquí porque no pueden capturar cómo cambia un valor a lo largo de la llamada a un método. Los invariantes no pueden acceder a los valores previos a la llamada ni compararlos con los valores posteriores a la llamada, por lo que no pueden expresar propiedades como “este estado puede cambiar solo cuando se llaman métodos específicos” o “este estado cambia exactamente en esta cantidad”. Estas son propiedades de transición de estado, que requieren razonar sobre el estado previo y posterior a la llamada.
Un patrón paramétrico resuelve esto probando todos los métodos del contrato en una sola regla y razonando sobre el estado previo y posterior a la llamada. Esto permite verificar ambas cosas: qué métodos están permitidos para cambiar el estado y que ningún otro método puede causar el mismo cambio.
La regla parcialmente paramétrica
En el capítulo anterior, “Introducción a las reglas paramétricas”, aprendimos que:
“… una regla paramétrica verifica que una propiedad se mantenga verdadera después de que cualquier función sea llamada con cualquier argumento válido.”
La frase clave es: ”después de que cualquier función sea llamada con cualquier argumento válido”, lo cual corresponde al siguiente patrón de código:
rule parametricExample(env e, method f, calldataarg args) {
/// set precondition
/// record pre-call state
/// parametric call: invokes all functions in the scene with arbitrary arguments
f(e, args);
/// record post-call state
/// assertions
}
Este patrón (completamente paramétrico) funciona bien cuando se aplican las mismas precondiciones a todos los métodos. Sin embargo, no es apropiado cuando diferentes métodos necesitan diferentes restricciones.
En lugar del patrón completamente paramétrico f(e, args), podemos usar un patrón “parcialmente paramétrico”. Esto no es sintaxis de CVL, sino un patrón de diseño de especificaciones. Como describe la documentación de Certora:
“Esta regla parcialmente paramétrica demuestra la lógica condicional basada en el tipo de método invocado, permitiendo acciones y aserciones específicas adaptadas a diferentes escenarios dentro del contrato inteligente.”
La frase clave es “acciones y aserciones específicas adaptadas a diferentes escenarios”, lo cual corresponde al siguiente patrón de código:
rule partiallyParametricExample(env e) {
method f;
if (f.selector == sig:exampleMethod1(uint256, address).selector) {
// method-specific logic
}
else if (f.selector == sig:exampleMethod2(address, address).selector) {
// method-specific logic
}
else {
// method-specific logic
}
}
La lógica específica del método pueden ser precondiciones, llamadas a métodos o incluso aserciones. Para tener un código más limpio, estas declaraciones condicionales se pueden abstraer en una sola función de CVL, como se muestra a continuación:
rule partiallyParametricExample(env e) {
method f;
helperFunction(e, f); // contains all conditional logic
}
La especificación de OpenZeppelin utiliza la función auxiliar helperSoundFnCall() para implementar este patrón. Aquí hay un ejemplo de la regla supplyChange (que examinaremos en detalle más adelante):
/// ERC721.spec
rule supplyChange(env e) {
...
method f; helperSoundFnCall(e, f);
...
/// assert
/// assert
}
El término “Sound” (sólido) en helperSoundFnCall() es deliberado. La solidez (soundness) significa que la verificación no pasa por alto ningún error real, y una fuente común de falta de solidez es excluir rutas de ejecución válidas mediante precondiciones excesivamente restrictivas.
La función auxiliar enruta f(e, args) de una manera sólida aplicando precondiciones selectivamente en función del método invocado en lugar de globalmente a todas las llamadas. Aplicar una precondición a métodos que no la requieren excluiría rutas de ejecución válidas.
En la siguiente sección, veremos cómo la llamada a un método arbitrario f(e, args) se enruta a las precondiciones específicas del método adecuadas que mantienen la especificación sólida.
helperSoundFnCall() enruta la llamada de f(e, args) a la rama de método correcta
La función de CVL helperSoundFnCall() enruta la llamada al método arbitrario f(e, args) a la rama de método correcta coincidiendo con el selector de función. Para cada selector que coincida, la función auxiliar de CVL hace lo siguiente:
- declara los argumentos requeridos,
- aplica las precondiciones específicas del método, y
- llama a la función concreta correspondiente.
Para operaciones de mint — mint(), safeMint(), y safeMint(bytes)
Cuando la función invocada es una variante de mint, la función auxiliar:
- Declara los argumentos requeridos:
address to,uint256 tokenId, y para la variante de bytes,bytes data. - Aplica las precondiciones específicas del método:
require balanceLimited(to)— restringe el saldo del destinatario a menos demax_uint256para evitar el desbordamientorequire data.length < 0xffff— limita la longitud de los datos a menos de 65.535 bytes (0xffff) para evitar matrices poco realistamente grandes durante la ejecución del Prover
- Llama a las funciones correspondientes:
mint(e, to, tokenId),safeMint(e, to, tokenId)osafeMint(e, to, tokenId, data).
function helperSoundFnCall(env e, method f) {
if (f.selector == sig:mint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
mint(e, to, tokenId);
}
else if (f.selector == sig:safeMint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId);
}
else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId, data);
}
...
}
Para la operación de burn — burn()
Cuando la función invocada es burn(), la función auxiliar:
-
Declara el argumento requerido
uint256 tokenId. -
Aplica la precondición específica del método
requireInvariant ownerHasBalance(tokenId), la cual requiere que el token exista (tenga un propietario distinto de cero) antes del burn. -
Llama a la función correspondiente
burn(e, tokenId).function helperSoundFnCall(env e, method f) { ... } else if (f.selector == sig:burn(uint256).selector) { uint256 tokenId; requireInvariant ownerHasBalance(tokenId); // requireInvariant notMintedUnset(tokenId); burn(e, tokenId); } ... }
Para operaciones de transferencia — transferFrom(), safeTransferFrom(), y safeTransferFrom(bytes)
Cuando la función invocada es una variante de transferencia, la función auxiliar:
- Declara los argumentos requeridos:
address from,address to,uint256 tokenId, y para la variante de bytes,bytes data - Aplica las precondiciones específicas del método:
require balanceLimited(to)— restringe el saldo del destinatario para que sea estrictamente menor amax_uint256y así evitar que el Prover explore saldos de destinatario poco realistas.requireInvariant ownerHasBalance(tokenId)— asegura que el token exista antes de que pueda ser transferido. Sin esto, el Prover consideraría casos en los que un token es transferido desde la dirección cero.requireInvariant notMintedUnset(tokenId)— descarta cualquier aprobación para un token no acuñado. Sin esto, el Prover podría tratar un token inexistente como si tuviera un operador aprobado.require data.length < 0xffff— (solo en la variante de bytes) limita la longitud de los datos a menos de 65.535 bytes (0xffff) para evitar matrices poco realistamente grandes durante la ejecución del Prover.
- Llama a las funciones correspondientes:
transferFrom(),safeTransferFrom(),safeTransferFrom(bytes)
function helperSoundFnCall(env e, method f) {
...
} else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
transferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
address from; address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId, data);
...
}
Para todas las operaciones distintas a mint, burn y transferencia
Las funciones distintas a mint, burn o transferencia se manejan con una llamada completamente paramétrica f(e, args) con argumentos arbitrarios:
function helperSoundFnCall(env e, method f) {
...
} else {
calldataarg args;
f(e, args);
}
}
Implementación completa de la función de CVL helperSoundFnCall()
Aquí está la función auxiliar completa de CVL:
function helperSoundFnCall(env e, method f) {
if (f.selector == sig:mint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
mint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId, data);
} else if (f.selector == sig:burn(uint256).selector) {
uint256 tokenId;
requireInvariant ownerHasBalance(tokenId);
// requireInvariant notMintedUnset(tokenId);
burn(e, tokenId);
} else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
transferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
address from; address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId, data);
} else {
calldataarg args;
f(e, args);
}
}
Nota: En las ramas de mint y burn hemos comentado requireInvariant notMintedUnset(tokenId) para mostrar únicamente las precondiciones que son estrictamente necesarias para cada método invocado. Esto no significa que el invariante sea inútil; dado que se ha probado como un invariante separado en la especificación, se puede asumir que siempre se cumple y restituirse de forma segura. Agregarlo como precondición generalmente acorta los tiempos de ejecución del Prover.
Con las precondiciones específicas del método manejadas en helperSoundFnCall(), podemos proceder a las discusiones sobre las reglas en la siguiente sección.
supplyChange — el suministro total solo puede cambiar a través de mint(), safeMint(), safeMint(bytes) y burn()
Esta regla verifica qué métodos del contrato pueden aumentar o disminuir el suministro total en 1. Aquí está la regla que captura este comportamiento, la cual discutiremos en detalle a continuación:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
mathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;
assert supplyAfter > supplyBefore => (
supplyAfter == supplyBefore + 1 &&
(
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
)
);
assert supplyAfter < supplyBefore => (
supplyAfter == supplyBefore - 1 &&
f.selector == sig:burn(uint256).selector
);
}
Ejecución del Prover: link
Precondiciones
-
require nonzerosender(e)Esta precondición restringe que el llamador sea distinto de cero. Sin esta restricción, el Prover puede explorar ejecuciones en las que una transferencia se origina en
address(0)y mueve un token a una dirección distinta de cero, lo que en la práctica es un mint ejecutado a través de una operación de transferencia. -
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)Esta precondición de invariante evita que
address(0)apruebe operadores. Sin esta restricción, el Prover puede explorar estados en los queaddress(0)ha otorgado permisos de operador a direcciones distintas de cero.
Estados previos y posteriores a la llamada
-
supplyBefore = _supplyRegistra el suministro total antes de ejecutar la llamada parcialmente paramétrica (
method f; helperSoundFnCall(e, f)). -
method f; helperSoundFnCall(e, f)Ejecuta la llamada parcialmente paramétrica discutida anteriormente.
-
mathint supplyAfter = _supplyRegistra el suministro total después de ejecutar la llamada parcialmente paramétrica.
mathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;
ERC-721 no rastrea el suministro total, por lo que usamos una variable fantasma _supply que rastrea la suma de todos los _balances a través de un hook de Sstore:
ghost mathint _supply {
init_state axiom _supply == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
Aserciones
-
La primera aserción establece que si el suministro total aumenta (
supplyAfter > supplyBefore), el aumento debe ser exactamente de 1 y solo puede ser causado pormint(),safeMint()osafeMint(bytes):rule supplyChange(env e) { ... assert supplyAfter > supplyBefore => ( supplyAfter == supplyBefore + 1 && ( f.selector == sig:mint(address,uint256).selector || f.selector == sig:safeMint(address,uint256).selector || f.selector == sig:safeMint(address,uint256,bytes).selector ) ); ... } -
La segunda aserción cubre el caso de burn. Si el suministro total disminuye (
supplyAfter < supplyBefore), la disminución debe ser exactamente de 1 y solo puede ser causada porburn():rule supplyChange(env e) { ... assert supplyAfter < supplyBefore => ( supplyAfter == supplyBefore - 1 && f.selector == sig:burn(uint256).selector ); }
balanceChange — los saldos de las cuentas solo pueden cambiar a través de operaciones de mint, burn y transferencia
La siguiente regla verifica dos propiedades sobre los cambios de saldo:
- Los saldos cambian exactamente en un token por operación
- Solo las operaciones de mint, burn o transferencia pueden cambiar los saldos
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {
// requireInvariant balanceOfConsistency(account);
// require balanceLimited(account);
mathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter = balanceOf(account);
// balance can change by at most 1
assert balanceBefore != balanceAfter => (
balanceAfter == balanceBefore - 1 ||
balanceAfter == balanceBefore + 1
);
// only selected function can change balances
assert balanceBefore != balanceAfter => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
);
}
Ejecución del Prover: link
Precondiciones
Los requireInvariant balanceOfConsistency(account) y require balanceLimited(account) están comentados porque helperSoundFnCall() ya aplica estas precondiciones para todos los métodos que cambian saldos. El balanceOfConsistency se aplica a través del bloque preservado del invariante ownerHasBalance en las ramas de burn y transferencia.
Estados previos y posteriores a la llamada
La regla registra el saldo de la cuenta antes y después de la llamada a helperSoundFnCall(e, f) para comparar los valores y determinar si la llamada al método cambió el saldo, y en qué cantidad:
mathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter = balanceOf(account);
Aserciones
La primera aserción establece que si el saldo de una cuenta cambia (balanceBefore != balanceAfter) después de la llamada a helperSoundFnCall(e, f), el cambio debe ser más o menos uno — ni más, ni menos.
// balance can change by at most 1
assert balanceBefore != balanceAfter => (
balanceAfter == balanceBefore - 1 ||
balanceAfter == balanceBefore + 1
);
La segunda aserción establece que solo las siguientes funciones pueden cambiar los saldos:
- funciones de mint (
mint(),safeMint(),safeMint(bytes)) - burn (
burn()) - funciones de transferencia (
transferFrom(),safeTransferFrom(),safeTransferFrom(bytes))
// only selected function can change balances
assert balanceBefore != balanceAfter => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
);
Si cualquier otra función no enumerada causa un cambio de saldo, la aserción fallará y el Prover informará de una violación.
ownershipChange() — la propiedad puede cambiar solo a través de operaciones de mint, burn y transferencia
La siguiente regla verifica que la propiedad de un token (ownerOf(tokenId)) puede cambiar solo a través de operaciones de mint, burn o transferencia. El tipo de operación depende de cómo cambie la dirección del propietario:
- De la dirección cero a una dirección distinta de cero — indica un mint, que solo
mint(),safeMint()osafeMint(bytes)pueden causar. - De una dirección distinta de cero a la dirección cero — indica un burn, que solo
burn()puede causar. - De una dirección distinta de cero a otra dirección distinta de cero — indica una transferencia, que solo
transferFrom(),safeTransferFrom()osafeTransferFrom(bytes)pueden causar.
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
address ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter = unsafeOwnerOf(tokenId);
assert ownerBefore == 0 && ownerAfter != 0 => (
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
);
assert ownerBefore != 0 && ownerAfter == 0 => (
f.selector == sig:burn(uint256).selector
);
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
);
}
Ejecución del Prover: link
Precondiciones
-
require nonzerosender(e)Esta precondición requiere que el llamador (
e.msg.sender) sea distinto de cero. Sin ella, el Prover puede modelar ejecuciones en las queaddress(0)llama atransferFromdirectamente, lo que crea propiedad desdeaddress(0), violando la regla de que solo las funciones de mint pueden hacer esto. -
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender)
Esta precondición de invariante evita que la dirección cero apruebe a cualquier operador. Sin ella, el Prover puede asumir queaddress(0)aprobó a un operador distinto de cero. Esto permite quetransferFrom(from = address(0), ...)tenga éxito incluso cuando el llamador es distinto de cero, lo que crea una transición de propiedad desde la dirección cero y viola la regla de que solo las funciones de mint pueden crear propiedad.
Estados previos y posteriores a la llamada
Estas líneas registran el propietario del token antes y después de helperSoundFnCall(e, f):
address ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter = unsafeOwnerOf(tokenId);
El uso de unsafeOwnerOf(tokenId) permite que la regla razone sobre los cambios de propiedad incluso cuando el token no existe, en cuyo caso el propietario es address(0).
Aserciones
-
assert ownerBefore == 0 && ownerAfter != 0 => (...)Si la propiedad cambia de la dirección cero a una dirección distinta de cero, lo que significa que ocurrió un mint, entonces solo las siguientes funciones podrían haberlo causado:
mint(),safeMint()osafeMint(bytes):assert ownerBefore == 0 && ownerAfter != 0 => ( f.selector == sig:mint(address,uint256).selector || f.selector == sig:safeMint(address,uint256).selector || f.selector == sig:safeMint(address,uint256,bytes).selector ); -
assert ownerBefore != 0 && ownerAfter == 0 => (...)Si la propiedad cambia de una dirección distinta de cero a la dirección cero, lo que significa que ocurrió un burn, entonces solo la función
burn()es responsable de esto:assert ownerBefore != 0 && ownerAfter == 0 => ( f.selector == sig:burn(uint256).selector ); -
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (...)Por último, si el cambio es de una dirección distinta de cero a otra dirección distinta de cero, entonces ocurrió una transferencia. Solo
transferFrom(),safeTransferFrom()ysafeTransferFrom(bytes)son responsables de estos cambios:assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => ( f.selector == sig:transferFrom(address,address,uint256).selector || f.selector == sig:safeTransferFrom(address,address,uint256).selector || f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector );
approvalChange() — la aprobación cambia solo a través de las funciones approve, transferFrom y burn
La siguiente regla verifica que la aprobación de un token específico (getApproved(tokenId)) solo puede cambiar de tres maneras:
- establecida directamente mediante una llamada a la función
approve() - restablecida a
address(0)como efecto secundario de una transferencia - restablecida a
address(0)como efecto secundario de un burn
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
address approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter = unsafeGetApproved(tokenId);
// approve can set any value, other functions reset
assert approvalBefore != approvalAfter => (
f.selector == sig:approve(address,uint256).selector ||
(
(
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
) && approvalAfter == 0
)
);
}
Ejecución del Prover: link
Estados previos y posteriores a la llamada
La siguiente línea registra la dirección aprobada antes y después de la llamada parcialmente paramétrica method f; helperSoundFnCall(e, f) para determinar si la aprobación cambió como resultado del método invocado enumerado, y si se borró a address(0):
address approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter = unsafeGetApproved(tokenId);
Aserción
Esta aserción establece que un cambio en la dirección aprobada solo puede ocurrir si:
- La llamada a la función es
approve(), la cual establece explícitamente la dirección aprobada, o - La llamada a la función es
transferFrom(),safeTransferFrom()(con o sin datos de bytes), oburn(), y la dirección aprobada se borra aaddress(0)(approvalAfter == 0) como efecto secundario.
// approve can set any value, other functions reset
assert approvalBefore != approvalAfter => (
f.selector == sig:approve(address,uint256).selector ||
(
(
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
) && approvalAfter == 0
)
);
La aserción fallará si:
- una función no enumerada en la regla borra o modifica la dirección aprobada.
transferFrom,safeTransferFromoburnno borra la dirección aprobada aaddress(0).
approvedForAllChange — la aprobación para todos solo cambia a través de la función setApprovalForAll()
Esta regla verifica que el estado de ‘aprobado para todos’ (approved-for-all) de un gastador (isApprovedForAll(owner, spender)) solo puede cambiar a través de una llamada explícita a la función setApprovalForAll():
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
bool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter = isApprovedForAll(owner, spender);
assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
}
Ejecución del Prover: link
Estados previos y posteriores a la llamada
-
bool approvedForAllBefore = isApprovedForAll(owner, spender);Esto registra el estado de ‘aprobado para todos’ antes de la llamada a
helperSoundFnCall(e, f). -
bool approvedForAllAfter = isApprovedForAll(owner, spender);Esto registra el estado de ‘aprobado para todos’ después de la llamada a
helperSoundFnCall(e, f).
bool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter = isApprovedForAll(owner, spender);
Aserción
Si el estado de ‘aprobado para todos’ para el gastador cambia, entonces la única causa es una llamada a setApprovalForAll():
assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
A diferencia de approve(), que se restablece en transferencias o burns, isApprovedForAll no cambia durante mint, transferencia o burn. Solo una llamada explícita a setApprovalForAll puede modificarlo. Si cualquier otra función cambia este estado, la aserción falla y el Prover informa de una violación.
Especificaciones completas
Aquí está la especificación completa para las reglas parcialmente paramétricas:
methods {
function balanceOf(address) external returns (uint256) envfree;
function ownerOf(uint256) external returns (address) envfree;
function isApprovedForAll(address,address) external returns (bool) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function unsafeGetApproved(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helper │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
function helperSoundFnCall(env e, method f) {
if (f.selector == sig:mint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
mint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256).selector) {
address to; uint256 tokenId;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId);
} else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
// requireInvariant notMintedUnset(tokenId);
safeMint(e, to, tokenId, data);
} else if (f.selector == sig:burn(uint256).selector) {
uint256 tokenId;
requireInvariant ownerHasBalance(tokenId);
// requireInvariant notMintedUnset(tokenId);
burn(e, tokenId);
} else if (f.selector == sig:transferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
transferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
address from; address to; uint256 tokenId;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId);
} else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
address from; address to; uint256 tokenId; bytes data;
require data.length < 0xffff;
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
requireInvariant notMintedUnset(tokenId);
safeTransferFrom(e, from, to, tokenId, data);
} else {
calldataarg args;
f(e, args);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _supply {
init_state axiom _supply == 0;
}
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover v8.3.1
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: total supply can only change through mint and burn │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule supplyChange(env e) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
mathint supplyBefore = _supply;
method f; helperSoundFnCall(e, f);
mathint supplyAfter = _supply;
assert supplyAfter > supplyBefore => (
supplyAfter == supplyBefore + 1 &&
(
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
)
);
assert supplyAfter < supplyBefore => (
supplyAfter == supplyBefore - 1 &&
f.selector == sig:burn(uint256).selector
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: balanceOf can only change through mint, burn or transfers. balanceOf cannot change by more than 1. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule balanceChange(env e, address account) {
// requireInvariant balanceOfConsistency(account);
// require balanceLimited(account);
mathint balanceBefore = balanceOf(account);
method f; helperSoundFnCall(e, f);
mathint balanceAfter = balanceOf(account);
// balance can change by at most 1
assert balanceBefore != balanceAfter => (
balanceAfter == balanceBefore - 1 ||
balanceAfter == balanceBefore + 1
);
// only selected function can change balances
assert balanceBefore != balanceAfter => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: ownership can only change through mint, burn or transfers. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule ownershipChange(env e, uint256 tokenId) {
require nonzerosender(e);
requireInvariant zeroAddressHasNoApprovedOperator(e.msg.sender);
address ownerBefore = unsafeOwnerOf(tokenId);
method f; helperSoundFnCall(e, f);
address ownerAfter = unsafeOwnerOf(tokenId);
assert ownerBefore == 0 && ownerAfter != 0 => (
f.selector == sig:mint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256).selector ||
f.selector == sig:safeMint(address,uint256,bytes).selector
);
assert ownerBefore != 0 && ownerAfter == 0 => (
f.selector == sig:burn(uint256).selector
);
assert (ownerBefore != ownerAfter && ownerBefore != 0 && ownerAfter != 0) => (
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: token approval can only change through approve or transfers (implicitly). │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvalChange(env e, uint256 tokenId) {
address approvalBefore = unsafeGetApproved(tokenId);
method f; helperSoundFnCall(e, f);
address approvalAfter = unsafeGetApproved(tokenId);
// approve can set any value, other functions reset
assert approvalBefore != approvalAfter => (
f.selector == sig:approve(address,uint256).selector ||
(
(
f.selector == sig:transferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector ||
f.selector == sig:burn(uint256).selector
) && approvalAfter == 0
)
);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rules: approval for all tokens can only change through isApprovedForAll. │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approvedForAllChange(env e, address owner, address spender) {
bool approvedForAllBefore = isApprovedForAll(owner, spender);
method f; helperSoundFnCall(e, f);
bool approvedForAllAfter = isApprovedForAll(owner, spender);
assert approvedForAllBefore != approvedForAllAfter => f.selector == sig:setApprovalForAll(address,bool).selector;
}
Ejecución del Prover: link
Una nota sobre la diferencia entre usar reglas parcialmente paramétricas o completamente paramétricas
Estas propiedades de cambio de estado se pueden verificar utilizando una sola regla parcialmente paramétrica o varias reglas completamente paramétricas (una por propiedad). Ambos enfoques usan method f para razonar sobre los cambios de estado en todos los métodos del contrato, pero difieren en cómo se define el alcance de las precondiciones.
En una regla completamente paramétrica, todas las precondiciones se aplican a nivel de regla y, por lo tanto, restringen todas las posibles invocaciones a métodos. Esto funciona bien cuando se aplican las mismas precondiciones a todos los métodos que afectan el estado que se está verificando.
Por otro lado, una regla parcialmente paramétrica utiliza lógica condicional basada en el método invocado. En lugar de aplicar precondiciones a todas las invocaciones a métodos, enruta la llamada al método arbitrario a ramas específicas del método, cada una con sus propias precondiciones relevantes. Las precondiciones se aplican solo donde se requieren, lo cual funciona bien cuando una regla verifica múltiples aserciones que requieren diferentes restricciones específicas del método.
La elección entre ellas es principalmente sobre la organización del código: las reglas parcialmente paramétricas centralizan la lógica específica del método, mientras que las reglas completamente paramétricas separan las responsabilidades en reglas independientes. Esta diferencia organizativa afecta el mantenimiento y la claridad, pero ambos enfoques son igualmente válidos cuando las precondiciones tienen el alcance adecuado.
Este artículo es parte de una serie sobre verificación formal utilizando Certora Prover