VERIFICACIÓN FORMAL DE CONTRATOS INTELIGENTES
Contratos inteligentesestán haciendo posible crear aplicaciones descentralizadas, sin confianza y robustas que introducen nuevos casos de uso y desbloquean valor para los usuarios. Debido a que los contratos inteligentes manejan grandes cantidades de valor, la seguridad es una consideración crítica para los desarrolladores.
La verificación formal es una de las técnicas recomendadas para mejorar seguridad de contratos inteligentesVerificación formal, que utilizamétodos formales
(se abre en una nueva pestaña)
para especificar, diseñar y verificar programas, se ha utilizado durante años para garantizar la corrección de sistemas críticos de hardware y software.
Cuando se implementa en contratos inteligentes, la verificación formal puede demostrar que la lógica empresarial de un contrato cumple con una especificación predefinida. En comparación con otros métodos para evaluar la corrección del código de contrato, como las pruebas, la verificación formal ofrece garantías más sólidas de que un contrato inteligente es correcto desde el punto de vista funcional.
¿QUÉ ES LA VERIFICACIÓN FORMAL?
La verificación formal se refiere al proceso de evaluar la corrección de un sistema con respecto a una especificación formal. En términos más simples, la verificación formal nos permite verificar si el comportamiento de un sistema satisface algunos requisitos (es decir, hace lo que queremos).
Los comportamientos esperados del sistema (un contrato inteligente en este caso) se describen utilizando modelado formal, mientras que los lenguajes de especificación permiten la creación de propiedades formales. Las técnicas de verificación formal pueden entonces verificar que la implementación de un contrato cumple con su especificación y derivar una prueba matemática de la corrección del primero. Cuando un contrato satisface su especificación, se describe como "correcto funcionalmente", "correcto por diseño" o "correcto por construcción".
¿Qué es un modelo formal?
En informática, modelo formal
(se abre en una pestaña nueva)
es una descripción matemática de un proceso computacional. Los programas se abstraen en funciones matemáticas (ecuaciones), con el modelo que describe cómo se calculan las salidas de las funciones dada una entrada.
Los modelos formales proporcionan un nivel de abstracción sobre el cual se puede evaluar el análisis del comportamiento de un programa. La existencia de modelos formales permite la creación de una especificación formal, que describe las propiedades deseadas del modelo en cuestión.
Se utilizan diferentes técnicas para modelar contratos inteligentes para verificación formal. Por ejemplo, algunos modelos se utilizan para razonar sobre el comportamiento de alto nivel de un contrato inteligente. Estas técnicas de modelado aplican una vista de caja negra a los contratos inteligentes, considerándolos como sistemas que aceptan entradas y ejecutan cálculos basados en esas entradas.
Los modelos de alto nivel se centran en la relación entre los contratos inteligentes y agentes externos, como cuentas de propiedad externa (EOAs), cuentas de contrato y el entorno de la cadena de bloques. Estos modelos son útiles para definir propiedades que especifican cómo un contrato debe comportarse en respuesta a ciertas interacciones del usuario.
Por el contrario, otros modelos formales se centran en el comportamiento de bajo nivel de un contrato inteligente. Si bien los modelos de alto nivel pueden ayudar a razonar sobre la funcionalidad de un contrato, pueden no capturar detalles sobre el funcionamiento interno de la implementación. Los modelos de bajo nivel aplican una vista de caja blanca al análisis de programas y se basan en representaciones de bajo nivel de las aplicaciones de contratos inteligentes, como trazas de programas y gráficos de flujo de control
(se abre en una pestaña nueva)
, para razonar sobre propiedades relevantes para la ejecución de un contrato.
Los modelos de bajo nivel se consideran ideales ya que representan la ejecución real de un contrato inteligente en el entorno de ejecución de Ethereum (es decir, el EVM). Las técnicas de modelado de bajo nivel son especialmente útiles para establecer propiedades críticas de seguridad en contratos inteligentes y detectar posibles vulnerabilidades.
¿Qué es una especificación formal?
Una especificación es simplemente un requisito técnico que un sistema particular debe cumplir. En programación, las especificaciones representan ideas generales sobre la ejecución de un programa (es decir, lo que el programa debería hacer).
En el contexto de los contratos inteligentes, las especificaciones formales se refieren a propiedades, descripciones formales de los requisitos que un contrato debe cumplir. Estas propiedades se describen como "invariantes" y representan afirmaciones lógicas sobre la ejecución de un contrato que deben seguir siendo verdaderas en todas las circunstancias posibles, sin excepciones.
Así, podemos pensar en una especificación formal como una colección de declaraciones escritas en un lenguaje formal que describen la ejecución prevista de un contrato inteligente. Las especificaciones cubren las propiedades de un contrato y definen cómo debería comportarse el contrato en diferentes circunstancias. El propósito de la verificación formal es determinar si un contrato inteligente posee estas propiedades (invariantes) y que estas propiedades no se violan durante la ejecución.
Las especificaciones formales son críticas en el desarrollo de implementaciones seguras de contratos inteligentes. Los contratos que no implementan invariantes o tienen sus propiedades violadas durante la ejecución son propensos a vulnerabilidades que pueden dañar la funcionalidad o causar exploits maliciosos.
TIPOS DE ESPECIFICACIONES FORMALES PARA CONTRATOS INTELIGENTES
Las especificaciones formales permiten el razonamiento matemático sobre la corrección de la ejecución del programa. Al igual que los modelos formales, las especificaciones formales pueden capturar propiedades de alto nivel o el comportamiento de bajo nivel de una implementación de contrato.
Las especificaciones formales se derivan utilizando elementos delógica del programa
, que permiten el razonamiento formal sobre las propiedades de un programa. La lógica de un programa tiene reglas formales que expresan (en lenguaje matemático) el comportamiento esperado de un programa. Se utilizan varias lógicas de programa en la creación de especificaciones formales, incluyendo lógica de alcanzabilidad
(se abre en una nueva pestaña)
(se abre en una nueva pestaña)
Las especificaciones formales para contratos inteligentes pueden clasificarse ampliamente como especificaciones de alto nivel o de bajo nivel. Independientemente de la categoría a la que pertenezca una especificación, debe describir adecuada y sin ambigüedades la propiedad del sistema bajo análisis.
Especificaciones de alto nivel
Como su nombre lo indica, una especificación de alto nivel (también llamada especificación orientada al modelo) describe el comportamiento de alto nivel de un programa. Las especificaciones de alto nivel modelan un contrato inteligente como un máquina de estados finitos
(se abre en una pestaña nueva)
(FSM), que puede transitar entre estados realizando operaciones, con lógica temporal utilizada para definir propiedades formales para el modelo de FSM.
(se abre en una nueva pestaña)
son "reglas para razonar sobre proposiciones calificadas en términos de tiempo (por ejemplo, "siempre tengo hambre" o "eventualmente tendré hambre")." Cuando se aplican a la verificación formal, las lógicas temporales se utilizan para afirmar sobre el comportamiento correcto de sistemas modelados como máquinas de estados. Específicamente, una lógica temporal describe los estados futuros en los que puede estar un contrato inteligente y cómo transita entre estados.
Las especificaciones de alto nivel generalmente capturan dos propiedades temporales críticas para los contratos inteligentes: seguridad y viabilidad. Las propiedades de seguridad representan la idea de que "nunca sucede nada malo" y suelen expresarse como invarianza. Una propiedad de seguridad puede definir requisitos generales de software, como la libertad de punto muerto
(se abre en una nueva pestaña)
, o expresar propiedades específicas de dominio para contratos (por ejemplo, invariantes en el control de acceso para funciones, valores admisibles de variables de estado o condiciones para transferencias de tokens).
Tomemos, por ejemplo, este requisito de seguridad que cubre las condiciones para usar transfer() o transferFrom() en contratos de tokens ERC-20: "El saldo del remitente nunca es menor que la cantidad solicitada de tokens a enviar". Esta descripción en lenguaje natural de una invariante de contrato puede traducirse a una especificación formal (matemática), la cual luego se puede verificar rigurosamente para validarla.
Las propiedades de vitalidad afirman que "eventualmente algo bueno sucede" y se refieren a la capacidad de un contrato para progresar a través de diferentes estados. Un ejemplo de una propiedad de vitalidad es "liquidez", que se refiere a la capacidad de un contrato para transferir sus saldos a los usuarios a pedido. Si esta propiedad se viola, los usuarios no podrían retirar los activos almacenados en el contrato, como sucedió con el Incidente de billetera de paridad
(se abre en una nueva pestaña)
.
Especificaciones de bajo nivel
Las especificaciones de alto nivel toman como punto de partida un modelo de estado finito de un contrato y definen las propiedades deseadas de este modelo. En contraste, las especificaciones de bajo nivel (también llamadas "especificaciones orientadas a propiedades") a menudo modelan programas (contratos inteligentes) como sistemas que comprenden una colección de funciones matemáticas y describen el comportamiento correcto de dichos sistemas.
En términos más simples, las especificaciones de nivel bajo analizan las trazas del programa e intentan definir las propiedades de un contrato inteligente a lo largo de estas trazas. Las trazas se refieren a secuencias de ejecuciones de funciones que alteran el estado de un contrato inteligente; por lo tanto, las especificaciones de nivel bajo ayudan a especificar los requisitos para la ejecución interna de un contrato.
Las especificaciones formales de bajo nivel se pueden dar como propiedades de estilo Hoare o invariantes en caminos de ejecución.
propiedades de estilo Hoare
(se abre en una nueva pestaña)
proporciona un conjunto de reglas formales para razonar sobre la corrección de programas, incluidos contratos inteligentes. Una propiedad de estilo Hoare está representada por un triple de Hoare {P}c{Q}, donde c es un programa y P y Q son predicados sobre el estado de c (es decir, el programa), descritos formalmente como precondiciones y postcondiciones, respectivamente.
Una precondición es un predicado que describe las condiciones necesarias para la correcta ejecución de una función; los usuarios que llaman al contrato deben cumplir con este requisito. Una postcondición es un predicado que describe la condición que una función establece si se ejecuta correctamente; los usuarios pueden esperar que esta condición sea verdadera después de llamar a la función. Un invariante en la lógica de Hoare es un predicado que se conserva mediante la ejecución de una función (es decir, no cambia).
Las especificaciones de estilo Hoare pueden garantizar tanto la corrección parcial como la corrección total. La implementación de una función de contrato es "parcialmente correcta" si la precondición es verdadera antes de que se ejecute la función, y si la ejecución termina, la postcondición también es verdadera. La prueba de corrección total se obtiene si una precondición es verdadera antes de que la función se ejecute, se garantiza que la ejecución terminará y cuando lo haga, la postcondición es verdadera.
Obtener una prueba de la total exactitud es difícil, ya que algunas ejecuciones pueden retrasarse antes de terminar, o nunca terminar. Dicho esto, la cuestión de si la ejecución termina es posiblemente un punto discutible, ya que el mecanismo de gas de Ethereum evita infinitos bucles de programa (la ejecución termina con éxito o finaliza debido a un error de "falta de gas").
Las especificaciones del contrato inteligente creadas utilizando la lógica de Hoare tendrán precondiciones, postcondiciones e invariables definidas para la ejecución de funciones y bucles en un contrato. Las precondiciones a menudo incluyen la posibilidad de entradas erróneas a una función, con postcondiciones que describen la respuesta esperada a tales entradas (por ejemplo, lanzar una excepción específica). De esta manera, las propiedades de estilo Hoare son efectivas para asegurar la corrección de las implementaciones de contrato.
Muchos marcos de verificación formal utilizan especificaciones de estilo Hoare para demostrar la corrección semántica de las funciones. También es posible agregar propiedades de estilo Hoare (como afirmaciones) directamente al código del contrato mediante el uso de las declaraciones require y assert en Solidity.
Las declaraciones require expresan una precondición o invariante y a menudo se utilizan para validar las entradas del usuario, mientras que assert captura una postcondición necesaria para la seguridad. Por ejemplo, el control adecuado de acceso para funciones (un ejemplo de una propiedad de seguridad) se puede lograr utilizando require como una verificación de precondición en la identidad de la cuenta que llama. De manera similar, un invariante en los valores permitidos de las variables de estado en un contrato (por ejemplo, el número total de tokens en circulación) se puede proteger de la violación utilizando assert para confirmar el estado del contrato después de la ejecución de la función.
Propiedades a nivel de trazas
Las especificaciones basadas en trazas describen operaciones que transicionan un contrato entre diferentes estados y las relaciones entre estas operaciones. Como se explicó anteriormente, las trazas son secuencias de operaciones que alteran el estado de un contrato de una manera particular.
Este enfoque se basa en el modelo de contratos inteligentes como sistemas de transición de estado con algunos estados predefinidos (descritos por variables de estado) junto con un conjunto de transiciones predefinidas (descritas por funciones de contrato). Además, un gráfico de flujo de control
(se abre en una nueva pestaña)
(CFG), que es una representación gráfica del flujo de ejecución de un programa, a menudo se utiliza para describir la semántica operativa de un contrato. Aquí, cada traza representada como un camino en el grafo de flujo de control.
Principalmente, las especificaciones a nivel de traza se utilizan para razonar sobre los patrones de ejecución interna en contratos inteligentes. Al crear especificaciones a nivel de traza, afirmamos los caminos de ejecución admisibles (es decir, transiciones de estado) para un contrato inteligente. Mediante técnicas como la ejecución simbólica, podemos verificar formalmente que la ejecución nunca sigue un camino no definido en el modelo formal.
Utilicemos un ejemplo de unDAOcontrato que tiene algunas funciones públicamente accesibles para describir propiedades de nivel de traza. Aquí, asumimos que el contrato DAO permite a los usuarios realizar las siguientes operaciones:
- Depositar fondos
- Votar en una propuesta después de depositar fondos
- Reclamar un reembolso si no votan sobre una propuesta
Ejemplos de propiedades a nivel de traza podrían ser "los usuarios que no depositan fondos no pueden votar en una propuesta" o "los usuarios que no votan en una propuesta siempre deben poder reclamar un reembolso". Ambas propiedades afirman secuencias de ejecución preferidas (la votación no puede ocurrir antes de depositar fondos y reclamar un reembolso no puede ocurrir después de votar en una propuesta).
TÉCNICAS PARA LA VERIFICACIÓN FORMAL DE CONTRATOS INTELIGENTES
Comprobación de modelos
El modelado con verificación es una técnica de verificación formal en la que un algoritmo verifica un modelo formal de un contrato inteligente contra su especificación. En la verificación de modelos, los contratos inteligentes a menudo se representan como sistemas de transición de estados, mientras que las propiedades de los estados de contrato permitidos se definen utilizando lógica temporal.
La verificación de modelos requiere crear una representación matemática abstracta de un sistema (es decir, un contrato) y expresar propiedades de este sistema utilizando fórmulas arraigadas en lógica proposicional
(se abre en una nueva pestaña)
. Esto simplifica la tarea del algoritmo de verificación del modelo, es decir, demostrar que un modelo matemático satisface una fórmula lógica dada.
La verificación de modelos en la verificación formal se utiliza principalmente para evaluar propiedades temporales que describen el comportamiento de un contrato a lo largo del tiempo. Las propiedades temporales para contratos inteligentes incluyen seguridad y viabilidad, que explicamos anteriormente.
Por ejemplo, una propiedad de seguridad relacionada con el control de acceso (por ejemplo, solo el propietario del contrato puede llamar a selfdestruct) se puede escribir en lógica formal. Posteriormente, el algoritmo de verificación de modelos puede verificar si el contrato satisface esta especificación formal.
El modelado de verificación utiliza la exploración del espacio de estados, que implica la construcción de todos los estados posibles de un contrato inteligente e intentar encontrar estados alcanzables que resulten en violaciones de propiedades. Sin embargo, esto puede llevar a un número infinito de estados (conocido como el “problema de la explosión de estados”), por lo tanto, los verificadores de modelos dependen de técnicas de abstracción para hacer posible un análisis eficiente de contratos inteligentes.
Demostración de teoremas
La demostración de teoremas es un método de razonamiento matemático sobre la corrección de programas, incluidos contratos inteligentes. Implica transformar el modelo del sistema de un contrato y sus especificaciones en fórmulas matemáticas (enunciados lógicos).
El objetivo de la demostración de teoremas es verificar la equivalencia lógica entre estas afirmaciones. “Equivalencia lógica” (también llamada “bicondicional lógico”) es un tipo de relación entre dos afirmaciones tal que la primera afirmación es verdadera si y solo si la segunda afirmación es verdadera.
La relación requerida (equivalencia lógica) entre las afirmaciones sobre el modelo de un contrato y su propiedad se formula como una declaración demostrable (llamada teorema). Utilizando un sistema formal de inferencia, el demostrador automatizado de teoremas puede verificar la validez del teorema. En otras palabras, un demostrador de teoremas puede probar de manera concluyente que el modelo de un contrato inteligente coincide precisamente con sus especificaciones.
Mientras que la verificación de modelos considera los contratos como sistemas de transición con estados finitos, la demostración de teoremas puede abordar el análisis de sistemas de estado infinito. Sin embargo, esto significa que un demostrador automático de teoremas no siempre puede saber si un problema lógico es "decidible" o no.
Como resultado, a menudo se requiere asistencia humana para guiar al demostrador de teoremas en la derivación de pruebas de corrección. El uso del esfuerzo humano en la demostración de teoremas lo hace más costoso de usar que la verificación de modelos, que es completamente automatizada.
Ejecución simbólica
La ejecución simbólica es un método de análisis de un contrato inteligente mediante la ejecución de funciones utilizando valores simbólicos (por ejemplo, x > 5) en lugar de valores concretos (por ejemplo, x == 5). Como técnica de verificación formal, la ejecución simbólica se utiliza para razonar formalmente sobre propiedades a nivel de trazas en el código de un contrato.
La ejecución simbólica representa una traza de ejecución como una fórmula matemática sobre valores de entrada simbólicos, también llamada predicado de ruta. AnSolucionador SMT
(se abre en una pestaña nueva)
se utiliza para comprobar si un predicado de ruta es "satisfacible" (es decir, existe un valor que puede satisfacer la fórmula). Si una ruta vulnerable es satisfacible, el solucionador SMT generará un valor concreto que activa la ejecución hacia esa ruta.
Supongamos que la función de un contrato inteligente toma como entrada un valor uint (x) y revierte cuando x es mayor que 5 y también menor que 10. Encontrar un valor para x que desencadene el error utilizando un procedimiento de prueba normal requeriría ejecutar docenas de casos de prueba (o más) sin la garantía de encontrar realmente una entrada que desencadene el error.
Por el contrario, una herramienta de ejecución simbólica ejecutaría la función con el valor simbólico: X > 5 ∧ X < 10 (es decir, x es mayor que 5 Y x es menor que 10). El predicado de ruta asociado x = X > 5 ∧ X < 10 se daría entonces a un solucionador SMT para resolverlo. Si un valor particular satisface la fórmula x = X > 5 ∧ X < 10, el solucionador SMT lo calculará, por ejemplo, el solucionador podría producir 7 como valor para x.
Dado que la ejecución simbólica depende de las entradas a un programa, y el conjunto de entradas para explorar todos los estados alcanzables es potencialmente infinito, sigue siendo una forma de prueba. Sin embargo, como se muestra en el ejemplo, la ejecución simbólica es más eficiente que las pruebas regulares para encontrar entradas que desencadenen violaciones de propiedades.
Además, la ejecución simbólica produce menos falsos positivos que otras técnicas basadas en propiedades (por ejemplo, fuzzing) que generan aleatoriamente entradas a una función. Si se desencadena un estado de error durante la ejecución simbólica, es posible generar un valor concreto que desencadene el error y reproducir el problema.
La ejecución simbólica también puede proporcionar cierto grado de prueba matemática de corrección. Considere el siguiente ejemplo de una función de contrato con protección contra desbordamiento:
Una traza de ejecución que resulta en un desbordamiento de enteros necesitaría satisfacer la fórmula: z = x + y AND (z >= x) AND (z=>y) AND (z < x OR z < y). Es poco probable que dicha fórmula se resuelva, por lo tanto, sirve como una prueba matemática de que la función safe_add nunca produce un desbordamiento.
¿Por qué usar la verificación formal para contratos inteligentes?
Necesidad de fiabilidad
La verificación formal se utiliza para evaluar la corrección de sistemas críticos de seguridad cuyo fallo puede tener consecuencias devastadoras, como la muerte, lesiones o ruina financiera. Los contratos inteligentes son aplicaciones de alto valor que controlan enormes cantidades de valor, y errores simples en el diseño pueden llevar apérdidas irreparables para los usuarios
(se abre en una nueva pestaña)
. Verificar formalmente un contrato antes de su implementación, sin embargo, puede aumentar las garantías de que funcionará como se espera una vez que se ejecute en la cadena de bloques.
La fiabilidad es una cualidad muy deseada en cualquier contrato inteligente, especialmente porque el código desplegado en la máquina virtual de Ethereum (EVM) suele ser inmutable. Dado que no se puede acceder fácilmente a las actualizaciones posteriores al lanzamiento, la necesidad de garantizar la fiabilidad de los contratos hace necesaria una verificación formal. La verificación formal es capaz de detectar problemas complicados, como desbordamientos y desbordamientos de enteros, reentrada y optimizaciones de gas deficientes, que pueden pasar desapercibidos para los auditores y evaluadores.
Demostrar corrección funcional
La prueba del programa es el método más común para demostrar que un contrato inteligente satisface algunos requisitos. Esto implica ejecutar un contrato con una muestra de los datos que se espera que maneje y analizar su comportamiento. Si el contrato devuelve los resultados esperados para los datos de muestra, entonces los desarrolladores tienen una prueba objetiva de su corrección.
Sin embargo, este enfoque no puede demostrar la ejecución correcta para los valores de entrada que no forman parte de la muestra. Por lo tanto, probar un contrato puede ayudar a detectar errores (es decir, si algunas rutas de código no devuelven los resultados deseados durante la ejecución), pero no puede demostrar de manera concluyente la ausencia de errores.
Por el contrario, la verificación formal puede demostrar formalmente que un contrato inteligente cumple con los requisitos para un rango infinito de ejecuciones sin ejecutar el contrato en absoluto. Esto requiere crear una especificación formal que describa con precisión los comportamientos correctos del contrato y desarrollar un modelo formal (matemático) del sistema del contrato. Luego podemos seguir un procedimiento de prueba formal para verificar la consistencia entre el modelo del contrato y su especificación.
Con la verificación formal, la cuestión de verificar si la lógica comercial de un contrato satisface los requisitos es una proposición matemática que puede ser demostrada o refutada. Al demostrar formalmente una proposición, podemos verificar un número infinito de casos de prueba con un número finito de pasos. De esta manera, la verificación formal tiene mejores perspectivas de demostrar que un contrato es funcionalmente correcto con respecto a una especificación.
Objetivos ideales de verificación
Un objetivo de verificación describe el sistema que se va a verificar formalmente. La verificación formal es mejor utilizada en sistemas integrados (pequeñas piezas de software simples que forman parte de un sistema más grande). También son ideales para dominios especializados que tienen pocas reglas, ya que esto facilita la modificación de herramientas para verificar propiedades específicas del dominio.
Los contratos inteligentes, al menos en cierta medida, cumplen con ambos requisitos. Por ejemplo, el tamaño pequeño de los contratos de Ethereum los hace susceptibles a verificación formal. De manera similar, la Máquina Virtual Ethereum sigue reglas simples, lo que facilita especificar y verificar propiedades semánticas para programas que se ejecutan en la EVM.
Ciclo de desarrollo más rápido
Las técnicas de verificación formal, como la comprobación de modelos y la ejecución simbólica, son generalmente más eficientes que el análisis regular del código de contrato inteligente (realizado durante pruebas o auditorías). Esto se debe a que la verificación formal se basa en valores simbólicos para probar afirmaciones ("¿qué pasa si un usuario intenta retirar n ether?") a diferencia de las pruebas que utilizan valores concretos ("¿qué pasa si un usuario intenta retirar 5 ether?").
Las variables de entrada simbólicas pueden abarcar múltiples clases de valores concretos, por lo que los enfoques de verificación formal prometen una mayor cobertura de código en un período de tiempo más corto. Cuando se utiliza de manera efectiva, la verificación formal puede acelerar el ciclo de desarrollo para los desarrolladores.
La verificación formal también mejora el proceso de construcción de aplicaciones descentralizadas (dapps) al reducir costosos errores de diseño. Actualizar contratos (cuando sea posible) para corregir vulnerabilidades requiere una reescritura extensa de las bases de código y más esfuerzo dedicado al desarrollo. La verificación formal puede detectar muchos errores en las implementaciones de contratos que pueden pasar desapercibidos por los probadores y auditores, y brinda amplias oportunidades para corregir esos problemas antes de implementar un contrato.
DESVENTAJAS DE LA VERIFICACIÓN FORMAL
Costo de mano de obra manual
La verificación formal, especialmente la verificación semi-automatizada en la que un ser humano guía al demostrador para derivar pruebas de corrección, requiere un trabajo manual considerable. Además, la creación de una especificación formal es una actividad compleja que exige un alto nivel de habilidad.
Estos factores (esfuerzo y habilidad) hacen que la verificación formal sea más exigente y costosa en comparación con los métodos habituales de evaluar la corrección en contratos, como pruebas y auditorías. Sin embargo, pagar el costo de una auditoría de verificación completa es práctico, dada la coste de los errores en las implementaciones de contratos inteligentes.
Falsos negativos
La verificación formal solo puede verificar si la ejecución del contrato inteligente coincide con la especificación formal. Como tal, es importante asegurarse de que la especificación describa adecuadamente los comportamientos esperados de un contrato inteligente.
Si las especificaciones están mal escritas, las violaciones de propiedades, que apuntan a ejecuciones vulnerables, no pueden ser detectadas por la auditoría de verificación formal. En este caso, un desarrollador podría asumir erróneamente que el contrato está libre de errores.
Problemas de rendimiento
La verificación formal se encuentra con una serie de problemas de rendimiento. Por ejemplo, los problemas de explosión de estado y de camino encontrados durante la verificación de modelos y la verificación simbólica, respectivamente, pueden afectar los procedimientos de verificación. Además, las herramientas de verificación formal a menudo utilizan solucionadores SMT y otros solucionadores de restricciones en su capa subyacente, y estos solucionadores se basan en procedimientos computacionalmente intensivos.
Además, no siempre es posible para los verificadores de programas determinar si una propiedad (descrita como una fórmula lógica) puede ser satisfecha o no (el Problema de decidibilidad
(se abre en una nueva pestaña)
") porque un programa podría no terminar nunca. Como tal, puede ser imposible probar algunas propiedades de un contrato incluso si está bien especificado.
HERRAMIENTAS DE VERIFICACIÓN FORMAL PARA CONTRATOS INTELIGENTES DE ETHEREUM
Lenguajes de especificación para crear especificaciones formales
Act: Act permite la especificación de actualizaciones de almacenamiento, condiciones previas/posteriores e invariantes de contrato. Su conjunto de herramientas también tiene motores de prueba capaces de demostrar muchas propiedades a través de Coq, solucionadores SMT o hevm.
Scribble: Scribble transforma anotaciones de código en el lenguaje de especificación de Scribble en afirmaciones concretas que verifican la especificación.
Dafny - Dafny es un lenguaje de programación listo para verificación que se basa en anotaciones de alto nivel para razonar y demostrar la corrección del código.
Verificadores de programas para verificar la corrección
Certora Prover - Certora Prover es una herramienta de verificación formal automática para verificar la corrección del código en contratos inteligentes. Las especificaciones se escriben en CVL (Certora Verification Language), y las violaciones de propiedades se detectan utilizando una combinación de análisis estático y resolución de restricciones.
Solidity SMTChecker - El SMTChecker de Solidity es un verificador de modelos incorporado basado en SMT (Satisfiability Modulo Theories) y resolución de Horn. Confirma si el código fuente de un contrato coincide con las especificaciones durante la compilación y verifica estáticamente las violaciones de propiedades de seguridad.
solc-verify - solc-verify es una versión extendida del compilador de Solidity que puede realizar verificación formal automatizada en código de Solidity utilizando anotaciones y verificación de programas modulares.
KEVM - KEVM es una semántica formal de la Máquina Virtual Ethereum (EVM) escrita en el marco K. KEVM es ejecutable y puede demostrar ciertas afirmaciones relacionadas con propiedades utilizando lógica de alcanzabilidad.
Marcos lógicos para la demostración de teoremas
Isabelle - Isabelle/HOL es un asistente de demostración que permite expresar fórmulas matemáticas en un lenguaje formal y proporciona herramientas para demostrar esas fórmulas. La principal aplicación es la formalización de demostraciones matemáticas y en particular la verificación formal, que incluye demostrar la corrección del hardware o software de computadora y probar propiedades de lenguajes de computadora y protocolos.
Coq - Coq es un demostrador interactivo de teoremas que te permite definir programas usando teoremas e generar interactivamente pruebas verificadas por máquina de corrección.
Herramientas basadas en la ejecución simbólica para detectar patrones vulnerables en contratos inteligentes
Mantícora: una herramienta para analizar el código de bytes de EVM basada en la ejecución simbólica.
hevm: hevm es un motor de ejecución simbólica y verificador de equivalencia para el bytecode de EVM.
Mythril - Una herramienta de ejecución simbólica para detectar vulnerabilidades en contratos inteligentes de Ethereum
Descargo de responsabilidad：
- Este artículo es reimpreso de [ ]. Todos los derechos de autor pertenecen al autor original [**]. If there are objections to this reprint, please contact the Gate Learnequipo, y lo manejarán prontamente.
- Descargo de responsabilidad: Las opiniones y puntos de vista expresados en este artículo son únicamente los del autor y no constituyen ningún consejo de inversión.
- Las traducciones del artículo a otros idiomas son realizadas por el equipo de Gate Learn. A menos que se mencione, está prohibido copiar, distribuir o plagiar los artículos traducidos.
Пригласить больше голосов
Статьи по теме
¿Qué es Ethereum envuelto (WETH)?
Guía sobre cómo cambiar de red en MetaMask
¿Qué es Neiro? Todo lo que necesitas saber sobre NEIROETH
VERIFICACIÓN FORMAL DE CONTRATOS INTELIGENTES
¿QUÉ ES LA VERIFICACIÓN FORMAL?
TIPOS DE ESPECIFICACIONES FORMALES PARA CONTRATOS INTELIGENTES
TECNICAS PARA LA VERIFICACION FORMAL DE CONTRATOS INTELIGENTES
DESVENTAJAS DE LA VERIFICACIÓN FORMAL
HERRAMIENTAS DE VERIFICACIÓN FORMAL PARA CONTRATOS INTELIGENTES DE ETHEREUM
Contratos inteligentesestán haciendo posible crear aplicaciones descentralizadas, sin confianza y robustas que introducen nuevos casos de uso y desbloquean valor para los usuarios. Debido a que los contratos inteligentes manejan grandes cantidades de valor, la seguridad es una consideración crítica para los desarrolladores.
La verificación formal es una de las técnicas recomendadas para mejorar seguridad de contratos inteligentesVerificación formal, que utilizamétodos formales
(se abre en una nueva pestaña)
para especificar, diseñar y verificar programas, se ha utilizado durante años para garantizar la corrección de sistemas críticos de hardware y software.
Cuando se implementa en contratos inteligentes, la verificación formal puede demostrar que la lógica empresarial de un contrato cumple con una especificación predefinida. En comparación con otros métodos para evaluar la corrección del código de contrato, como las pruebas, la verificación formal ofrece garantías más sólidas de que un contrato inteligente es correcto desde el punto de vista funcional.
¿QUÉ ES LA VERIFICACIÓN FORMAL?
La verificación formal se refiere al proceso de evaluar la corrección de un sistema con respecto a una especificación formal. En términos más simples, la verificación formal nos permite verificar si el comportamiento de un sistema satisface algunos requisitos (es decir, hace lo que queremos).
Los comportamientos esperados del sistema (un contrato inteligente en este caso) se describen utilizando modelado formal, mientras que los lenguajes de especificación permiten la creación de propiedades formales. Las técnicas de verificación formal pueden entonces verificar que la implementación de un contrato cumple con su especificación y derivar una prueba matemática de la corrección del primero. Cuando un contrato satisface su especificación, se describe como "correcto funcionalmente", "correcto por diseño" o "correcto por construcción".
¿Qué es un modelo formal?
En informática, modelo formal
(se abre en una pestaña nueva)
es una descripción matemática de un proceso computacional. Los programas se abstraen en funciones matemáticas (ecuaciones), con el modelo que describe cómo se calculan las salidas de las funciones dada una entrada.
Los modelos formales proporcionan un nivel de abstracción sobre el cual se puede evaluar el análisis del comportamiento de un programa. La existencia de modelos formales permite la creación de una especificación formal, que describe las propiedades deseadas del modelo en cuestión.
Se utilizan diferentes técnicas para modelar contratos inteligentes para verificación formal. Por ejemplo, algunos modelos se utilizan para razonar sobre el comportamiento de alto nivel de un contrato inteligente. Estas técnicas de modelado aplican una vista de caja negra a los contratos inteligentes, considerándolos como sistemas que aceptan entradas y ejecutan cálculos basados en esas entradas.
Los modelos de alto nivel se centran en la relación entre los contratos inteligentes y agentes externos, como cuentas de propiedad externa (EOAs), cuentas de contrato y el entorno de la cadena de bloques. Estos modelos son útiles para definir propiedades que especifican cómo un contrato debe comportarse en respuesta a ciertas interacciones del usuario.
Por el contrario, otros modelos formales se centran en el comportamiento de bajo nivel de un contrato inteligente. Si bien los modelos de alto nivel pueden ayudar a razonar sobre la funcionalidad de un contrato, pueden no capturar detalles sobre el funcionamiento interno de la implementación. Los modelos de bajo nivel aplican una vista de caja blanca al análisis de programas y se basan en representaciones de bajo nivel de las aplicaciones de contratos inteligentes, como trazas de programas y gráficos de flujo de control
(se abre en una pestaña nueva)
, para razonar sobre propiedades relevantes para la ejecución de un contrato.
Los modelos de bajo nivel se consideran ideales ya que representan la ejecución real de un contrato inteligente en el entorno de ejecución de Ethereum (es decir, el EVM). Las técnicas de modelado de bajo nivel son especialmente útiles para establecer propiedades críticas de seguridad en contratos inteligentes y detectar posibles vulnerabilidades.
¿Qué es una especificación formal?
Una especificación es simplemente un requisito técnico que un sistema particular debe cumplir. En programación, las especificaciones representan ideas generales sobre la ejecución de un programa (es decir, lo que el programa debería hacer).
En el contexto de los contratos inteligentes, las especificaciones formales se refieren a propiedades, descripciones formales de los requisitos que un contrato debe cumplir. Estas propiedades se describen como "invariantes" y representan afirmaciones lógicas sobre la ejecución de un contrato que deben seguir siendo verdaderas en todas las circunstancias posibles, sin excepciones.
Así, podemos pensar en una especificación formal como una colección de declaraciones escritas en un lenguaje formal que describen la ejecución prevista de un contrato inteligente. Las especificaciones cubren las propiedades de un contrato y definen cómo debería comportarse el contrato en diferentes circunstancias. El propósito de la verificación formal es determinar si un contrato inteligente posee estas propiedades (invariantes) y que estas propiedades no se violan durante la ejecución.
Las especificaciones formales son críticas en el desarrollo de implementaciones seguras de contratos inteligentes. Los contratos que no implementan invariantes o tienen sus propiedades violadas durante la ejecución son propensos a vulnerabilidades que pueden dañar la funcionalidad o causar exploits maliciosos.
TIPOS DE ESPECIFICACIONES FORMALES PARA CONTRATOS INTELIGENTES
Las especificaciones formales permiten el razonamiento matemático sobre la corrección de la ejecución del programa. Al igual que los modelos formales, las especificaciones formales pueden capturar propiedades de alto nivel o el comportamiento de bajo nivel de una implementación de contrato.
Las especificaciones formales se derivan utilizando elementos delógica del programa
, que permiten el razonamiento formal sobre las propiedades de un programa. La lógica de un programa tiene reglas formales que expresan (en lenguaje matemático) el comportamiento esperado de un programa. Se utilizan varias lógicas de programa en la creación de especificaciones formales, incluyendo lógica de alcanzabilidad
(se abre en una nueva pestaña)
(se abre en una nueva pestaña)
Las especificaciones formales para contratos inteligentes pueden clasificarse ampliamente como especificaciones de alto nivel o de bajo nivel. Independientemente de la categoría a la que pertenezca una especificación, debe describir adecuada y sin ambigüedades la propiedad del sistema bajo análisis.
Especificaciones de alto nivel
Como su nombre lo indica, una especificación de alto nivel (también llamada especificación orientada al modelo) describe el comportamiento de alto nivel de un programa. Las especificaciones de alto nivel modelan un contrato inteligente como un máquina de estados finitos
(se abre en una pestaña nueva)
(FSM), que puede transitar entre estados realizando operaciones, con lógica temporal utilizada para definir propiedades formales para el modelo de FSM.
(se abre en una nueva pestaña)
son "reglas para razonar sobre proposiciones calificadas en términos de tiempo (por ejemplo, "siempre tengo hambre" o "eventualmente tendré hambre")." Cuando se aplican a la verificación formal, las lógicas temporales se utilizan para afirmar sobre el comportamiento correcto de sistemas modelados como máquinas de estados. Específicamente, una lógica temporal describe los estados futuros en los que puede estar un contrato inteligente y cómo transita entre estados.
Las especificaciones de alto nivel generalmente capturan dos propiedades temporales críticas para los contratos inteligentes: seguridad y viabilidad. Las propiedades de seguridad representan la idea de que "nunca sucede nada malo" y suelen expresarse como invarianza. Una propiedad de seguridad puede definir requisitos generales de software, como la libertad de punto muerto
(se abre en una nueva pestaña)
, o expresar propiedades específicas de dominio para contratos (por ejemplo, invariantes en el control de acceso para funciones, valores admisibles de variables de estado o condiciones para transferencias de tokens).
Tomemos, por ejemplo, este requisito de seguridad que cubre las condiciones para usar transfer() o transferFrom() en contratos de tokens ERC-20: "El saldo del remitente nunca es menor que la cantidad solicitada de tokens a enviar". Esta descripción en lenguaje natural de una invariante de contrato puede traducirse a una especificación formal (matemática), la cual luego se puede verificar rigurosamente para validarla.
Las propiedades de vitalidad afirman que "eventualmente algo bueno sucede" y se refieren a la capacidad de un contrato para progresar a través de diferentes estados. Un ejemplo de una propiedad de vitalidad es "liquidez", que se refiere a la capacidad de un contrato para transferir sus saldos a los usuarios a pedido. Si esta propiedad se viola, los usuarios no podrían retirar los activos almacenados en el contrato, como sucedió con el Incidente de billetera de paridad
(se abre en una nueva pestaña)
.
Especificaciones de bajo nivel
Las especificaciones de alto nivel toman como punto de partida un modelo de estado finito de un contrato y definen las propiedades deseadas de este modelo. En contraste, las especificaciones de bajo nivel (también llamadas "especificaciones orientadas a propiedades") a menudo modelan programas (contratos inteligentes) como sistemas que comprenden una colección de funciones matemáticas y describen el comportamiento correcto de dichos sistemas.
En términos más simples, las especificaciones de nivel bajo analizan las trazas del programa e intentan definir las propiedades de un contrato inteligente a lo largo de estas trazas. Las trazas se refieren a secuencias de ejecuciones de funciones que alteran el estado de un contrato inteligente; por lo tanto, las especificaciones de nivel bajo ayudan a especificar los requisitos para la ejecución interna de un contrato.
Las especificaciones formales de bajo nivel se pueden dar como propiedades de estilo Hoare o invariantes en caminos de ejecución.
propiedades de estilo Hoare
(se abre en una nueva pestaña)
proporciona un conjunto de reglas formales para razonar sobre la corrección de programas, incluidos contratos inteligentes. Una propiedad de estilo Hoare está representada por un triple de Hoare {P}c{Q}, donde c es un programa y P y Q son predicados sobre el estado de c (es decir, el programa), descritos formalmente como precondiciones y postcondiciones, respectivamente.
Una precondición es un predicado que describe las condiciones necesarias para la correcta ejecución de una función; los usuarios que llaman al contrato deben cumplir con este requisito. Una postcondición es un predicado que describe la condición que una función establece si se ejecuta correctamente; los usuarios pueden esperar que esta condición sea verdadera después de llamar a la función. Un invariante en la lógica de Hoare es un predicado que se conserva mediante la ejecución de una función (es decir, no cambia).
Las especificaciones de estilo Hoare pueden garantizar tanto la corrección parcial como la corrección total. La implementación de una función de contrato es "parcialmente correcta" si la precondición es verdadera antes de que se ejecute la función, y si la ejecución termina, la postcondición también es verdadera. La prueba de corrección total se obtiene si una precondición es verdadera antes de que la función se ejecute, se garantiza que la ejecución terminará y cuando lo haga, la postcondición es verdadera.
Obtener una prueba de la total exactitud es difícil, ya que algunas ejecuciones pueden retrasarse antes de terminar, o nunca terminar. Dicho esto, la cuestión de si la ejecución termina es posiblemente un punto discutible, ya que el mecanismo de gas de Ethereum evita infinitos bucles de programa (la ejecución termina con éxito o finaliza debido a un error de "falta de gas").
Las especificaciones del contrato inteligente creadas utilizando la lógica de Hoare tendrán precondiciones, postcondiciones e invariables definidas para la ejecución de funciones y bucles en un contrato. Las precondiciones a menudo incluyen la posibilidad de entradas erróneas a una función, con postcondiciones que describen la respuesta esperada a tales entradas (por ejemplo, lanzar una excepción específica). De esta manera, las propiedades de estilo Hoare son efectivas para asegurar la corrección de las implementaciones de contrato.
Muchos marcos de verificación formal utilizan especificaciones de estilo Hoare para demostrar la corrección semántica de las funciones. También es posible agregar propiedades de estilo Hoare (como afirmaciones) directamente al código del contrato mediante el uso de las declaraciones require y assert en Solidity.
Las declaraciones require expresan una precondición o invariante y a menudo se utilizan para validar las entradas del usuario, mientras que assert captura una postcondición necesaria para la seguridad. Por ejemplo, el control adecuado de acceso para funciones (un ejemplo de una propiedad de seguridad) se puede lograr utilizando require como una verificación de precondición en la identidad de la cuenta que llama. De manera similar, un invariante en los valores permitidos de las variables de estado en un contrato (por ejemplo, el número total de tokens en circulación) se puede proteger de la violación utilizando assert para confirmar el estado del contrato después de la ejecución de la función.
Propiedades a nivel de trazas
Las especificaciones basadas en trazas describen operaciones que transicionan un contrato entre diferentes estados y las relaciones entre estas operaciones. Como se explicó anteriormente, las trazas son secuencias de operaciones que alteran el estado de un contrato de una manera particular.
Este enfoque se basa en el modelo de contratos inteligentes como sistemas de transición de estado con algunos estados predefinidos (descritos por variables de estado) junto con un conjunto de transiciones predefinidas (descritas por funciones de contrato). Además, un gráfico de flujo de control
(se abre en una nueva pestaña)
(CFG), que es una representación gráfica del flujo de ejecución de un programa, a menudo se utiliza para describir la semántica operativa de un contrato. Aquí, cada traza representada como un camino en el grafo de flujo de control.
Principalmente, las especificaciones a nivel de traza se utilizan para razonar sobre los patrones de ejecución interna en contratos inteligentes. Al crear especificaciones a nivel de traza, afirmamos los caminos de ejecución admisibles (es decir, transiciones de estado) para un contrato inteligente. Mediante técnicas como la ejecución simbólica, podemos verificar formalmente que la ejecución nunca sigue un camino no definido en el modelo formal.
Utilicemos un ejemplo de unDAOcontrato que tiene algunas funciones públicamente accesibles para describir propiedades de nivel de traza. Aquí, asumimos que el contrato DAO permite a los usuarios realizar las siguientes operaciones:
- Depositar fondos
- Votar en una propuesta después de depositar fondos
- Reclamar un reembolso si no votan sobre una propuesta
Ejemplos de propiedades a nivel de traza podrían ser "los usuarios que no depositan fondos no pueden votar en una propuesta" o "los usuarios que no votan en una propuesta siempre deben poder reclamar un reembolso". Ambas propiedades afirman secuencias de ejecución preferidas (la votación no puede ocurrir antes de depositar fondos y reclamar un reembolso no puede ocurrir después de votar en una propuesta).
TÉCNICAS PARA LA VERIFICACIÓN FORMAL DE CONTRATOS INTELIGENTES
Comprobación de modelos
El modelado con verificación es una técnica de verificación formal en la que un algoritmo verifica un modelo formal de un contrato inteligente contra su especificación. En la verificación de modelos, los contratos inteligentes a menudo se representan como sistemas de transición de estados, mientras que las propiedades de los estados de contrato permitidos se definen utilizando lógica temporal.
La verificación de modelos requiere crear una representación matemática abstracta de un sistema (es decir, un contrato) y expresar propiedades de este sistema utilizando fórmulas arraigadas en lógica proposicional
(se abre en una nueva pestaña)
. Esto simplifica la tarea del algoritmo de verificación del modelo, es decir, demostrar que un modelo matemático satisface una fórmula lógica dada.
La verificación de modelos en la verificación formal se utiliza principalmente para evaluar propiedades temporales que describen el comportamiento de un contrato a lo largo del tiempo. Las propiedades temporales para contratos inteligentes incluyen seguridad y viabilidad, que explicamos anteriormente.
Por ejemplo, una propiedad de seguridad relacionada con el control de acceso (por ejemplo, solo el propietario del contrato puede llamar a selfdestruct) se puede escribir en lógica formal. Posteriormente, el algoritmo de verificación de modelos puede verificar si el contrato satisface esta especificación formal.
El modelado de verificación utiliza la exploración del espacio de estados, que implica la construcción de todos los estados posibles de un contrato inteligente e intentar encontrar estados alcanzables que resulten en violaciones de propiedades. Sin embargo, esto puede llevar a un número infinito de estados (conocido como el “problema de la explosión de estados”), por lo tanto, los verificadores de modelos dependen de técnicas de abstracción para hacer posible un análisis eficiente de contratos inteligentes.
Demostración de teoremas
La demostración de teoremas es un método de razonamiento matemático sobre la corrección de programas, incluidos contratos inteligentes. Implica transformar el modelo del sistema de un contrato y sus especificaciones en fórmulas matemáticas (enunciados lógicos).
El objetivo de la demostración de teoremas es verificar la equivalencia lógica entre estas afirmaciones. “Equivalencia lógica” (también llamada “bicondicional lógico”) es un tipo de relación entre dos afirmaciones tal que la primera afirmación es verdadera si y solo si la segunda afirmación es verdadera.
La relación requerida (equivalencia lógica) entre las afirmaciones sobre el modelo de un contrato y su propiedad se formula como una declaración demostrable (llamada teorema). Utilizando un sistema formal de inferencia, el demostrador automatizado de teoremas puede verificar la validez del teorema. En otras palabras, un demostrador de teoremas puede probar de manera concluyente que el modelo de un contrato inteligente coincide precisamente con sus especificaciones.
Mientras que la verificación de modelos considera los contratos como sistemas de transición con estados finitos, la demostración de teoremas puede abordar el análisis de sistemas de estado infinito. Sin embargo, esto significa que un demostrador automático de teoremas no siempre puede saber si un problema lógico es "decidible" o no.
Como resultado, a menudo se requiere asistencia humana para guiar al demostrador de teoremas en la derivación de pruebas de corrección. El uso del esfuerzo humano en la demostración de teoremas lo hace más costoso de usar que la verificación de modelos, que es completamente automatizada.
Ejecución simbólica
La ejecución simbólica es un método de análisis de un contrato inteligente mediante la ejecución de funciones utilizando valores simbólicos (por ejemplo, x > 5) en lugar de valores concretos (por ejemplo, x == 5). Como técnica de verificación formal, la ejecución simbólica se utiliza para razonar formalmente sobre propiedades a nivel de trazas en el código de un contrato.
La ejecución simbólica representa una traza de ejecución como una fórmula matemática sobre valores de entrada simbólicos, también llamada predicado de ruta. AnSolucionador SMT
(se abre en una pestaña nueva)
se utiliza para comprobar si un predicado de ruta es "satisfacible" (es decir, existe un valor que puede satisfacer la fórmula). Si una ruta vulnerable es satisfacible, el solucionador SMT generará un valor concreto que activa la ejecución hacia esa ruta.
Supongamos que la función de un contrato inteligente toma como entrada un valor uint (x) y revierte cuando x es mayor que 5 y también menor que 10. Encontrar un valor para x que desencadene el error utilizando un procedimiento de prueba normal requeriría ejecutar docenas de casos de prueba (o más) sin la garantía de encontrar realmente una entrada que desencadene el error.
Por el contrario, una herramienta de ejecución simbólica ejecutaría la función con el valor simbólico: X > 5 ∧ X < 10 (es decir, x es mayor que 5 Y x es menor que 10). El predicado de ruta asociado x = X > 5 ∧ X < 10 se daría entonces a un solucionador SMT para resolverlo. Si un valor particular satisface la fórmula x = X > 5 ∧ X < 10, el solucionador SMT lo calculará, por ejemplo, el solucionador podría producir 7 como valor para x.
Dado que la ejecución simbólica depende de las entradas a un programa, y el conjunto de entradas para explorar todos los estados alcanzables es potencialmente infinito, sigue siendo una forma de prueba. Sin embargo, como se muestra en el ejemplo, la ejecución simbólica es más eficiente que las pruebas regulares para encontrar entradas que desencadenen violaciones de propiedades.
Además, la ejecución simbólica produce menos falsos positivos que otras técnicas basadas en propiedades (por ejemplo, fuzzing) que generan aleatoriamente entradas a una función. Si se desencadena un estado de error durante la ejecución simbólica, es posible generar un valor concreto que desencadene el error y reproducir el problema.
La ejecución simbólica también puede proporcionar cierto grado de prueba matemática de corrección. Considere el siguiente ejemplo de una función de contrato con protección contra desbordamiento:
Una traza de ejecución que resulta en un desbordamiento de enteros necesitaría satisfacer la fórmula: z = x + y AND (z >= x) AND (z=>y) AND (z < x OR z < y). Es poco probable que dicha fórmula se resuelva, por lo tanto, sirve como una prueba matemática de que la función safe_add nunca produce un desbordamiento.
¿Por qué usar la verificación formal para contratos inteligentes?
Necesidad de fiabilidad
La verificación formal se utiliza para evaluar la corrección de sistemas críticos de seguridad cuyo fallo puede tener consecuencias devastadoras, como la muerte, lesiones o ruina financiera. Los contratos inteligentes son aplicaciones de alto valor que controlan enormes cantidades de valor, y errores simples en el diseño pueden llevar apérdidas irreparables para los usuarios
(se abre en una nueva pestaña)
. Verificar formalmente un contrato antes de su implementación, sin embargo, puede aumentar las garantías de que funcionará como se espera una vez que se ejecute en la cadena de bloques.
La fiabilidad es una cualidad muy deseada en cualquier contrato inteligente, especialmente porque el código desplegado en la máquina virtual de Ethereum (EVM) suele ser inmutable. Dado que no se puede acceder fácilmente a las actualizaciones posteriores al lanzamiento, la necesidad de garantizar la fiabilidad de los contratos hace necesaria una verificación formal. La verificación formal es capaz de detectar problemas complicados, como desbordamientos y desbordamientos de enteros, reentrada y optimizaciones de gas deficientes, que pueden pasar desapercibidos para los auditores y evaluadores.
Demostrar corrección funcional
La prueba del programa es el método más común para demostrar que un contrato inteligente satisface algunos requisitos. Esto implica ejecutar un contrato con una muestra de los datos que se espera que maneje y analizar su comportamiento. Si el contrato devuelve los resultados esperados para los datos de muestra, entonces los desarrolladores tienen una prueba objetiva de su corrección.
Sin embargo, este enfoque no puede demostrar la ejecución correcta para los valores de entrada que no forman parte de la muestra. Por lo tanto, probar un contrato puede ayudar a detectar errores (es decir, si algunas rutas de código no devuelven los resultados deseados durante la ejecución), pero no puede demostrar de manera concluyente la ausencia de errores.
Por el contrario, la verificación formal puede demostrar formalmente que un contrato inteligente cumple con los requisitos para un rango infinito de ejecuciones sin ejecutar el contrato en absoluto. Esto requiere crear una especificación formal que describa con precisión los comportamientos correctos del contrato y desarrollar un modelo formal (matemático) del sistema del contrato. Luego podemos seguir un procedimiento de prueba formal para verificar la consistencia entre el modelo del contrato y su especificación.
Con la verificación formal, la cuestión de verificar si la lógica comercial de un contrato satisface los requisitos es una proposición matemática que puede ser demostrada o refutada. Al demostrar formalmente una proposición, podemos verificar un número infinito de casos de prueba con un número finito de pasos. De esta manera, la verificación formal tiene mejores perspectivas de demostrar que un contrato es funcionalmente correcto con respecto a una especificación.
Objetivos ideales de verificación
Un objetivo de verificación describe el sistema que se va a verificar formalmente. La verificación formal es mejor utilizada en sistemas integrados (pequeñas piezas de software simples que forman parte de un sistema más grande). También son ideales para dominios especializados que tienen pocas reglas, ya que esto facilita la modificación de herramientas para verificar propiedades específicas del dominio.
Los contratos inteligentes, al menos en cierta medida, cumplen con ambos requisitos. Por ejemplo, el tamaño pequeño de los contratos de Ethereum los hace susceptibles a verificación formal. De manera similar, la Máquina Virtual Ethereum sigue reglas simples, lo que facilita especificar y verificar propiedades semánticas para programas que se ejecutan en la EVM.
Ciclo de desarrollo más rápido
Las técnicas de verificación formal, como la comprobación de modelos y la ejecución simbólica, son generalmente más eficientes que el análisis regular del código de contrato inteligente (realizado durante pruebas o auditorías). Esto se debe a que la verificación formal se basa en valores simbólicos para probar afirmaciones ("¿qué pasa si un usuario intenta retirar n ether?") a diferencia de las pruebas que utilizan valores concretos ("¿qué pasa si un usuario intenta retirar 5 ether?").
Las variables de entrada simbólicas pueden abarcar múltiples clases de valores concretos, por lo que los enfoques de verificación formal prometen una mayor cobertura de código en un período de tiempo más corto. Cuando se utiliza de manera efectiva, la verificación formal puede acelerar el ciclo de desarrollo para los desarrolladores.
La verificación formal también mejora el proceso de construcción de aplicaciones descentralizadas (dapps) al reducir costosos errores de diseño. Actualizar contratos (cuando sea posible) para corregir vulnerabilidades requiere una reescritura extensa de las bases de código y más esfuerzo dedicado al desarrollo. La verificación formal puede detectar muchos errores en las implementaciones de contratos que pueden pasar desapercibidos por los probadores y auditores, y brinda amplias oportunidades para corregir esos problemas antes de implementar un contrato.
DESVENTAJAS DE LA VERIFICACIÓN FORMAL
Costo de mano de obra manual
La verificación formal, especialmente la verificación semi-automatizada en la que un ser humano guía al demostrador para derivar pruebas de corrección, requiere un trabajo manual considerable. Además, la creación de una especificación formal es una actividad compleja que exige un alto nivel de habilidad.
Estos factores (esfuerzo y habilidad) hacen que la verificación formal sea más exigente y costosa en comparación con los métodos habituales de evaluar la corrección en contratos, como pruebas y auditorías. Sin embargo, pagar el costo de una auditoría de verificación completa es práctico, dada la coste de los errores en las implementaciones de contratos inteligentes.
Falsos negativos
La verificación formal solo puede verificar si la ejecución del contrato inteligente coincide con la especificación formal. Como tal, es importante asegurarse de que la especificación describa adecuadamente los comportamientos esperados de un contrato inteligente.
Si las especificaciones están mal escritas, las violaciones de propiedades, que apuntan a ejecuciones vulnerables, no pueden ser detectadas por la auditoría de verificación formal. En este caso, un desarrollador podría asumir erróneamente que el contrato está libre de errores.
Problemas de rendimiento
La verificación formal se encuentra con una serie de problemas de rendimiento. Por ejemplo, los problemas de explosión de estado y de camino encontrados durante la verificación de modelos y la verificación simbólica, respectivamente, pueden afectar los procedimientos de verificación. Además, las herramientas de verificación formal a menudo utilizan solucionadores SMT y otros solucionadores de restricciones en su capa subyacente, y estos solucionadores se basan en procedimientos computacionalmente intensivos.
Además, no siempre es posible para los verificadores de programas determinar si una propiedad (descrita como una fórmula lógica) puede ser satisfecha o no (el Problema de decidibilidad
(se abre en una nueva pestaña)
") porque un programa podría no terminar nunca. Como tal, puede ser imposible probar algunas propiedades de un contrato incluso si está bien especificado.
HERRAMIENTAS DE VERIFICACIÓN FORMAL PARA CONTRATOS INTELIGENTES DE ETHEREUM
Lenguajes de especificación para crear especificaciones formales
Act: Act permite la especificación de actualizaciones de almacenamiento, condiciones previas/posteriores e invariantes de contrato. Su conjunto de herramientas también tiene motores de prueba capaces de demostrar muchas propiedades a través de Coq, solucionadores SMT o hevm.
Scribble: Scribble transforma anotaciones de código en el lenguaje de especificación de Scribble en afirmaciones concretas que verifican la especificación.
Dafny - Dafny es un lenguaje de programación listo para verificación que se basa en anotaciones de alto nivel para razonar y demostrar la corrección del código.
Verificadores de programas para verificar la corrección
Certora Prover - Certora Prover es una herramienta de verificación formal automática para verificar la corrección del código en contratos inteligentes. Las especificaciones se escriben en CVL (Certora Verification Language), y las violaciones de propiedades se detectan utilizando una combinación de análisis estático y resolución de restricciones.
Solidity SMTChecker - El SMTChecker de Solidity es un verificador de modelos incorporado basado en SMT (Satisfiability Modulo Theories) y resolución de Horn. Confirma si el código fuente de un contrato coincide con las especificaciones durante la compilación y verifica estáticamente las violaciones de propiedades de seguridad.
solc-verify - solc-verify es una versión extendida del compilador de Solidity que puede realizar verificación formal automatizada en código de Solidity utilizando anotaciones y verificación de programas modulares.
KEVM - KEVM es una semántica formal de la Máquina Virtual Ethereum (EVM) escrita en el marco K. KEVM es ejecutable y puede demostrar ciertas afirmaciones relacionadas con propiedades utilizando lógica de alcanzabilidad.
Marcos lógicos para la demostración de teoremas
Isabelle - Isabelle/HOL es un asistente de demostración que permite expresar fórmulas matemáticas en un lenguaje formal y proporciona herramientas para demostrar esas fórmulas. La principal aplicación es la formalización de demostraciones matemáticas y en particular la verificación formal, que incluye demostrar la corrección del hardware o software de computadora y probar propiedades de lenguajes de computadora y protocolos.
Coq - Coq es un demostrador interactivo de teoremas que te permite definir programas usando teoremas e generar interactivamente pruebas verificadas por máquina de corrección.
Herramientas basadas en la ejecución simbólica para detectar patrones vulnerables en contratos inteligentes
Mantícora: una herramienta para analizar el código de bytes de EVM basada en la ejecución simbólica.
hevm: hevm es un motor de ejecución simbólica y verificador de equivalencia para el bytecode de EVM.
Mythril - Una herramienta de ejecución simbólica para detectar vulnerabilidades en contratos inteligentes de Ethereum
Descargo de responsabilidad：
- Este artículo es reimpreso de [ ]. Todos los derechos de autor pertenecen al autor original [**]. If there are objections to this reprint, please contact the Gate Learnequipo, y lo manejarán prontamente.
- Descargo de responsabilidad: Las opiniones y puntos de vista expresados en este artículo son únicamente los del autor y no constituyen ningún consejo de inversión.
- Las traducciones del artículo a otros idiomas son realizadas por el equipo de Gate Learn. A menos que se mencione, está prohibido copiar, distribuir o plagiar los artículos traducidos.
Статьи по теме
¿Qué es Ethereum envuelto (WETH)?
Guía sobre cómo cambiar de red en MetaMask