¬ŅEn qu√© consiste la verificaci√≥n formal de los contratos inteligentes?
Inicio
Artículos
¬ŅEn qu√© consiste la verificaci√≥n formal de los contratos inteligentes?

¬ŅEn qu√© consiste la verificaci√≥n formal de los contratos inteligentes?

Avanzado
Publicación: Mar 2, 2023Actualización: Jul 12, 2023
5m

Este artículo es una contribución de la comunidad. El autor es David Tarditi, vicepresidente de Ingeniería de Certik, una empresa de auditoría de contratos inteligentes Web3.

Resumen

La verificación formal de los contratos inteligentes garantiza que estos estén libres de bugs, vulnerabilidades y otros comportamientos no deseados. La realiza un experto humano que presenta la lógica del contrato inteligente como enunciados matemáticos, luego los ejecuta a través de un proceso automatizado que verifica la lógica real contra los modelos de comportamiento esperado del contrato inteligente. La combinación de la verificación formal y la auditoría manual proporciona una evaluación integral de la seguridad de un contrato inteligente.

Introducción

Los contratos inteligentes son programas informáticos implementados en una blockchain que se ejecutan automáticamente cuando se cumplen ciertas condiciones. Pueden variar de simples a extremadamente complejos, y pueden contener activos por valor de millones o incluso miles de millones de dólares.  

Las vulnerabilidades de seguridad en el código de los contratos inteligentes pueden traer consecuencias graves, incluido el robo de todos los activos del contrato inteligente. En 2021, el Automated Market Maker (AMM) Uranium Finance sufrió un robo de 50 millones de dólares por un error tipográfico en un contrato inteligente.

También en 2021, Compound Finance entregó 80 millones de dólares en recompensas no ganadas solo por carácter erróneo. En 2022, 320 millones dólares fueron robados de Wormhole Bridge a causa de un bug en uno de sus contratos inteligentes.

Es importante que el programa de contratos inteligentes sea correcto desde el inicio. Los contratos inteligentes son de c√≥digo abierto, lo que significa que, una vez implementado el contrato, el c√≥digo est√° disponible al p√ļblico. Si un hacker encuentra un bug, puede aprovecharlo de inmediato. Adem√°s, aplicar parches a las vulnerabilidades de seguridad no es una opci√≥n sostenible, ya que el c√≥digo del contrato normalmente no se puede modificar luego de implementado.

¬ŅC√≥mo funciona la verificaci√≥n de un contrato inteligente?¬†¬†

La verificación formal de los contratos inteligentes se lleva a cabo presentando la lógica y el comportamiento deseado de los contratos como enunciados matemáticos. Los auditores luego utilizan herramientas automatizadas para verificar si los enunciados son correctos.

El proceso implica:

  1. Definir las especificaciones y propiedades deseadas de un contrato en lenguaje formal.

  2. Traducir el código del contrato inteligente a una representación formal, como los modelos matemáticos y la lógica.

  3. Usar probadores de teorema automatizados o verificadores de modelos para validar las especificaciones y propiedades del contrato.

  4. Repetir el proceso de verificación para encontrar y corregir cualquier error o desviación de las propiedades deseadas.

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

El uso del razonamiento matemático ayuda a garantizar que los contratos verificados formalmente no tengan bugs, vulnerabilidades y otros comportamientos no deseados. También ayuda a aumentar la confianza en el contrato, ya que se probó rigurosamente que sus propiedades son correctas. 

A continuación incluimos algunos ejemplos de cómo la verificación de los contratos inteligentes ha ayudado a prevenir pérdidas financieras significativas y otros resultados graves.  

Uniswap

Uniswap es un AMM conocido. Cuando se desarrolló la primera versión del contrato inteligente de Uniswap, se verificó formalmente. Antes de su lanzamiento, esta verificación formal encontró y corrigió errores de redondeo que pudieron haber generado el drenado de los fondos de Uniswap V1. 

Balancer

Balancer V2 también es conocido como un AMM que se verificó formalmente. La verificación formal encontró y corrigió un cálculo de comisiones incorrecto relacionado con la funcionalidad de los préstamos flash en el contrato inteligente, lo cual podría haber dejado al exchange vulnerable al robo.

SafeMoon

SafeMoon V1 conten√≠a un bug sutil que se descubri√≥ en la verificaci√≥n formal luego de la implementaci√≥n del contrato. Si se hac√≠an ciertas operaciones antes de renunciar a la propiedad del contrato, era posible para el due√Īo del contrato renunciar a la propiedad y luego readquirirla.

Este bug pasó desapercibido en la mayoría de las auditorías manuales de los forks de SafeMoon V1 porque encontrarlo requería analizar combinaciones específicas de los valores variables del programa. Esto es algo que escapa fácilmente al control humano, pero que descubre fácilmente una máquina.

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

La verificaci√≥n formal proporciona una manera sistem√°tica y automatizada de corroborar la l√≥gica y el comportamiento de un contrato en relaci√≥n con sus propiedades deseadas, lo que facilita la identificaci√≥n y correcci√≥n de potenciales errores y bugs. Es especialmente √ļtil para encontrar problemas complejos y sutiles que pueden pasar desapercibidos en la inspecci√≥n manual.

La auditor√≠a manual implica la revisi√≥n experta del c√≥digo, dise√Īo e implementaci√≥n del contrato. El auditor utiliza su experiencia y habilidad para identificar los riesgos de seguridad y evaluar la postura general de seguridad del contrato. Tambi√©n puede confirmar que el proceso de verificaci√≥n formal se haya realizado correctamente, as√≠ como revisar cualquier problema que no sea detectable por herramientas automatizadas.¬†

La combinaci√≥n de la verificaci√≥n formal y la auditor√≠a manual proporciona una evaluaci√≥n integral y exhaustiva de la seguridad del contrato inteligente, lo que aumenta las probabilidades de encontrar y corregir cualquier vulnerabilidad que pueda contener. El resultado es un enfoque de defensa profunda en torno a la seguridad que aprovecha las capacidades √ļnicas de los humanos y de las m√°quinas.¬†

Conclusiones

Para garantizar la seguridad de los contratos inteligentes, es esencial seguir una verificación formal y también una auditoría manual, de esta manera se asegura una evaluación integral y exhaustiva de la postura de seguridad del contrato inteligente.

Aunque la verificaci√≥n formal puede requerir muchos recursos, vale la pena la inversi√≥n en el caso de contratos con factores de alto valor o alto riesgo. Por √ļltimo, es fundamental priorizar la seguridad y asegurarse de que los contratos inteligentes no tengan bugs, vulnerabilidades y comportamientos no deseados.

Lecturas adicionales

Aviso legal y advertencia de riesgo: Este contenido se presenta "tal cual" √ļnicamente para fines de informaci√≥n general y educativos, sin representaci√≥n ni garant√≠a de ning√ļn tipo. No debe interpretarse como un asesoramiento financiero, ni pretende recomendar la compra de ning√ļn producto o servicio espec√≠fico. Los precios de los activos digitales son vol√°tiles. El valor de una inversi√≥n puede bajar o subir, y podr√≠a darse el caso de que no recuperes el monto invertido. Solo t√ļ eres responsable de tus decisiones de inversi√≥n. Binance Academy no se responsabiliza de ninguna p√©rdida en la que puedas incurrir. Este material no se debe interpretar como un asesoramiento financiero.