¿Qué es la Verificación formal de contratos inteligentes?
Introducción
A medida que el valor de los activos en la cadena de bloques crece rápidamente con varios proyectos que se turnan para lanzar diferentes casos de uso dentro de la economía criptográfica, estar al tanto de posibles lagunas y amenazas es más imperativo que nunca.
Bitcoin fue inventado para reemplazar a los bancos, pero la tecnología subyacente, blockchain, demostró que podía reemplazar a casi cualquier intermediario. En adelante, no se detuvo allí, viendo el enorme potencial que poseía el dinero digital, lo que el dinero en efectivo nunca podría hacer, y eso implica la capacidad de programar el dinero. De repente, los abogados y los contratos se podían sustituir en las transacciones financieras. Esta forma de moneda digital avanzó en la descentralización al permitir la ejecución automática de contratos con completa transparencia y sin intervención humana. Sin embargo, ¿cómo funcionan exactamente los contratos inteligentes? ¿Es realmente confiable confiar en estos sistemas que carecen de confianza?
En este artículo, exploraremos las extensas preguntas sobre la verificación formal de contratos inteligentes, discutiendo sus pros, contras, impacto en el ecosistema criptográfico y más con énfasis en Ethereum.
Breve historia de contratos inteligentes
Fuente:CryptoSlate
Nick Szabo, un científico de la computación y criptógrafo estadounidense a menudo especulado como Satoshi Nakamoto, fue el pionero de los contratos inteligentes, presentando por primera vez el concepto en 1994. Szabo describió los contratos inteligentes como protocolos de transacción digital diseñados para hacer cumplir automáticamente los términos de un acuerdo. Su objetivo era mejorar los métodos de transacción electrónica, como los sistemas de punto de venta, y expandir sus capacidades al mundo digital.
Szabo imaginó un futuro en el que los acuerdos pudieran funcionar como máquinas expendedoras, automatizadas, confiables e irrompibles. Aunque la tecnología de su época no era lo suficientemente avanzada como para realizar completamente su visión, las ideas de Szabo sentaron las bases de lo que más tarde revolucionaría la industria blockchain. Cuando Ethereum lanzadoen 2015, introdujo contratos inteligentes en uso práctico, convirtiendo los conceptos teóricos de Szabo en componentes esenciales de aplicaciones descentralizadas.
Su visión era la de contratos que pudieran manejar relaciones con términos precisos y automatizados, reduciendo la necesidad de intervención y supervisión humana. Este enfoque buscaba crear una forma más segura y eficiente de manejar acuerdos, allanando el camino para la evolución de los contratos inteligentes en herramientas poderosas dentro del ecosistema de blockchain. Las primeras ideas de Szabo continúan moldeando el panorama de las transacciones digitales y el desarrollo de contratos inteligentes hoy en día.
¿Qué es la Verificación Formal?
Origen: Medio
La verificación formal es el proceso de evaluar rigurosamente si un sistema, como un contrato inteligente, opera de acuerdo con un conjunto definido de reglas o especificaciones. En esencia, verifica si el sistema se comporta como se espera, asegurando que cumple con las condiciones requeridas y realiza las funciones previstas sin errores.
Para lograr esto, se esbozan los comportamientos esperados del sistema utilizando modelos formales, mientras que los lenguajes de especificación se utilizan para definir las propiedades exactas que el contrato debe cumplir y veremos más escenarios prácticos a medida que progrese el artículo. Las técnicas de verificación formal luego comparan la implementación del contrato con sus especificaciones, proporcionando una prueba matemática de su corrección. Cuando un contrato cumple con estas especificaciones, se considera "funcionalmente correcto" o "correcto por diseño", confirmando su confiabilidad y seguridad en el entorno blockchain.
Tipos de Especificaciones Formales para Contratos Inteligentes
Fuente: Ever Scale
Las especificaciones formales proporcionan una forma estructurada de utilizar el razonamiento matemático para verificar la precisión de la ejecución de un programa. Estas especificaciones pueden describir propiedades de alto nivel, que se centran en el comportamiento general, o detalles de bajo nivel de cómo opera un contrato internamente. Al definir estos comportamientos matemáticamente, las especificaciones formales garantizan que el contrato funcione como se pretende.
Especificaciones de alto nivel
Las especificaciones de alto nivel, también conocidas como especificaciones orientadas al modelo, describen el comportamiento general de un contrato inteligente, tratándolo como una máquina de estados finitos (FSM) que hace transiciones entre diferentes estados a través de operaciones específicas. A menudo se utiliza lógica temporal para definir las reglas formales que rigen estas transiciones, detallando cómo se mueve el contrato entre estados con el tiempo y las condiciones que debe cumplir para hacerlo correctamente.
Estas especificaciones capturan dos propiedades esenciales: seguridad y vivacidad. La seguridad garantiza que no ocurran eventos indeseables, como evitar que el saldo del remitente caiga por debajo de la cantidad necesaria para una transacción. La vivacidad, por el contrario, garantiza que el contrato continúe funcionando y progresando, como mantener la liquidez para que los usuarios puedan retirar fondos cuando lo soliciten. Ambas propiedades aseguran que los contratos inteligentes operen de manera segura y confiable, protegiendo las interacciones y activos de los usuarios.
Especificaciones de bajo nivel
Las especificaciones de bajo nivel, también conocidas como especificaciones orientadas a la propiedad, se centran en definir el comportamiento correcto de los contratos inteligentes mediante el análisis de sus procesos de ejecución internos. A diferencia de las especificaciones de alto nivel que modelan los contratos como máquinas de estado finito, las especificaciones de bajo nivel ven los contratos inteligentes como sistemas de funciones matemáticas y examinan las secuencias de ejecuciones de funciones, conocidas como trazas, que cambian el estado del contrato.
Técnicas para la Verificación Formal de Contratos Inteligentes
Origen: Ever Escala
Verificación de modelos
El model checking es un método de verificación formal que utiliza algoritmos para evaluar si el modelo de un contrato inteligente se alinea con sus especificaciones. Los contratos inteligentes suelen representarse como sistemas de transición de estados, y sus propiedades se definen utilizando temporal lógica. Este proceso implica crear un modelo matemático del contrato y expresar sus propiedades a través de fórmulas lógicas, permitiendo que el algoritmo verifique si el modelo cumple con estas especificaciones.
Demostración de teoremas
A diferencia de la verificación de modelos, la demostración de teoremas es un enfoque matemático utilizado para establecer la corrección de los programas, incluidos los contratos inteligentes. Este método implica convertir el modelo y las especificaciones de un contrato en fórmulas lógicas para verificar su equivalencia lógica, lo que significa que una afirmación es verdadera si la otra es verdadera. Al formular esta relación como un teorema, un demostrador automático de teoremas puede validar la corrección del modelo de contrato frente a sus especificaciones.
En marcado contraste con la comprobación de modelos, que está limitada a sistemas de estado finito, la demostración de teoremas puede analizar sistemas de estado infinito, pero a menudo requiere la orientación humana para naviGate problemas lógicos complejos. En consecuencia, la demostración de teoremas tiende a ser más intensiva en recursos que el proceso de comprobación de modelos completamente automatizado.
Ejecución simbólica
La ejecución simbólica es un método de análisis potente para contratos inteligentes que implica la ejecución de funciones con valores simbólicos en lugar de entradas específicas. Esta técnica de verificación formal permite razonar sobre propiedades a nivel de traza en el código de un contrato representando los caminos de ejecución como fórmulas matemáticas, conocidas como predicados de camino. Luego se emplea un solucionador SMT para determinar si estos predicados son satisfactorios, lo que significa que existe una entrada que cumple las condiciones.
Por ejemplo, si una función de contrato revierte cuando un valor está entre 5 y 10, la ejecución simbólica puede identificar eficientemente dichos valores desencadenantes evaluando la condición como X>5 ∧ X<10. Este método suele ser más efectivo que las pruebas tradicionales, produciendo menos falsos positivos y generando directamente valores concretos que replican cualquier error encontrado, por lo que es una herramienta valiosa para garantizar la confiabilidad de los contratos inteligentes.
¿Qué son los contratos inteligentes?
Origen:Tenderly
Los contratos inteligentes son programas informáticos automatizados que operan en una cadena de bloques, ejecutando acciones cuando se cumplen condiciones específicas. Pueden variar desde acuerdos sencillos hasta procesos altamente complejos y pueden gestionar activos valorados en millones o incluso miles de millones de dólares.
Si bien los contratos inteligentes tienen el potencial de revolucionar diversos sectores como la votación política, la gestión de la cadena de suministro, la atención médica y los bienes raíces, este artículo aún mantiene su enfoque en su impacto en el ámbito de las criptomonedas. Su diseño permite que múltiples partes colaboren sin riesgo de manipulación, ofreciendo un marco transparente y seguro que mejora la eficiencia y la innovación. Sin embargo, es importante reconocer que los contratos inteligentes también presentan vulnerabilidades y desafíos.
Vulnerabilidades con Contratos Inteligentes
Vulnerabilidades de seguridaden el código de contrato inteligente puede llevar a resultados catastróficos, como la pérdida total de los activos almacenados dentro del contrato, como lo demuestran los incidentes recientes.
- En 2021, el creador de mercado automático Uranium Finance sufrió un robo de $50 millonesdebido a un simple error tipográfico en su contrato inteligente.
- También en 2021, Compound Finance distribuyó inadvertidamente $80 millonesen recompensas no ganadas, nuevamente debido a un error de un solo carácter.
- Ocurrió una violación más significativa en 2022cuando se robaron $320 millones del Puente Wormholedebido a un error en uno de sus contratos inteligentes.
Dado estos ejemplos, es crucial asegurar que los contratos inteligentes estén codificados con precisión desde el principio. Una vez desplegados, los contratos inteligentes son de código abierto, lo que significa que su código es públicamente accesible, facilitando que los piratas informáticos exploten cualquier vulnerabilidad descubierta. Además, la naturaleza inmutable de los contratos inteligentes significa que una vez lanzados, su código generalmente no puede ser modificado para solucionar fallas de seguridad, dejándolos perpetuamente en riesgo si no se desarrollan con la máxima precisión.
¿Cómo funciona la verificación de contratos inteligentes?
Origen: Certik
El proceso incluye:
- Definir las especificaciones y propiedades deseadas del contrato utilizando un lenguaje formal de verificación.
- Traducir el código del contrato a una representación formal, como modelos matemáticos o expresiones lógicas.
- Los demostradores automáticos de teoremas o verificadores de modelos se emplean para confirmar la validez de las especificaciones y propiedades del contrato.
- Repetir de forma iterativa el proceso de verificación para identificar y corregir errores o desviaciones de las propiedades previstas.
Características clave de los contratos inteligentes
Fuente: Certik
Piense en los contratos inteligentes como acuerdos grabados en piedra, una vez creados no se pueden alterar. Operando en el libro mayor inmutable de una cadena de bloques, estos contratos hacen cumplir automáticamente los términos sin necesidad de intermediarios, lo que acelera las transacciones y reduce los costos. Esta naturaleza fija mejora la seguridad y descentraliza el control, reduciendo significativamente las posibilidades de fraude y corrupción.
Por qué es importante la verificación de contratos inteligentes
El razonamiento matemático juega un papel crucial en garantizar que los contratos inteligentes verificados formalmente estén libres de errores, vulnerabilidades y comportamientos inesperados. Este riguroso proceso aumenta la confianza en el contrato, ya que sus propiedades han sido validadas minuciosamente.
Los ejemplos exitosos de verificación formal de contratos inteligentes destacan su importancia en la prevención de pérdidas financieras significativas.
Uniswap
Por ejemplo, Uniswap, un conocido creador de mercado automatizado (AMM), se sometió a verificación formal durante el desarrollo de su contrato inteligente V1, que identificó y corrigió errores de redondeoque podría haber drenado fondos.
Balancer
Del mismo modo, Balancer V2, otro AMM, se benefició de la verificación formal que descubrió un cálculo incorrecto de la tarifarelacionado con préstamos rápidos, previniendo posibles robos.
SafeMoon
SafeMoon V1 tenía un error sutilidentificado a través de verificación formal después de la implementación. Este error permitía al propietario renunciar a la propiedad y recuperarla bajo ciertas condiciones, un detalle que la mayoría de las auditorías manuales pasaron por alto debido a su complejidad. La capacidad de verificación formal para analizar combinaciones específicas de valores de variables lo convierte en una herramienta eficaz para detectar problemas que los auditores humanos podrían pasar por alto.
Cómo la Verificación Formal y la Auditoría Manual trabajan juntas
La verificación formal ofrece un método sistemático y automatizado para verificar la lógica y el comportamiento de un contrato inteligente frente a sus propiedades previstas. Este enfoque simplifica la identificación y corrección de posibles errores o fallos, especialmente problemas complejos que las inspecciones manuales podrían pasar por alto.
Por otro lado, la auditoría manual implica una revisión exhaustiva del código, diseño e implementación del contrato por parte de un experto. El auditor utiliza su experiencia para identificar riesgos de seguridad y evaluar la postura general de seguridad del contrato. También puede validar la corrección del proceso de verificación formal e identificar problemas que las herramientas automatizadas podrían pasar por alto. Combinar la verificación formal con la auditoría manual crea una evaluación de seguridad integral, aumentando la probabilidad de descubrir y resolver vulnerabilidades, y estableciendo una estrategia de defensa sólida que aprovecha las fortalezas tanto de la experiencia humana como del análisis automatizado.
Pros y contras de contratos inteligentes
Fuente: Blockonomi
Los contratos inteligentes no son perfectos, pero sus ventajas superan significativamente los inconvenientes. Simplifican transacciones complejas, ahorran tiempo y dinero al mismo tiempo que promueven la transparencia y reducen los conflictos. Dado que operan mediante código, minimizan los errores humanos. Su seguridad es sólida, gracias a las protecciones criptográficas. Sin embargo, los contratos inteligentes pueden ser inflexibles y tener dificultades para adaptarse a situaciones inesperadas. Además, configurarlos requiere habilidades de codificación especializadas, lo que puede ser una barrera para algunos. A pesar de estos desafíos, los contratos inteligentes están transformando industrias.
Ventajas de los contratos inteligentes
- Mejore la eficiencia automatizando tareas, ahorrando tiempo y dinero.
- Aumentar la transparencia al dar acceso a todas las partes a la misma información, reduciendo las disputas.
- Reducir errores al depender del código, lo que elimina el error humano.
- Refuerce la seguridad con protecciones criptográficas, lo que dificulta la manipulación.
Desventajas de los contratos inteligentes
- Falta de flexibilidad para adaptarse a situaciones imprevistas debido a su naturaleza rígida.
- Requiere conocimientos especializados de codificación, limitando la adopción generalizada.
Herramientas de Verificación Formal para Contratos Inteligentes de Ethereum
Fuente: Calibraint
Lenguajes de especificación para crear especificaciones formales
- Act: Act permite a los usuarios definir actualizaciones de almacenamiento, pre y post-condiciones, e invariantes de contrato. Su conjunto de herramientas incluye backends de prueba que pueden validar varias propiedades utilizando Coq, solucionadores SMT o hevm.
- Scribble: Scribble convierte anotaciones de código escritas en su lenguaje de especificación en afirmaciones específicas que verifican las especificaciones.
- Dafny: Dafny es un lenguaje de programación diseñado para verificación, utilizando anotaciones de alto nivel para ayudar a razonar y confirmar la corrección del código.
Verificadores de programas para verificar la corrección
- Certora Prover: Certora Prover es una herramienta automatizada de verificación formal que verifica la corrección de los códigos de contratos inteligentes. Las especificaciones se crean utilizando el Lenguaje de Verificación Certora (CVL), y detecta violaciones de propiedades a través de una combinación de técnicas de análisis estático y resolución de restricciones.
- Solidity SMTChecker: El SMTChecker de Solidity es un verificador de modelos integrado que utiliza la Satisfacción Módulo Teorías (SMT) y resolución de Horn. Verifica si el código fuente de un contrato se alinea con las especificaciones durante la compilación y verifica violaciones de propiedades de seguridad.
- Solc-verify: Solc-verify es una versión mejorada del compilador de Solidity que permite la verificación formal automatizada del código de Solidity a través de anotaciones y verificación de programas modulares.
- KEVM: KEVM representa formalmente la Máquina Virtual Ethereum(EVM)creado usando el marco K. Es ejecutable y puede verificar reclamaciones específicas relacionadas con propiedades a través de la lógica de alcanzabilidad.
Marcos lógicos para la demostración de teoremas
- Isabelle: Isabelle/HOL es un asistente de pruebas que ayuda a los usuarios a expresar fórmulas matemáticas en un lenguaje formal y proporciona herramientas para demostrarlas. Su uso principal es formalizar pruebas matemáticas, especialmente para verificar la corrección del hardware y software de computadora y las propiedades de lenguajes de programación y protocolos.
- Coq - Coq es un demostrador interactivo de teoremas que te permite definir programas con teoremas y crear pruebas verificadas por máquina de su corrección a través de un proceso interactivo.
Herramientas basadas en la ejecución simbólica para detectar patrones vulnerables en contratos inteligentes
- Manticore - Una herramienta que analiza el bytecode de EVM utilizando ejecución simbólica.
- Hevm - hevm es un motor de ejecución simbólica que comprueba la equivalencia del código de bytes de EVM.
- Mythril - Una herramienta de ejecución simbólica utilizada para encontrar vulnerabilidades en contratos inteligentes de Ethereum.
Conclusión
Para salvaguardar los contratos inteligentes, es crucial combinar la verificación formal con la auditoría manual para una evaluación integral de su seguridad. Aunque la verificación formal puede ser costosa en recursos, es una inversión valiosa para los contratos que involucran altas apuestas o riesgos significativos. Los contratos inteligentes son más que un concepto de moda; están transformando las operaciones comerciales a nivel global y, si bien presentan desafíos, su capacidad incomparable para aumentar la eficiencia, minimizar errores y fortalecer la seguridad no puede ser ignorada. Los contratos inteligentes tienen un tremendo potencial para simplificar procesos y fomentar la confianza en las transacciones digitales. Con este fin, las organizaciones que adopten esta tecnología hoy estarán preparadas para prosperar en un futuro que prioriza la transparencia y la confiabilidad.
Compartir
Contenu
¿Qué es la Verificación formal?
Tipos de especificaciones formales para contratos inteligentes
Técnicas de Verificación Formal de Contratos Inteligentes
¿Qué son los contratos inteligentes?
¿Cómo funciona la verificación de contratos inteligentes?
Características clave de los contratos inteligentes
Por qué es importante la verificación de contratos inteligentes
Herramientas de Verificación Formal para Contratos Inteligentes Ethereum
Conclusión
Artículos relacionados
¿Qué es SegWit?
¿Cómo apostar ETH?
¿Qué es Tronscan y cómo se puede utilizar?
¿Qué es la Verificación formal de contratos inteligentes?
¿Qué es la Verificación formal?
Tipos de especificaciones formales para contratos inteligentes
Técnicas de Verificación Formal de Contratos Inteligentes
¿Qué son los contratos inteligentes?
¿Cómo funciona la verificación de contratos inteligentes?
Características clave de los contratos inteligentes
Por qué es importante la verificación de contratos inteligentes
Herramientas de Verificación Formal para Contratos Inteligentes Ethereum
Conclusión
Introducción
A medida que el valor de los activos en la cadena de bloques crece rápidamente con varios proyectos que se turnan para lanzar diferentes casos de uso dentro de la economía criptográfica, estar al tanto de posibles lagunas y amenazas es más imperativo que nunca.
Bitcoin fue inventado para reemplazar a los bancos, pero la tecnología subyacente, blockchain, demostró que podía reemplazar a casi cualquier intermediario. En adelante, no se detuvo allí, viendo el enorme potencial que poseía el dinero digital, lo que el dinero en efectivo nunca podría hacer, y eso implica la capacidad de programar el dinero. De repente, los abogados y los contratos se podían sustituir en las transacciones financieras. Esta forma de moneda digital avanzó en la descentralización al permitir la ejecución automática de contratos con completa transparencia y sin intervención humana. Sin embargo, ¿cómo funcionan exactamente los contratos inteligentes? ¿Es realmente confiable confiar en estos sistemas que carecen de confianza?
En este artículo, exploraremos las extensas preguntas sobre la verificación formal de contratos inteligentes, discutiendo sus pros, contras, impacto en el ecosistema criptográfico y más con énfasis en Ethereum.
Breve historia de contratos inteligentes
Fuente:CryptoSlate
Nick Szabo, un científico de la computación y criptógrafo estadounidense a menudo especulado como Satoshi Nakamoto, fue el pionero de los contratos inteligentes, presentando por primera vez el concepto en 1994. Szabo describió los contratos inteligentes como protocolos de transacción digital diseñados para hacer cumplir automáticamente los términos de un acuerdo. Su objetivo era mejorar los métodos de transacción electrónica, como los sistemas de punto de venta, y expandir sus capacidades al mundo digital.
Szabo imaginó un futuro en el que los acuerdos pudieran funcionar como máquinas expendedoras, automatizadas, confiables e irrompibles. Aunque la tecnología de su época no era lo suficientemente avanzada como para realizar completamente su visión, las ideas de Szabo sentaron las bases de lo que más tarde revolucionaría la industria blockchain. Cuando Ethereum lanzadoen 2015, introdujo contratos inteligentes en uso práctico, convirtiendo los conceptos teóricos de Szabo en componentes esenciales de aplicaciones descentralizadas.
Su visión era la de contratos que pudieran manejar relaciones con términos precisos y automatizados, reduciendo la necesidad de intervención y supervisión humana. Este enfoque buscaba crear una forma más segura y eficiente de manejar acuerdos, allanando el camino para la evolución de los contratos inteligentes en herramientas poderosas dentro del ecosistema de blockchain. Las primeras ideas de Szabo continúan moldeando el panorama de las transacciones digitales y el desarrollo de contratos inteligentes hoy en día.
¿Qué es la Verificación Formal?
Origen: Medio
La verificación formal es el proceso de evaluar rigurosamente si un sistema, como un contrato inteligente, opera de acuerdo con un conjunto definido de reglas o especificaciones. En esencia, verifica si el sistema se comporta como se espera, asegurando que cumple con las condiciones requeridas y realiza las funciones previstas sin errores.
Para lograr esto, se esbozan los comportamientos esperados del sistema utilizando modelos formales, mientras que los lenguajes de especificación se utilizan para definir las propiedades exactas que el contrato debe cumplir y veremos más escenarios prácticos a medida que progrese el artículo. Las técnicas de verificación formal luego comparan la implementación del contrato con sus especificaciones, proporcionando una prueba matemática de su corrección. Cuando un contrato cumple con estas especificaciones, se considera "funcionalmente correcto" o "correcto por diseño", confirmando su confiabilidad y seguridad en el entorno blockchain.
Tipos de Especificaciones Formales para Contratos Inteligentes
Fuente: Ever Scale
Las especificaciones formales proporcionan una forma estructurada de utilizar el razonamiento matemático para verificar la precisión de la ejecución de un programa. Estas especificaciones pueden describir propiedades de alto nivel, que se centran en el comportamiento general, o detalles de bajo nivel de cómo opera un contrato internamente. Al definir estos comportamientos matemáticamente, las especificaciones formales garantizan que el contrato funcione como se pretende.
Especificaciones de alto nivel
Las especificaciones de alto nivel, también conocidas como especificaciones orientadas al modelo, describen el comportamiento general de un contrato inteligente, tratándolo como una máquina de estados finitos (FSM) que hace transiciones entre diferentes estados a través de operaciones específicas. A menudo se utiliza lógica temporal para definir las reglas formales que rigen estas transiciones, detallando cómo se mueve el contrato entre estados con el tiempo y las condiciones que debe cumplir para hacerlo correctamente.
Estas especificaciones capturan dos propiedades esenciales: seguridad y vivacidad. La seguridad garantiza que no ocurran eventos indeseables, como evitar que el saldo del remitente caiga por debajo de la cantidad necesaria para una transacción. La vivacidad, por el contrario, garantiza que el contrato continúe funcionando y progresando, como mantener la liquidez para que los usuarios puedan retirar fondos cuando lo soliciten. Ambas propiedades aseguran que los contratos inteligentes operen de manera segura y confiable, protegiendo las interacciones y activos de los usuarios.
Especificaciones de bajo nivel
Las especificaciones de bajo nivel, también conocidas como especificaciones orientadas a la propiedad, se centran en definir el comportamiento correcto de los contratos inteligentes mediante el análisis de sus procesos de ejecución internos. A diferencia de las especificaciones de alto nivel que modelan los contratos como máquinas de estado finito, las especificaciones de bajo nivel ven los contratos inteligentes como sistemas de funciones matemáticas y examinan las secuencias de ejecuciones de funciones, conocidas como trazas, que cambian el estado del contrato.
Técnicas para la Verificación Formal de Contratos Inteligentes
Origen: Ever Escala
Verificación de modelos
El model checking es un método de verificación formal que utiliza algoritmos para evaluar si el modelo de un contrato inteligente se alinea con sus especificaciones. Los contratos inteligentes suelen representarse como sistemas de transición de estados, y sus propiedades se definen utilizando temporal lógica. Este proceso implica crear un modelo matemático del contrato y expresar sus propiedades a través de fórmulas lógicas, permitiendo que el algoritmo verifique si el modelo cumple con estas especificaciones.
Demostración de teoremas
A diferencia de la verificación de modelos, la demostración de teoremas es un enfoque matemático utilizado para establecer la corrección de los programas, incluidos los contratos inteligentes. Este método implica convertir el modelo y las especificaciones de un contrato en fórmulas lógicas para verificar su equivalencia lógica, lo que significa que una afirmación es verdadera si la otra es verdadera. Al formular esta relación como un teorema, un demostrador automático de teoremas puede validar la corrección del modelo de contrato frente a sus especificaciones.
En marcado contraste con la comprobación de modelos, que está limitada a sistemas de estado finito, la demostración de teoremas puede analizar sistemas de estado infinito, pero a menudo requiere la orientación humana para naviGate problemas lógicos complejos. En consecuencia, la demostración de teoremas tiende a ser más intensiva en recursos que el proceso de comprobación de modelos completamente automatizado.
Ejecución simbólica
La ejecución simbólica es un método de análisis potente para contratos inteligentes que implica la ejecución de funciones con valores simbólicos en lugar de entradas específicas. Esta técnica de verificación formal permite razonar sobre propiedades a nivel de traza en el código de un contrato representando los caminos de ejecución como fórmulas matemáticas, conocidas como predicados de camino. Luego se emplea un solucionador SMT para determinar si estos predicados son satisfactorios, lo que significa que existe una entrada que cumple las condiciones.
Por ejemplo, si una función de contrato revierte cuando un valor está entre 5 y 10, la ejecución simbólica puede identificar eficientemente dichos valores desencadenantes evaluando la condición como X>5 ∧ X<10. Este método suele ser más efectivo que las pruebas tradicionales, produciendo menos falsos positivos y generando directamente valores concretos que replican cualquier error encontrado, por lo que es una herramienta valiosa para garantizar la confiabilidad de los contratos inteligentes.
¿Qué son los contratos inteligentes?
Origen:Tenderly
Los contratos inteligentes son programas informáticos automatizados que operan en una cadena de bloques, ejecutando acciones cuando se cumplen condiciones específicas. Pueden variar desde acuerdos sencillos hasta procesos altamente complejos y pueden gestionar activos valorados en millones o incluso miles de millones de dólares.
Si bien los contratos inteligentes tienen el potencial de revolucionar diversos sectores como la votación política, la gestión de la cadena de suministro, la atención médica y los bienes raíces, este artículo aún mantiene su enfoque en su impacto en el ámbito de las criptomonedas. Su diseño permite que múltiples partes colaboren sin riesgo de manipulación, ofreciendo un marco transparente y seguro que mejora la eficiencia y la innovación. Sin embargo, es importante reconocer que los contratos inteligentes también presentan vulnerabilidades y desafíos.
Vulnerabilidades con Contratos Inteligentes
Vulnerabilidades de seguridaden el código de contrato inteligente puede llevar a resultados catastróficos, como la pérdida total de los activos almacenados dentro del contrato, como lo demuestran los incidentes recientes.
- En 2021, el creador de mercado automático Uranium Finance sufrió un robo de $50 millonesdebido a un simple error tipográfico en su contrato inteligente.
- También en 2021, Compound Finance distribuyó inadvertidamente $80 millonesen recompensas no ganadas, nuevamente debido a un error de un solo carácter.
- Ocurrió una violación más significativa en 2022cuando se robaron $320 millones del Puente Wormholedebido a un error en uno de sus contratos inteligentes.
Dado estos ejemplos, es crucial asegurar que los contratos inteligentes estén codificados con precisión desde el principio. Una vez desplegados, los contratos inteligentes son de código abierto, lo que significa que su código es públicamente accesible, facilitando que los piratas informáticos exploten cualquier vulnerabilidad descubierta. Además, la naturaleza inmutable de los contratos inteligentes significa que una vez lanzados, su código generalmente no puede ser modificado para solucionar fallas de seguridad, dejándolos perpetuamente en riesgo si no se desarrollan con la máxima precisión.
¿Cómo funciona la verificación de contratos inteligentes?
Origen: Certik
El proceso incluye:
- Definir las especificaciones y propiedades deseadas del contrato utilizando un lenguaje formal de verificación.
- Traducir el código del contrato a una representación formal, como modelos matemáticos o expresiones lógicas.
- Los demostradores automáticos de teoremas o verificadores de modelos se emplean para confirmar la validez de las especificaciones y propiedades del contrato.
- Repetir de forma iterativa el proceso de verificación para identificar y corregir errores o desviaciones de las propiedades previstas.
Características clave de los contratos inteligentes
Fuente: Certik
Piense en los contratos inteligentes como acuerdos grabados en piedra, una vez creados no se pueden alterar. Operando en el libro mayor inmutable de una cadena de bloques, estos contratos hacen cumplir automáticamente los términos sin necesidad de intermediarios, lo que acelera las transacciones y reduce los costos. Esta naturaleza fija mejora la seguridad y descentraliza el control, reduciendo significativamente las posibilidades de fraude y corrupción.
Por qué es importante la verificación de contratos inteligentes
El razonamiento matemático juega un papel crucial en garantizar que los contratos inteligentes verificados formalmente estén libres de errores, vulnerabilidades y comportamientos inesperados. Este riguroso proceso aumenta la confianza en el contrato, ya que sus propiedades han sido validadas minuciosamente.
Los ejemplos exitosos de verificación formal de contratos inteligentes destacan su importancia en la prevención de pérdidas financieras significativas.
Uniswap
Por ejemplo, Uniswap, un conocido creador de mercado automatizado (AMM), se sometió a verificación formal durante el desarrollo de su contrato inteligente V1, que identificó y corrigió errores de redondeoque podría haber drenado fondos.
Balancer
Del mismo modo, Balancer V2, otro AMM, se benefició de la verificación formal que descubrió un cálculo incorrecto de la tarifarelacionado con préstamos rápidos, previniendo posibles robos.
SafeMoon
SafeMoon V1 tenía un error sutilidentificado a través de verificación formal después de la implementación. Este error permitía al propietario renunciar a la propiedad y recuperarla bajo ciertas condiciones, un detalle que la mayoría de las auditorías manuales pasaron por alto debido a su complejidad. La capacidad de verificación formal para analizar combinaciones específicas de valores de variables lo convierte en una herramienta eficaz para detectar problemas que los auditores humanos podrían pasar por alto.
Cómo la Verificación Formal y la Auditoría Manual trabajan juntas
La verificación formal ofrece un método sistemático y automatizado para verificar la lógica y el comportamiento de un contrato inteligente frente a sus propiedades previstas. Este enfoque simplifica la identificación y corrección de posibles errores o fallos, especialmente problemas complejos que las inspecciones manuales podrían pasar por alto.
Por otro lado, la auditoría manual implica una revisión exhaustiva del código, diseño e implementación del contrato por parte de un experto. El auditor utiliza su experiencia para identificar riesgos de seguridad y evaluar la postura general de seguridad del contrato. También puede validar la corrección del proceso de verificación formal e identificar problemas que las herramientas automatizadas podrían pasar por alto. Combinar la verificación formal con la auditoría manual crea una evaluación de seguridad integral, aumentando la probabilidad de descubrir y resolver vulnerabilidades, y estableciendo una estrategia de defensa sólida que aprovecha las fortalezas tanto de la experiencia humana como del análisis automatizado.
Pros y contras de contratos inteligentes
Fuente: Blockonomi
Los contratos inteligentes no son perfectos, pero sus ventajas superan significativamente los inconvenientes. Simplifican transacciones complejas, ahorran tiempo y dinero al mismo tiempo que promueven la transparencia y reducen los conflictos. Dado que operan mediante código, minimizan los errores humanos. Su seguridad es sólida, gracias a las protecciones criptográficas. Sin embargo, los contratos inteligentes pueden ser inflexibles y tener dificultades para adaptarse a situaciones inesperadas. Además, configurarlos requiere habilidades de codificación especializadas, lo que puede ser una barrera para algunos. A pesar de estos desafíos, los contratos inteligentes están transformando industrias.
Ventajas de los contratos inteligentes
- Mejore la eficiencia automatizando tareas, ahorrando tiempo y dinero.
- Aumentar la transparencia al dar acceso a todas las partes a la misma información, reduciendo las disputas.
- Reducir errores al depender del código, lo que elimina el error humano.
- Refuerce la seguridad con protecciones criptográficas, lo que dificulta la manipulación.
Desventajas de los contratos inteligentes
- Falta de flexibilidad para adaptarse a situaciones imprevistas debido a su naturaleza rígida.
- Requiere conocimientos especializados de codificación, limitando la adopción generalizada.
Herramientas de Verificación Formal para Contratos Inteligentes de Ethereum
Fuente: Calibraint
Lenguajes de especificación para crear especificaciones formales
- Act: Act permite a los usuarios definir actualizaciones de almacenamiento, pre y post-condiciones, e invariantes de contrato. Su conjunto de herramientas incluye backends de prueba que pueden validar varias propiedades utilizando Coq, solucionadores SMT o hevm.
- Scribble: Scribble convierte anotaciones de código escritas en su lenguaje de especificación en afirmaciones específicas que verifican las especificaciones.
- Dafny: Dafny es un lenguaje de programación diseñado para verificación, utilizando anotaciones de alto nivel para ayudar a razonar y confirmar la corrección del código.
Verificadores de programas para verificar la corrección
- Certora Prover: Certora Prover es una herramienta automatizada de verificación formal que verifica la corrección de los códigos de contratos inteligentes. Las especificaciones se crean utilizando el Lenguaje de Verificación Certora (CVL), y detecta violaciones de propiedades a través de una combinación de técnicas de análisis estático y resolución de restricciones.
- Solidity SMTChecker: El SMTChecker de Solidity es un verificador de modelos integrado que utiliza la Satisfacción Módulo Teorías (SMT) y resolución de Horn. Verifica si el código fuente de un contrato se alinea con las especificaciones durante la compilación y verifica violaciones de propiedades de seguridad.
- Solc-verify: Solc-verify es una versión mejorada del compilador de Solidity que permite la verificación formal automatizada del código de Solidity a través de anotaciones y verificación de programas modulares.
- KEVM: KEVM representa formalmente la Máquina Virtual Ethereum(EVM)creado usando el marco K. Es ejecutable y puede verificar reclamaciones específicas relacionadas con propiedades a través de la lógica de alcanzabilidad.
Marcos lógicos para la demostración de teoremas
- Isabelle: Isabelle/HOL es un asistente de pruebas que ayuda a los usuarios a expresar fórmulas matemáticas en un lenguaje formal y proporciona herramientas para demostrarlas. Su uso principal es formalizar pruebas matemáticas, especialmente para verificar la corrección del hardware y software de computadora y las propiedades de lenguajes de programación y protocolos.
- Coq - Coq es un demostrador interactivo de teoremas que te permite definir programas con teoremas y crear pruebas verificadas por máquina de su corrección a través de un proceso interactivo.
Herramientas basadas en la ejecución simbólica para detectar patrones vulnerables en contratos inteligentes
- Manticore - Una herramienta que analiza el bytecode de EVM utilizando ejecución simbólica.
- Hevm - hevm es un motor de ejecución simbólica que comprueba la equivalencia del código de bytes de EVM.
- Mythril - Una herramienta de ejecución simbólica utilizada para encontrar vulnerabilidades en contratos inteligentes de Ethereum.
Conclusión
Para salvaguardar los contratos inteligentes, es crucial combinar la verificación formal con la auditoría manual para una evaluación integral de su seguridad. Aunque la verificación formal puede ser costosa en recursos, es una inversión valiosa para los contratos que involucran altas apuestas o riesgos significativos. Los contratos inteligentes son más que un concepto de moda; están transformando las operaciones comerciales a nivel global y, si bien presentan desafíos, su capacidad incomparable para aumentar la eficiencia, minimizar errores y fortalecer la seguridad no puede ser ignorada. Los contratos inteligentes tienen un tremendo potencial para simplificar procesos y fomentar la confianza en las transacciones digitales. Con este fin, las organizaciones que adopten esta tecnología hoy estarán preparadas para prosperar en un futuro que prioriza la transparencia y la confiabilidad.
Artículos relacionados
¿Qué es SegWit?
¿Cómo apostar ETH?