La verificación formal es el proceso de demostrar matemáticamente que un programa cumple con una especificación.

Este artículo introduce conceptualmente cómo funciona la verificación formal, cómo se compara con el fuzzing, y las limitaciones y ventajas de la verificación formal.

Definición de “especificación”

Una especificación es un comportamiento bien definido bajo circunstancias específicas.

Aquí hay algunos ejemplos de especificaciones que se aplican a los contratos inteligentes de DeFi:

(1) Los prestamistas no deberían ganar intereses si no ha pasado el tiempo.

(2) Si ha pasado el tiempo y hay préstamos activos, el prestamista debería ganar un interés mayor a cero.

(3) Si el protocolo no está pausado, los prestatarios siempre pueden pagar sus préstamos.

(4) Si no se ha superado el límite de suministro y el protocolo no está pausado, los prestamistas siempre pueden depositar.

La verificación formal también nos permite razonar sobre el estado interno de un contrato. Podemos escribir especificaciones como las siguientes, que inspeccionan únicamente las variables de almacenamiento:

(5) Para cualquier secuencia de transacciones, la suma de los balances de un token ERC-20 debería ser igual al suministro total.

(6) Si no se llama a deposit(), entonces un balance no puede aumentar.

Supongamos que tuviéramos una forma de saber con certeza que “(1) Los prestamistas no deberían ganar intereses si no ha pasado el tiempo”. En ese caso, sabemos que el vector de ataque particular de robar dinero del protocolo a través de intereses que no deberían haberse ganado es imposible. Aunque no garantizamos que el protocolo no tenga errores (bugs), sabemos que no tiene un error particular.

Consideremos las implicaciones si se viola la especificación “(2) Si ha pasado el tiempo y hay préstamos activos, el prestamista debería ganar un interés mayor a cero”. Esto significa que alguien está pidiendo dinero prestado, pero el prestamista no está ganando intereses. Eso significa que ocurre una de las siguientes situaciones:

• un error en el que el protocolo está ganando los intereses, pero no el prestamista
• el prestatario está pagando intereses que van a alguna cuenta a la que no deberían ir, o los intereses se están quemando
• el prestatario no está pagando ningún interés

Lo bueno de saber con certeza que la especificación 2 se cumple es que sabemos que ninguno de los errores anteriores se aplica al protocolo.

Si 3 y 4 se cumplen, se eliminan categorías enteras de ataques de denegación de servicio. Si un atacante tuviera una forma de evitar que los prestatarios paguen, entonces podría forzar a los prestatarios a acumular intereses y luego liquidarlos para obtener una ganancia injusta. Por otro lado, si los atacantes pueden bloquear los depósitos de los prestamistas, entonces un competidor malicioso podría intentar alejar la liquidez de ese protocolo evitando los depósitos en primer lugar.

Si 5 y 6 se cumplen, podemos estar seguros de que no hay errores relacionados con desajustes contables en las variables de almacenamiento del ERC-20.

La verificación formal solo puede detectar los errores para los cuales creamos una especificación. Usando el ejemplo del ERC-20, si dejamos la función burn(address from, uint256 amount) desprotegida (es decir, dejamos que cualquiera la llame; no hay control de acceso), ninguna de las especificaciones anteriores detectará la falta de control de acceso.

La herramienta de verificación formal que estudiaremos en esta serie, Certora Prover, razona sobre los contratos inteligentes a nivel del bytecode. Esto significa que si el compilador introduce un error, entonces la verificación formal puede detectarlo, siempre y cuando el error resulte en una violación de una de nuestras especificaciones.

Una especificación como una declaración sobre las transiciones de estado

Usando la especificación “la suma de todos los balances de un token ERC-20 debería ser igual al suministro total”, la herramienta de verificación formal definiría dos cosas:

1. Una función de transición de estado $\phi$
2. Una representación del estado (una colección de valores en un momento determinado, como las variables de estado de un contrato y los balances de las cuentas de Ethereum), al que simplemente llamamos $\texttt{state}$. Podemos referirnos a un estado particular como $\texttt{state}_i$ y a un estado diferente como $\texttt{state}_j$. También podemos referirnos a $\texttt{state}_{i+1}$, que es el estado posterior a una transacción que ocurrió durante $\texttt{state}_i$ y provocó que cambiaran algunas variables de almacenamiento o balances de cuentas.

La primera es una función de transición de estado $\phi$ que, dado un estado (como las variables de almacenamiento y los balances de las cuentas), el entorno (como el block timestamp) y la calldata de una transacción, produce un nuevo estado:

Esta función $\phi$ es una representación matemática del bytecode del contrato inteligente. Entonces, nuestra especificación “la suma de todos los balances es igual al suministro total” se compilaría a la siguiente fórmula matemática:

En otras palabras, para cualquier estado $i$, la suma de los balances $\left(\sum_a\texttt{state}_i\texttt{.balances}_a\right)$ en ese estado para cada cuenta $a$ es igual al total_supply de ese estado.

Ahora supongamos que se nos da una función de transición de estado $\phi:\texttt{state}\rightarrow\texttt{state}'.$ Queremos saber si, para cualquier $\texttt{state}$ insertado en $\phi$ que obedece la fórmula anterior, el estado resultante $\texttt{state}'$ también obedece la fórmula. (Ten en cuenta que nuestra especificación es independiente de $\phi$).

El Prover luego intentaría demostrar por inducción (no te preocupes si este término no te resulta familiar; hablaremos de él en un capítulo posterior) que si $\texttt{state}_i$ sigue la especificación anterior, entonces cualquier estado que venga después también debe seguir la especificación.

$\phi$ es el contrato inteligente en sí, ya que toma un estado, una calldata y un entorno para producir un nuevo estado. La fórmula que escribimos anteriormente es una propiedad que queremos asegurar que tiene el contrato inteligente.

Como beneficio adicional, si hay un $\text{state}$ y una $\texttt{calldata}$ que conducen a una violación, Certora Prover proporcionará un ejemplo de ello.

El enorme beneficio de una herramienta automática de verificación formal como Certora Prover es que descubre la función $\phi$ por nosotros, traduciendo el bytecode del contrato inteligente en una función matemática de las variables de estado, la calldata y las variables de entorno. Este es un proceso inmensamente complejo que requiere una investigación y desarrollo sustanciales, pero afortunadamente podemos tratarlo en su mayoría como una caja negra (existen algunas excepciones importantes que exploraremos más adelante).

Ejemplo de especificación

Nuestro ejemplo de “los prestamistas no deberían ganar intereses si no ha pasado el tiempo” se puede expresar matemáticamente como:

Lo que esto está diciendo es “si el block timestamp de los estados $i$ y $j$ son iguales, entonces el interestEarned debe ser el mismo”.

No te preocupes si las matemáticas se sienten un poco extrañas de leer. Podemos traducirlo como:

• $\forall_{i,j}$ significa “para todos los $i$ y $j$” o “para cualesquiera dos valores de $i$ y $j$”
• $\texttt{state}_i\texttt{.timestamp}\texttt{ == } \texttt{state}_j\texttt{.timestamp}\rightarrow$ si esos dos estados tienen el mismo timestamp
• $\texttt{state}_i\texttt{.interestEarned == }\texttt{state}_j\texttt{.interestEarned}$ entonces el interestEarned es el mismo

Ten en cuenta que el $\rightarrow$ se comporta como un “if then” (si… entonces) en la programación normal. La sintaxis real que utiliza Certora se parece más a Solidity que a las matemáticas que tenemos arriba, pero el significado subyacente sería el mismo.

Verificación Formal vs Fuzzing

La verificación formal y el fuzzing logran el mismo propósito, pero usan estrategias diferentes para alcanzar el mismo objetivo. El fuzzing utiliza una secuencia aleatoria, pero a menudo guiada, de transacciones para intentar encontrar violaciones a los invariantes. Esto lo hacen ejecutando miles, posiblemente millones, de pruebas.

La verificación formal, por otro lado, demuestra matemáticamente que los invariantes se cumplen.

Por el contrario, el fuzzing no puede demostrar la ausencia de errores. Solo puede mostrar que el error estaba ausente en los casos que probó.

El fuzzing prueba el contrato inteligente para miles o millones de casos aleatorios. La verificación formal lo prueba para cada combinación posible de entradas y valores de las variables de almacenamiento.

Limitaciones de la Verificación Formal

La verificación formal es esencialmente escribir demostraciones matemáticas automáticamente, y puede ser bastante poderosa.

Por ejemplo, las computadoras han demostrado o han jugado un papel significativo en la demostración de lo siguiente (ejemplos tomados del artículo de Wikipedia sobre Computer Assisted Proofs):

• Cualquier mapa 2D puede colorearse con cuatro colores
• Quien juega primero en el juego Connect-4 siempre gana, siempre que realice el movimiento óptimo
• La conjetura de Kepler es cierta: si se colocan esferas en una caja, la densidad más alta de volumen ocupado por esferas empaquetadas sobre el volumen total de una caja no puede exceder $\frac{\pi}{3\sqrt{2}}$.
• Un Cubo de Rubik se puede resolver en un máximo de 20 movimientos

Como se puede ver arriba, las demostraciones matemáticas asistidas por computadora pueden ser extremadamente poderosas, pero no pueden resolver cualquier problema que se les presente (si pudieran, ya no habría problemas abiertos en matemáticas).

No necesitas saber muchas matemáticas para usar la verificación formal

Incluso si no has escrito una demostración matemática en tu vida, aún puedes usar Certora Prover. Casi todo está abstraído para el desarrollador, y los desarrolladores pueden definir las especificaciones usando un lenguaje similar a Solidity.

Sin embargo, sigue siendo útil tener cierta idea de lo que está haciendo el Prover. Por ejemplo, uno puede escribir y auditar contratos inteligentes sin saber cómo funciona la EVM, pero esto podría dar lugar a un código ineficiente. De manera similar, escribir especificaciones para Certora Prover sin tener cierta idea de lo que ocurre bajo el capó podría resultar en demostraciones que tarden demasiado en generarse.

Al igual que no intentarías almacenar un jpeg en las variables de almacenamiento de la EVM debido al alto costo, hay obstáculos que debes evitar conscientemente al usar la verificación formal.

Aquí hay algunas limitaciones fundamentales de la verificación formal:

1. El problema de la parada — dado un programa arbitrario, detectar bucles infinitos de manera confiable es matemáticamente imposible.

Si pudiéramos detectar bucles infinitos, entonces podríamos resolver fácilmente una cuestión abierta en matemáticas, la conjetura de los números primos gemelos. Ejemplos de primos gemelos son (3,5), (11,13), (17,19) — tienen una diferencia de dos.

La cuestión abierta es si existe un número infinito de estos primos. Si pudiéramos detectar bucles infinitos de manera confiable, entonces podríamos escribir un programa que busque el mayor primo gemelo posible y luego se detenga. Si el programa nunca se detiene, entonces sabemos que hay un número infinito de primos gemelos.

2. Criptografía — dada una secuencia de 32 bytes que supuestamente es la salida de un hash, ¿existe una preimagen para ese hash? Es extremadamente difícil (a todos los efectos prácticos, imposible) encontrar preimágenes para los hashes. Las demostraciones asistidas por computadora no nos permiten romper su dureza matemática.

3. Grandes sistemas de ecuaciones no lineales — los sistemas de ecuaciones no lineales con muchas variables son difíciles de resolver en un corto período de tiempo. Aquí, “lineal” significa que las variables que estamos resolviendo solo se multiplican por constantes o se suman a otras variables desconocidas.

Si dos variables desconocidas se multiplican entre sí, o se elevan a alguna potencia, entonces tenemos un sistema de ecuaciones no lineales. Si una herramienta de verificación formal tiene que resolver indirectamente un sistema de ecuaciones no lineales, entonces la herramienta podría pasar una cantidad de tiempo excesiva buscando una solución.

Cómo está estructurada esta serie de tutoriales

Esta serie de tutoriales se centra en:

1. La sintaxis de cómo escribir especificaciones para Certora Prover
2. Abundantes ejemplos para identificar patrones y adaptarlos a tu propio uso
3. Cómo evitar errores en la especificación
4. Cómo verificar formalmente protocolos DeFi reales

Cada parte de la serie se basa en conceptos de capítulos anteriores. Por esta razón, aconsejamos a los lectores seguir la serie en orden en lugar de saltarse partes.

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