Introducción
En el capítulo anterior, demostramos que los hooks Sstore son necesarios para verificar propiedades que involucran cambios en los valores de los mapeos. El hook monitorea las escrituras en el almacenamiento, captura los valores antiguos y nuevos para cada clave, y ejecuta código CVL personalizado para actualizar las variables ghost.
Lo demostramos utilizando un contrato simple PointSystem que añade puntos a un usuario, los registra en pointsOf[address] y actualiza el total en totalPoints:
contract PointSystem {
mapping (address => uint256) public pointsOf;
uint256 public totalPoints;
function addPoints(address _user, uint256 _amount) external {
pointsOf[_user] += _amount;
totalPoints += _amount;
}
}
Sin embargo, en la práctica, los contratos se optimizan para la eficiencia de gas y utilizan bloques unchecked en casos donde el desbordamiento (overflow) es prácticamente imposible. Por ejemplo, el contrato PointSystem anterior puede usar un bloque unchecked y ser implementado de una manera en la que no pueda desbordarse.
El siguiente contrato demuestra esto: un bloque unchecked se usa de manera segura al añadir a pointsOf[address]:
contract PointSystemUnchecked {
mapping (address => uint256) public pointsOf;
uint256 public totalPoints;
function addPoints(address _user, uint256 _amount) external {
totalPoints += _amount;
unchecked {
pointsOf[_user] += _amount;
}
}
}
Esto funciona porque totalPoints += _amount se ejecuta primero sin unchecked, por lo que revierte en caso de overflow y actúa como un cortocircuito. Dado que cada incremento a pointsOf[_user] también incrementa totalPoints, ningún usuario puede acumular más puntos que los puntos totales.
Sin embargo, el Prover no tiene en cuenta este razonamiento. En el momento en que añadimos un bloque unchecked, el Prover deja de asumir la seguridad aritmética. Esto significa que asignará intencionalmente estados iniciales que desencadenen un comportamiento de reinicio cíclico (wraparound) en las operaciones unchecked.
El Prover no asume seguridad aritmética en bloques unchecked
Para demostrarlo, ejecutemos nuestras especificaciones para PointSystem en el nuevo contrato PointSystemUnchecked. A continuación se muestran las especificaciones (tanto el invariante como la regla), que ahora fallan debido al bloque unchecked:
ghost mathint g_sumOfUserPoints {
init_state axiom g_sumOfUserPoints == 0;
}
hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}
invariant sumOfUserPointsEqualsTotalPoints_i() // fails
totalPoints() == g_sumOfUserPoints;
rule sumOfUserPointsEqualsTotalPoints_r(env e, method f, calldataarg args) { // fails
require totalPoints() == 0 && g_sumOfUserPoints == 0;
f(e, args);
assert totalPoints() == g_sumOfUserPoints;
}
Ejecución del Prover (fallo): link
Esto plantea la pregunta: ¿por qué totalPoints y g_sumOfUserPoints divergen cuando se usa el bloque unchecked? La respuesta es que el bloque unchecked hace que el Prover asigne un valor inicial distinto de cero a un usuario arbitrario (pointsOf[address]) para crear un escenario de overflow a lo largo de la ruta de ejecución, mientras que totalPoints comienza en cero (el estado inicial real). Como resultado, el Prover probó un estado donde los puntos de un usuario son mayores que los puntos totales, un estado imposible en el contrato.
El Prover establece estados iniciales para provocar intencionalmente un overflow
Ahora, analicemos la traza de llamadas para la regla y el invariante que escribimos para entender cómo se produjo la violación, un falso positivo.
Traza de llamadas de la regla
El Prover asigna un valor distinto de cero a la dirección 0xf (pointsOf[0xf] = 0x2) para que más tarde, al sumar un valor suficientemente grande dentro del rango de uint256, pueda simular un overflow:
Luego se ejecuta la llamada addPoints(_user=0xf, _amount=2^256 - 2), lo que da como resultado pointsOf[address] = 0x2 + (2^256 - 2) = 2^256 ≡ 0 (el nuevo valor da la vuelta a cero debido al overflow):
Invocar addPoints() también suma a totalPoints en el contrato. Dado que totalPoints es inicialmente cero, sumar 2^256 - 2 (el argumento) da como resultado un valor final de 2^256 - 2, como se muestra en la traza a continuación:
Ahora, veamos cómo la lógica del hook Sstore calcula g_sumOfUserPoints:
hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}
Valores iniciales:
g_sumOfUserPoints = 0(valor inicial)pointsOf[0xf] (oldVal) = 0x2(valor inicial)
Valores posteriores a la llamada después de addPoints(0xf, 2^256 - 2):
pointsOf[0xf] (newVal) = 0x0(valor reiniciado tras dar la vuelta después de sumar0x2y2^256 - 2)pointsOf[0xf] (oldVal) = 0x2g_sumOfUserPoints = 0 + (0x0 - 0x2) = -0x2
Por lo tanto, totalPoints (2^256 - 2) ya no es igual a g_sumOfUserPoints(-2):
Traza de llamadas del invariante
El mismo problema ocurrió con el invariante. El Prover sembró intencionalmente pointsOf[address] = 0xc00…000, que es mayor que totalPoints en el estado previo a la llamada:
No necesitamos otra traza de llamadas para ver que, en el estado final, ocurren inconsistencias contables, y estas causan que totalPoints difiera de g_sumOfUserPoints.
El problema central
Tanto totalPoints como g_sumOfUserPoints comienzan en cero (como se muestra en la precondición de la regla y el axioma init_state del invariante), pero el Prover establece pointsOf[user] en un valor distinto de cero para probar una ruta de overflow.
La razón es que no puede ocurrir un overflow si pointsOf[user] comienza en cero. Sumar el valor max_uint256 a cero solo alcanza el límite de uint256, no lo sobrepasa. Para producir un overflow en la operación unchecked pointsOf[_user] += _amount, el valor inicial de pointsOf[_user] ya debe ser mayor que cero; por ejemplo, 2 + (2²⁵⁶ − 2) = 2²⁵⁶ ≡ 0.
Esta configuración crea un estado irreal donde pointsOf[user] > 0 mientras que totalPoints = 0, lo cual no puede ocurrir en una ejecución real ya que ambos valores siempre cambian juntos dentro de addPoints().
Definición de la relación realista entre la variable ghost y el almacenamiento
Veamos de nuevo la implementación del hook Sstore.
El hook Sstore actualiza la variable ghost g_sumOfUserPoints sumando el cambio (newVal - oldVal) de cada escritura en pointsOf[address]
hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}
Sin embargo, el Prover no conoce la relación realista entre la variable ghost g_sumOfUserPoints y el almacenamiento pointsOf[address].
La variable g_sumOfUserPoints simplemente acepta los valores que procesa, y el Prover no puede determinar el valor realista de pointsOf[address] para introducirlo en g_sumOfUserPoints. Como resultado, el Prover prueba todos los valores posibles, incluidos los irreales que pueden causar fallos.
Lo que debemos hacer a continuación es instruir explícitamente al Prover sobre la relación prevista entre los puntos de cada usuario individual (pointsOf[user]) y la suma de los puntos de los usuarios (g_sumOfUserPoints): g_sumOfUserPoints siempre debe ser mayor o igual a pointsOf[user]. Podemos imponer esta relación usando el hook Sload.
Sintaxis del hook Sload para mapeos
Antes de continuar, veamos primero la sintaxis y el patrón de los hooks Sload para mapeos. La sintaxis para los hooks es la misma que para las variables simples, excepto que para los mapeos debemos incluir la palabra clave KEY. Por ejemplo: storageVar[KEY address user]:
hook Sload uint256 val balances[KEY address user] {
// implement hook logic
}
En un hook Sload, la variable local del hook val captura el valor leído del mapeo de almacenamiento con la clave user.
En una operación de contrato, las lecturas de almacenamiento ocurren antes de que la variable sea actualizada o procesada. Por ejemplo, en esta línea de Solidity pointsOf[_user] += _amount, pointsOf[_user] debe leer su valor actual antes de sumar _amount.
Por lo tanto, es importante que el “valor leído” del mapeo de almacenamiento sea preciso antes de que sus datos se procesen y se asignen a una variable ghost (a través de los hooks Sstore).
Dado que el Prover no conoce la relación entre las variables de almacenamiento y las variables ghost, debemos definir explícitamente esta relación de la siguiente manera:
hook Sload uint256 points pointsOf[KEY address account] {
require g_sumOfUserPoints >= points;
}
Aquí, points es la variable local del hook que captura el valor leído del mapeo pointsOf[address]. Esta implementación restringe al Prover a explorar solo los estados en los que g_sumOfUserPoints es mayor o igual a points.
Alternativamente, podemos pensar en el require como una restricción al valor de pointsOf[address] (los puntos de cualquier usuario en particular) para que siempre sea menor o igual a g_sumOfUserPoints. Esto significa que el Prover nunca probará un escenario en el que los puntos de un usuario individual excedan los puntos totales rastreados por la variable ghost.
El uso del hook Sload soluciona las inconsistencias entre las variables ghost y el almacenamiento
En nuestra especificación, añadimos el hook Sload mostrado arriba para obligar a que la variable ghost que representa la suma de todos los puntos (g_sumOfUserPoints) siempre sea mayor o igual a cualquier valor individual de pointsOf[account] cuando se lea desde el almacenamiento.
Esto evita que el Prover inicialice un estado en el que el balance de una sola cuenta exceda la suma total, una situación que, como hemos visto, genera falsos positivos.
hook Sload uint256 points pointsOf[KEY address account] {
require g_sumOfUserPoints >= points;
}
Con esto en marcha, tanto la regla CVL como el invariante tienen éxito, y la propiedad es verificada:
Ejecución del Prover (verificado): link
Resumen
- El bloque
uncheckeddesactiva las comprobaciones de overflow integradas de Solidity, lo que hace que el Prover explore aritmética insegura asignando valores iniciales que provocan overflows para probar la implementación. - Estos valores iniciales irreales pueden prevenirse utilizando
requireen el hookSload, de modo que el Prover explore estados únicamente dentro de los límites especificados, como requerir que el valor de un punto individual no exceda el total.
Este artículo forma parte de una serie sobre verificación formal usando el Certora Prover