Este artículo es un envío de la comunidad. El autor es David Tarditi, vicepresidente de ingeniería de CertiK, una empresa de auditoría de contratos inteligentes Web3.
Las opiniones de este artículo pertenecen al colaborador/autor y no reflejan necesariamente las de Binance Academy.
TL;DR
Formal verification of smart contracts ensures they are free from bugs, vulnerabilities, and other unintended behavior. It involves a human expert presenting the smart contract's logic as mathematical statements, then running them through an automated process that checks the actual logic against models of the contract’s expected behavior. The combination of formal verification and manual auditing provides a comprehensive evaluation of a smart contract's security.
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. Pueden variar desde simples hasta 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 contrato inteligente pueden tener consecuencias devastadoras, incluido el robo de todos los activos contenidos en un contrato inteligente. En 2021, al creador de mercado automatizado (AMM) Uranium Finance le robaron 50 millones de dólares debido a un solo error tipográfico en un contrato inteligente.
También en 2021, Compound Finance entregó 80 millones de dólares en recompensas no ganadas debido a un error de un solo carácter. En 2022, se robaron 320 millones de dólares del puente Wormhole debido a un error en uno de sus contratos inteligentes.
Es importante acertar con el programa de contrato inteligente la primera vez. Los contratos inteligentes son de código abierto, lo que significa que el código está disponible públicamente una vez que se implementa el contrato. Si un hacker encuentra un error, puede aprovecharlo inmediatamente. Además, parchear las vulnerabilidades de seguridad a lo largo del tiempo no es una opción, ya que el código de un contrato inteligente normalmente no se puede modificar después de su implementación.
¿Cómo funciona la verificación de contratos inteligentes?
La verificación formal de los contratos inteligentes funciona presentando la lógica y el comportamiento deseado de los contratos inteligentes como declaraciones matemáticas. Luego, los auditores utilizan herramientas automatizadas para comprobar si estas declaraciones son correctas.
El proceso implica:
Definir las especificaciones y propiedades deseadas de un contrato en lenguaje formal.
Traducir el código del contrato a una representación formal, como modelos matemáticos o lógica.
Usar probadores de teoremas 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 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 se ha demostrado rigurosamente que sus propiedades son correctas.
A continuación se muestran algunos ejemplos de cómo la verificación de contratos inteligentes ha ayudado a prevenir pérdidas financieras significativas y otros resultados desastrosos.
Uniswap
Uniswap es una AMM muy conocida. Cuando se desarrolló el contrato inteligente Uniswap V1, se verificó formalmente. Antes de su lanzamiento, esta verificación formal encontró y solucionó errores de redondeo que podrían haber llevado a que Uniswap V1 se quedara sin fondos.
Balancín
Balancer V2 también es un AMM que fue verificado formalmente. La verificación formal encontró y solucionó un cálculo de tarifa incorrecto que involucraba la funcionalidad de préstamo rápido en el contrato inteligente, lo que podría haber hecho que el intercambio fuera vulnerable al robo.
Luna Segura
SafeMoon V1 contenía un error sutil encontrado mediante verificación formal después de su implementación. Era posible que un propietario renunciara a la propiedad del contrato y luego lo readquiriera, si ciertas operaciones se realizaban antes de renunciar a la propiedad.
Este error no se detectó en la mayoría de las auditorías manuales de las bifurcaciones de SafeMoon V1 porque encontrarlo requirió analizar combinaciones específicas de valores de variables del programa. Esto es algo que es fácil de pasar por alto para los humanos y fácil de captar para una máquina.
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 propiedades deseadas. Esto facilita la identificación y corrección de posibles errores o fallas. Es especialmente útil para encontrar problemas complejos y sutiles que pueden ser difíciles de detectar mediante una inspección manual.
La auditoría manual implica la revisión experta del código, el diseño y la implementación de un contrato. El auditor utiliza su experiencia y conocimientos para identificar riesgos de seguridad y evaluar la postura general de seguridad del contrato. También pueden confirmar que el proceso de verificación formal se realizó correctamente y verificar si hay problemas que no puedan ser detectados por herramientas automatizadas.
La combinación de verificación formal y auditoría manual proporciona una evaluación integral y exhaustiva de la seguridad de un contrato inteligente. Esto aumenta las posibilidades de encontrar y corregir cualquier vulnerabilidad. El resultado es un enfoque de seguridad de defensa en profundidad que aprovecha las capacidades únicas tanto de los humanos como de las máquinas.
Pensamientos finales
Para garantizar la seguridad de los contratos inteligentes, es esencial utilizar tanto la verificación formal como la auditoría manual para garantizar una evaluación integral y exhaustiva de la postura de seguridad de un contrato inteligente.
Si bien la verificación formal puede requerir muchos recursos, es una inversión que vale la pena para contratos con alto valor o factores de alto riesgo. En última instancia, es vital priorizar la seguridad y garantizar que los contratos inteligentes estén libres de errores, vulnerabilidades y comportamientos no deseados.
Otras lecturas
¿Qué son los contratos inteligentes?
¿Qué es una auditoría de seguridad de contrato inteligente?
Descargo de responsabilidad y advertencia de riesgo: este contenido se le presenta "tal cual" para información general y fines educativos únicamente, sin representación ni garantía de ningún tipo. No debe interpretarse como asesoramiento financiero, legal o de otro tipo, ni pretende recomendar la compra de ningún producto o servicio específico. Debe buscar su propio consejo de asesores profesionales adecuados. Cuando el artículo sea aportado por un tercero, tenga en cuenta que las opiniones expresadas pertenecen al tercero y no reflejan necesariamente las de Binance Academy. Lea nuestro descargo de responsabilidad completo aquí para obtener más detalles. Los precios de los activos digitales pueden ser volátiles. El valor de su inversión puede subir o bajar y es posible que no recupere el monto invertido. 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 material no debe interpretarse como asesoramiento financiero, legal o de otro tipo. Para obtener más información, consulte nuestros Términos de uso y Advertencia de riesgos.
