¿Qué es la verificación formal de contratos inteligentes?

La verificación formal de contratos inteligentes puede evitar que presenten errores, vulnerabilidades y otras situaciones adversas. En este proceso, expertos humanos convierten la lógica del contrato inteligente en enunciados matemáticos y luego utilizan procesos automatizados para verificar mediante model checking si la lógica real coincide con el comportamiento esperado del contrato. Al combinar la verificación formal con auditorías manuales, podemos realizar una evaluación integral de la seguridad de los contratos inteligentes.

Introducción

Los contratos inteligentes son programas informáticos desplegados en blockchain que se ejecutan automáticamente cuando se cumplen ciertas condiciones. Los contratos inteligentes pueden ser muy simples o extremadamente complejos, y pueden poseer activos por valor de millones o incluso miles de millones de dólares.

Si el código de un contrato inteligente tiene vulnerabilidades de seguridad, puede causar consecuencias devastadoras, como el robo de todos los activos que posee. En 2021, debido a un error ortográfico en un contrato inteligente, el Automated Market Maker(AMM)Uranium Finance fue robado por 50 millones de dólares.

También en 2021, debido a un error en el código, Compound Finance distribuyó incorrectamente 80 millones de dólares en recompensas. En 2022, debido a un error en un contrato inteligente, el puente Wormhole Bridge fue robado por 320 millones de dólares.

Por lo tanto, es importante hacer que el programa del contrato inteligente sea correcto desde el principio. Los contratos inteligentes utilizan un modelo de código abierto, lo que significa que una vez desplegado, el código será público. Si los hackers descubren errores en él, pueden explotarlos inmediatamente. Además, con el tiempo, las operaciones rutinarias para parchear vulnerabilidades de seguridad no serán efectivas, ya que el código del contrato inteligente generalmente no puede modificarse después del despliegue.

¿Cómo funciona la verificación de contratos inteligentes?

La verificación formal de contratos inteligentes se realiza presentando la lógica y el comportamiento esperado del contrato en forma de enunciados matemáticos. Luego, los auditores utilizan herramientas automatizadas para comprobar si estos enunciados son correctos.

El proceso implica:

Definir formalmente las especificaciones y características esperadas del contrato.

Convertir el código del contrato en declaraciones formales, como modelos matemáticos o lógica.

Utilizar pruebas de teoremas automatizadas o detección de modelos para verificar las especificaciones y características del contrato.

Repetir la verificación para detectar y corregir cualquier error o desviación de las características esperadas.

Por qué la verificación de contratos inteligentes es importante

Mediante el uso del razonamiento matemático, ayuda a garantizar que los contratos inteligentes verificados formalmente eviten errores, vulnerabilidades y otras situaciones adversas. La verificación también aumenta la confianza en el contrato, ya que sus características han sido sometidas a rigurosas pruebas, siendo correctas y confiables.

Los siguientes ejemplos ilustran cómo la verificación de contratos inteligentes puede ayudar a prevenir pérdidas financieras importantes y otros resultados catastróficos.

Uniswap

Uniswap es un conocido AMM. Durante el desarrollo de Uniswap V1, se realizó una verificación formal. Antes del lanzamiento, esta verificación detectó y corrigió algunos errores de redondeo, evitando que los fondos de Uniswap V1 fueran drenados por completo.

Balancer

Balancer V2 también es un AMM verificado. La verificación formal detectó y corrigió un error en el cálculo de tarifas en la función de préstamos flash, que podría haber facilitado robos en la plataforma.

SafeMoon

SafeMoon V1, tras su despliegue, mediante verificación formal, detectó un error extremadamente pequeño. Si este error no se hubiera detectado, el propietario del contrato podría haber recuperado el contrato después de renunciar a la propiedad, realizando ciertas operaciones antes de hacerlo.

La mayoría de las auditorías manuales de bifurcaciones de SafeMoon V1 pasaron por alto este error, ya que requería analizar combinaciones específicas de valores de variables del programa para detectarlo. Es fácil que los humanos pasen por alto este problema, pero las máquinas pueden detectarlo a tiempo.

Cómo complementan la verificación formal y la auditoría manual

La verificación formal proporciona un método sistemático y automatizado para comprobar la lógica y el comportamiento del contrato según sus características esperadas. Esto facilita la identificación y corrección de errores o vulnerabilidades potenciales, especialmente en problemas complejos y sutiles que son difíciles de detectar manualmente.

Por otro lado, la auditoría manual implica que expertos revisen el código, el diseño y el despliegue del contrato. Los auditores utilizan su experiencia y conocimientos especializados para identificar riesgos de seguridad y evaluar la seguridad general del contrato. También pueden verificar si el proceso de verificación formal se ha llevado a cabo correctamente y detectar problemas que las herramientas automatizadas puedan no captar.

Al combinar la verificación formal con la auditoría manual, podemos realizar una evaluación completa de la seguridad del contrato inteligente. Esto aumenta las probabilidades de detectar y corregir vulnerabilidades. Así, se adopta una estrategia de defensa en profundidad que aprovecha las fortalezas tanto humanas como mecánicas.

Conclusión

Para garantizar la seguridad de los contratos inteligentes, es fundamental combinar la verificación formal con auditorías manuales, asegurando una evaluación exhaustiva y completa de su estado de seguridad.

Aunque la verificación formal requiere recursos elevados, para contratos de alto valor o alto riesgo, es una inversión que vale la pena. Al fin y al cabo, la seguridad es lo primero, y se debe priorizar la protección contra errores, vulnerabilidades y comportamientos no deseados en los contratos inteligentes. **$BNT **$BROCCOLI