Este artículo es una publicació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 garantiza que los contratos inteligentes estén libres de errores, vulnerabilidades y otros comportamientos indeseables. En el proceso, un experto representa la lógica del contrato inteligente en una declaración matemática y luego la ejecuta a través de un proceso automatizado que compara la lógica real con un modelo 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.
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. Los contratos inteligentes pueden variar desde simples hasta muy complejos y pueden almacenar 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 perjudiciales, incluido el robo de todos los activos almacenados por el contrato inteligente. En 2021, se robaron 50 millones de dólares de los fondos del creador de mercado automatizado (AMM) Uranium Finance debido a un error en un contrato inteligente.
También en 2021, Compound Finance emitió 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 los contratos inteligentes.
Es importante programar los contratos inteligentes correctamente desde el principio. 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 explotarlo inmediatamente. Además, corregir las vulnerabilidades de seguridad con el tiempo no es una buena opción, ya que el código de contrato inteligente generalmente no se puede modificar una vez implementado.
¿Cómo funciona la verificación de contratos inteligentes?
La forma en que funciona la verificación formal de contratos inteligentes es presentando la lógica y el comportamiento deseado del contrato inteligente en forma de declaraciones matemáticas. Luego, los auditores utilizan herramientas automatizadas para garantizar que las declaraciones sean correctas.
El proceso incluye:
Define las especificaciones y características deseadas de un contrato en lenguaje formal.
Traducir el código del contrato a una representación formal, como un modelo matemático o lógico.
Utilice probadores de teoremas o verificadores de modelos automatizados para validar las especificaciones y características del contrato.
Repita el proceso de verificación para encontrar y corregir errores o desviaciones de las características deseadas.
Razones por las que la verificación de contratos inteligentes es importante
El uso del razonamiento matemático ayuda a garantizar que los contratos inteligentes que se han sometido a una verificación formal estén libres de errores, vulnerabilidades y otros comportamientos indeseables. Esto también ayuda a aumentar la confianza en el contrato, ya que se demuestra que sus características son ciertas.
A continuación se muestran algunos ejemplos que muestran que la verificación de contratos inteligentes ha ayudado a prevenir pérdidas financieras importantes y otros impactos perjudiciales.
Uniswap
Uniswap es una AMM muy conocida. Cuando se implementó, el contrato inteligente Uniswap V1 pasó por una verificación formal. Antes del lanzamiento, esta verificación formal descubrió y corrigió errores de redondeo que podrían haber provocado que se agotaran los fondos de Uniswap V1.
Balancín
Balancer V2 también es un AMM que ha pasado por una verificación formal. La verificación formal descubrió y corrigió cálculos de tarifas incorrectos relacionados con la funcionalidad de préstamos rápidos que podrían haber hecho que el intercambio fuera vulnerable al robo.
Luna Segura
SafeMoon V1 contenía un error sutil que se descubrió mediante verificación formal después de la implementación. El propietario puede renunciar a la propiedad del contrato y luego recuperarlo si se realizan ciertas operaciones antes de renunciar a la propiedad.
Este error no se detectó en la mayoría de las auditorías manuales de la bifurcación SafeMoon V1 porque requirió analizar ciertas combinaciones de valores de variables del programa para encontrarlo. Estos errores son fáciles de pasar por alto para los humanos y fáciles de rastrear para las máquinas.
Beneficios de combinar 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 deseadas. Esto facilita la identificación y corrección de posibles errores o fallas. Este proceso es especialmente útil para detectar problemas complejos y sutiles que pueden ser difíciles de detectar mediante una inspección manual.
En una auditoría manual, un experto revisa el código, el diseño y la implementación de un contrato. Los auditores utilizan su experiencia y conocimientos para identificar riesgos de seguridad y evaluar la postura general de seguridad del contrato. También pueden garantizar que el proceso de verificación formal se haya llevado a cabo correctamente y buscar problemas que las herramientas automatizadas no puedan detectar.
Al combinar la verificación formal y las auditorías manuales, obtiene una evaluación completa e integral de la seguridad de los contratos inteligentes. Esto aumenta las posibilidades de encontrar y corregir vulnerabilidades. El resultado es un enfoque de seguridad de defensa en profundidad que aprovecha las capacidades únicas de humanos y máquinas.
Clausura
Para garantizar la seguridad de los contratos inteligentes, es importante utilizar verificación formal y auditorías manuales para garantizar una evaluación integral y exhaustiva de la postura de seguridad de los contratos inteligentes.
Aunque requiere muchos recursos, vale la pena invertir en la verificación formal para contratos con factores de alto valor o alto riesgo. En última instancia, es importante priorizar la seguridad y garantizar que los contratos inteligentes estén libres de errores, vulnerabilidades y comportamientos indeseables.
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. Este contenido no debe considerarse asesoramiento financiero ni pretende sugerir 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. Es posible que no recupere el importe invertido. Usted es totalmente responsable de sus decisiones de inversión. Binance Academy no es responsable de las pérdidas que pueda experimentar. Este material no debe interpretarse como asesoramiento financiero.
