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:
Definir las especificaciones y propiedades deseadas de un contrato en lenguaje formal.
Traducir el código del contrato inteligente a una representación formal, como los modelos matemáticos y la lógica.
Usar probadores de teorema automatizados o verificadores de modelos para validar las especificaciones y propiedades del contrato.
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.