Este artículo fue publicado por un miembro 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 los protege de errores, vulnerabilidades y otras condiciones adversas. En este proceso, los expertos humanos convierten la lógica del contrato inteligente en declaraciones matemáticas y luego utilizan un proceso automatizado para comparar la lógica real con un modelo del comportamiento esperado del contrato. Combinando la verificación formal y la auditoría manual, podemos realizar una evaluación integral de la seguridad de los contratos inteligentes.
Introducción
Los contratos inteligentes son programas informáticos implementados en la cadena de bloques que se ejecutan automáticamente cuando se cumplen determinadas condiciones. Los contratos inteligentes pueden ser muy simples o extremadamente complejos y pueden contener activos por valor de millones o incluso miles de millones de dólares.
Si hay agujeros de seguridad en el código de contrato inteligente, puede tener consecuencias devastadoras, como el robo de todos los activos en poder de los delincuentes. En 2021, se robaron 50 millones de dólares del creador de mercado automatizado (AMM) Uranium Finance debido a un error tipográfico en un contrato inteligente.
También en 2021, Compound Finance emitió por error 80 millones de dólares en recompensas debido a un único error de codificación. En 2022, se robaron 320 millones de dólares del puente Wormhole debido a un error en el contrato inteligente.
Por lo tanto, es importante implementar correctamente su programa de contrato inteligente desde el principio. Los contratos inteligentes adoptan un modelo de código abierto, lo que significa que una vez que se implementa el contrato, el código se hace público. Si un pirata informático descubre un error, puede explotarlo inmediatamente. Además, la práctica normal de parchear las vulnerabilidades de seguridad a lo largo del tiempo es ineficaz porque el código de los contratos inteligentes a menudo no se puede modificar después de la implementación.
¿Cómo funciona la verificación de contratos inteligentes?
La verificación formal de los contratos inteligentes se logra presentando la lógica y el comportamiento esperado del contrato inteligente como declaraciones matemáticas. Luego, los auditores utilizan herramientas automatizadas para comprobar si estas declaraciones son correctas.
El proceso implica:
Definir las especificaciones y características esperadas del contrato en un lenguaje formal.
Convierta el código de un contrato en una declaración formal, como un modelo matemático o lógica.
Verifique las especificaciones y propiedades del contrato mediante la demostración automatizada de teoremas o la verificación de modelos.
Repita el proceso de validación para encontrar y corregir errores o desviaciones de las características esperadas.
Por qué es importante la verificación de contratos inteligentes
Al aplicar el razonamiento matemático, se ayuda a garantizar que los contratos inteligentes verificados formalmente estén libres de errores, vulnerabilidades y otras situaciones adversas. La verificación también ayuda a aumentar la confianza en el contrato porque sus propiedades han sido rigurosamente probadas y son correctas y confiables.
Los siguientes ejemplos describen cómo la verificación de contratos inteligentes puede ayudar a prevenir pérdidas financieras significativas y otras consecuencias catastróficas.
Uniswap
Uniswap es una AMM muy conocida. El contrato inteligente Uniswap V1 se sometió a una verificación formal durante el proceso de desarrollo. Antes del lanzamiento, esta verificación formal encontró y solucionó algunos errores de redondeo, lo que impidió que Uniswap V1 se quedara sin fondos.
Balancín
Balancer V2 también es un AMM probado. La verificación formal descubrió y solucionó un error de cálculo de tarifas en la función de préstamo rápido del contrato inteligente que dejaba a la plataforma comercial vulnerable al robo.
Luna Segura
Después de la implementación de SafeMoon V1, se descubrió un error muy pequeño mediante una verificación formal. Si el propietario del contrato realizó ciertas operaciones antes de renunciar a la propiedad, el propietario del contrato podría recuperarla después de renunciar.
La mayoría de las auditorías manuales de la bifurcación SafeMoon V1 pasan por alto este error porque es necesario analizar combinaciones específicas de valores de variables del programa para encontrarlo. Los humanos pueden pasar por alto este problema fácilmente, pero las máquinas pueden detectarlo a tiempo.
Cómo funcionan juntas la verificación formal y la auditoría manual
La verificación formal proporciona una forma sistemática y automatizada de comparar la lógica y el comportamiento de un contrato con sus características esperadas. Esto facilita la identificación y corrección de posibles errores o vulnerabilidades. Esto es particularmente útil para problemas complejos y sutiles que serían difíciles de detectar mediante una inspección manual.
La auditoría manual implica que expertos revisen el código, el diseño y la implementación del contrato. Los auditores utilizan su experiencia y conocimientos para identificar riesgos de seguridad y evaluar la situación general de seguridad del contrato. También pueden confirmar que el proceso de verificación formal se realiza correctamente y comprobar si hay problemas que las herramientas automatizadas no puedan detectar.
Combinando la verificación formal y la auditoría manual, podemos realizar una evaluación integral de la seguridad de los contratos inteligentes. Esto mejora las probabilidades de encontrar y corregir vulnerabilidades. Al hacerlo, estamos adoptando un enfoque de seguridad de defensa en profundidad que combina la experiencia de humanos y máquinas.
Conclusión
Para garantizar la seguridad de los contratos inteligentes, se debe combinar la verificación formal y la auditoría manual para garantizar una evaluación integral y exhaustiva de la postura de seguridad de los contratos inteligentes.
Aunque la verificación formal requiere más recursos, es una inversión que vale la pena para contratos con alto valor o factores de alto riesgo. Después de todo, al final del día, la seguridad es más importante que cualquier otra cosa. Asegúrese de priorizar la seguridad y garantizar que los contratos inteligentes estén libres de errores, vulnerabilidades y comportamientos adversos inesperados.
Otras lecturas
¿Qué es un contrato inteligente?
¿Qué es la auditoría de seguridad de contratos inteligentes?
Descargo de responsabilidad y advertencia de riesgo: el contenido de este artículo son hechos y tienen fines educativos y de información general únicamente y no constituyen ninguna representación o garantía. Este artículo no debe interpretarse como un asesoramiento financiero y no recomienda la compra de ningún producto o servicio específico. Los precios de los activos digitales pueden fluctuar. El valor de su inversión puede aumentar o disminuir y es posible que no recupere el capital invertido. Usted es el único responsable de sus propias decisiones de inversión y Binance Academy no es responsable de las pérdidas que pueda sufrir. Este material no constituye asesoramiento financiero.
