Este artículo es una contribución de la comunidad. Autor: Dimitris Tsapis, vicepresidente de ingeniería de CertiK, una empresa de auditoría de contratos inteligentes web3.
TL;DR
La verificación formal garantiza que los contratos inteligentes estén libres de errores, vulnerabilidades y otros comportamientos no deseados. El proceso implica que un experto humano muestre la lógica del contrato inteligente en forma de datos matemáticos y luego la ejecute a través de un proceso de verificación automática de la lógica real con modelos del comportamiento esperado del contrato. La combinación de verificación formal y auditoría manual proporciona una evaluación integral de la seguridad de los contratos inteligentes.
la introducción
Los contratos inteligentes son programas informáticos implementados en una cadena de bloques que se ejecutan automáticamente cuando se cumplen determinadas condiciones. Van desde programas simples hasta complejos y pueden contener activos por valor de miles de millones de dólares.
Las vulnerabilidades de seguridad en el código de contrato inteligente pueden tener consecuencias devastadoras, incluido el robo de todos los activos contenidos en el contrato inteligente. Durante 2021, el creador de mercado automatizado Uranium Finance sufrió un robo de 50 millones de dólares debido a un solo error tipográfico en un contrato inteligente.
También durante 2021, el protocolo Compound Finance entregó 80 millones de dólares en recompensas no ganadas como resultado de un error de un solo token. Durante 2022, se robaron 320 millones de dólares de Wormhole Bridge como consecuencia de un error de programación en uno de sus contratos inteligentes.
Es importante que su software de contrato inteligente funcione correctamente la primera vez. Los contratos inteligentes son contratos de código abierto, lo que significa que el código está disponible para el público una vez que se publica el contrato. Si un pirata informático encuentra un error, puede explotarlo inmediatamente. Además, abordar las vulnerabilidades de seguridad a lo largo del tiempo no es una opción, ya que el código de contrato inteligente normalmente no se puede modificar una vez implementado.
¿Cómo funciona la verificación de contratos inteligentes?
La verificación formal de los contratos inteligentes funciona exponiendo la lógica y el comportamiento requeridos de los contratos inteligentes en forma de datos computacionales. Los auditores pueden utilizar herramientas automatizadas para validar los datos.
El proceso incluye lo siguiente:
Concretando las especificaciones y características deseadas del contrato en el idioma oficial.
Traducir el código del contrato a una presentación formal, como modelos o marcos lógicos matemáticos.
Usar herramientas de prueba de teoremas o verificación de modelos para auditar las especificaciones y propiedades del contrato.
Repita el proceso de verificación para encontrar y corregir cualquier error o desviación de las características requeridas.
¿Por qué es importante la verificación de contratos inteligentes?
El uso del razonamiento matemático ayuda a garantizar que los contratos inteligentes verificados formalmente estén libres de errores, vulnerabilidades y otros comportamientos no deseados. También ayuda a aumentar la confianza en el contrato, ya que sus propiedades han sido cuidadosamente verificadas.
A continuación se muestran algunos ejemplos de cómo la verificación de contratos inteligentes puede ayudar a prevenir pérdidas financieras importantes y otras consecuencias nefastas.
Uniswap
Uniswap es un conocido creador de mercado automatizado. Cuando se desarrolló el contrato inteligente Uniswap V1, se verificó oficialmente. Antes de su lanzamiento, este proceso de verificación oficial pudo encontrar y corregir errores de redondeo que habrían llevado al robo de fondos de Uniswap V1.
Balancín
Balancer V2 también es un creador de mercado automatizado verificado oficialmente. El proceso de verificación oficial pudo encontrar y corregir cuentas de tarifas incorrectas e incluyó una función de préstamo rápido en el contrato inteligente, lo que podría poner la plataforma comercial en riesgo de robo.
Luna segura
SafeMoon V1 incluyó un error inadvertido que se encontró mediante verificación oficial después de su publicación. Era posible que el propietario renunciara a la propiedad del contrato y lo adquiriera nuevamente, si se realizaban ciertos procesos antes de renunciar a la propiedad.
El error pasa desapercibido durante la mayoría de las auditorías manuales de las bifurcaciones SafeMoon V1 porque encontrarlo requiere analizar conjuntos específicos de valores de variables del programa. Esto es algo que a los humanos les resulta fácil pasar por alto, pero que a las máquinas les resulta fácil encontrarlo.
Cómo funcionan juntas la verificación formal y la auditoría manual
La verificación formal proporciona una forma sistemática y automática de verificar la lógica y el comportamiento de un contrato con respecto a sus propiedades deseadas. Esto facilita la identificación y corrección de posibles errores o fallas. Es especialmente útil para encontrar problemas complejos y desapercibidos que pueden ser difíciles de detectar durante un análisis manual.
El proceso de auditoría manual implica la revisión por expertos del código y diseño del contrato, así como su publicación. El auditor utiliza su experiencia para identificar riesgos de seguridad y evaluar el estado de seguridad del contrato en general. También confirma que el proceso de verificación formal se ha completado correctamente y comprueba si hay problemas que las herramientas automatizadas no puedan detectar.
La combinación de verificación formal y auditoría manual proporciona una evaluación integral de la seguridad de los contratos inteligentes. Esto aumenta la probabilidad de encontrar y remediar cualquier vulnerabilidad. El resultado es un enfoque de seguridad profundo y defensivo que aprovecha las capacidades únicas de los humanos y las máquinas.
Pensamientos finales
Para garantizar la seguridad de los contratos inteligentes, es necesario utilizar tanto un proceso de verificación formal como una auditoría manual para garantizar una evaluación completa y precisa del estado de seguridad del contrato inteligente.
Aunque la verificación formal puede consumir muchos recursos, es una inversión que vale la pena para contratos inteligentes de alto valor o alto riesgo. Por último, es importante priorizar la seguridad y garantizar que los contratos inteligentes estén libres de errores, vulnerabilidades y otros comportamientos no deseados.
Artículos relacionados
¿Qué es un contrato inteligente?
¿Qué es una auditoría de seguridad para contratos inteligentes?
Descargo de responsabilidad y advertencia de riesgo: este contenido se le proporciona "tal cual" solo para información general y fines educativos, sin ninguna representación ni garantía de ningún tipo. No debe interpretarse como asesoramiento financiero ni pretende recomendar la compra de ningún producto o servicio en particular. Los precios de los activos digitales pueden ser volátiles. El valor de su inversión puede aumentar o disminuir y es posible que no recupere la cantidad que invirtió. Usted es el único responsable de sus decisiones de inversión y Binance Academy no es responsable de las pérdidas en las que pueda incurrir. Este no es un consejo financiero.