Los contratos inteligentes son códigos que se ejecutan automáticamente y constituyen la columna vertebral del ecosistema Web3. Los contratos inteligentes actúan como los pilares fundamentales del ecosistema Web3, equilibrando con precisión miles de millones en una red abierta. Hoy hablaremos de las herramientas y técnicas de prueba más utilizadas en el desarrollo de contratos inteligentes, como Truffle, Hardhat, Foundry, la verificación formal, el fuzzing y las pruebas unitarias. Este es un buen punto de partida si quieres aprender sobre Solidity y cómo auditar contratos inteligentes. Este artículo forma parte de una serie dedicada a la auditoría de contratos inteligentes en Solidity. La serie abordará las vulnerabilidades y los recursos que utilizan los auditores de contratos inteligentes.

Pruebas

Las pruebas de solidez consisten en evaluar y validar de forma sistemática el rendimiento, la seguridad y la funcionalidad de los contratos inteligentes.

Para crear casos de prueba exhaustivos, es necesario identificar posibles entradas, salidas e interacciones con el contrato en diversas condiciones, con el fin de abarcar diferentes escenarios y casos extremos. Los casos de prueba deben incluir tanto casos de uso habituales como escenarios excepcionales, a fin de verificar el comportamiento del contrato en todas las situaciones.

Herramientas de pruebas

Hay tres marcos de pruebas muy utilizados en el ecosistema de Ethereum: Truffle, Hardhat y Foundry.

‍

Técnicas de evaluación

1. Verificación formal

La verificación formal es un enfoque matemático que se utiliza para confirmar la corrección de un sistema, como un programa informático, un dispositivo físico o un contrato inteligente. Consiste en crear un modelo formal que defina con precisión el comportamiento esperado del sistema y, a continuación, utilizar técnicas matemáticas para verificar si la implementación real se ajusta a dicha especificación. 

El proceso de verificación formal comprende:

• Definición de especificaciones: Las propiedades deseadas de un contrato se definen mediante un lenguaje formal, es decir, mediante enunciados claros y precisos.
• Traducción a una representación formal: El código del contrato se transforma a un formato formal, que suele representarse mediante modelos matemáticos o lógicos.
• Validación automatizada: Se utilizan herramientas automatizadas, como demostradores de teoremas o verificadores de modelos, para validar las especificaciones y propiedades del contrato.
• Proceso iterativo: El proceso de verificación se repite para detectar y corregir cualquier desviación respecto a las propiedades previstas, garantizando así que el contrato esté libre de errores.

Técnicas de verificación formal

• Verificación de modelos: La verificación de modelos es una técnica de verificación formal que se utiliza para garantizar que un contrato inteligente se comporte de acuerdo con las especificaciones previstas. Consiste en analizar de forma sistemática un modelo matemático del contrato y verificar si ciertas propiedades se cumplen en dicho modelo. 

• Demostración de teoremas: La demostración de teoremas es un método utilizado para establecer la corrección de los programas, incluidos los contratos inteligentes, mediante el razonamiento matemático. Esta técnica consiste en transformar la descripción del sistema de un contrato y sus especificaciones en enunciados matemáticos precisos conocidos como fórmulas lógicas. El objetivo principal de la demostración de teoremas es demostrar que estas fórmulas lógicas son lógicamente equivalentes. La «equivalencia lógica», también denominada «biimplicación lógica», es una relación entre dos enunciados en la que el primer enunciado es verdadero si y solo si el segundo enunciado es verdadero.

• Ejecución simbólica: La ejecución simbólica es una técnica de verificación formal que se utiliza para analizar el comportamiento de los contratos inteligentes mediante la manipulación de valores simbólicos en lugar de valores concretos. Este método permite razonar sobre las propiedades del código de un contrato de forma sistemática y exhaustiva. Cuando se ejecutan las funciones de un contrato inteligente mediante la ejecución simbólica, los valores de entrada se representan de forma simbólica, en lugar de utilizar valores específicos y concretos. Por ejemplo, en lugar de proporcionar un valor fijo como `x = 5`, se representa como un valor simbólico `x > 5`. Este valor simbólico representa un rango de posibles valores concretos que satisfacen la desigualdad.

2. Pruebas de fuzz

Las pruebas de fuzz, conocidas comúnmente como «fuzzing», son una técnica de pruebas dinámicas de software diseñada para detectar errores y vulnerabilidades en la implementación de las aplicaciones mediante la inyección de datos malformados, inesperados o aleatorios como entradas. Este método se desarrolla en un marco de caja negra, centrándose en el comportamiento externo de la aplicación sin necesidad de conocer su código o lógica internos. El fuzzing mejora la seguridad y la robustez del software, ofreciendo un enfoque automatizado para identificar posibles puntos débiles que podrían pasar desapercibidos con los métodos de prueba convencionales.

3. Pruebas unitarias

Una prueba unitaria comprueba un fragmento de código, como una función, para garantizar que funciona correctamente. Estas pruebas son importantes porque abarcan todos los escenarios posibles para ese fragmento de código concreto y permiten detectar errores que quizá no se detecten en otros tipos de pruebas. 

Cuando realizas una prueba unitaria, seleccionas determinados datos de entrada para comprobar si dan el resultado correcto. La calidad de tu prueba depende de los datos de entrada que elijas. Seleccionar los datos de entrada adecuados es fácil en situaciones previsibles, pero los probadores con experiencia saben elegir bien los datos de entrada inesperados, ya que son precisamente esos los que suelen revelar errores en el código.

4. Pruebas de integración

Una prueba de integración comprueba el funcionamiento de una combinación de unidades. Aunque cada parte funcione correctamente por separado, al combinarlas pueden surgir problemas inesperados. Al realizar pruebas de integración, intenta integrar el mayor número posible de partes. Sin embargo, cuantas más partes se integren, más difícil resultará averiguar por qué ha fallado una prueba. Por lo tanto, una estrategia sencilla consiste en integrar únicamente aquellas partes que se influyan mutuamente en el sistema final.

5. Pruebas funcionales

Una prueba funcional evalúa el sistema —lo que a menudo se denomina «pruebas de historias de usuario»— basándose en las historias de usuario definidas durante la fase inicial de requisitos del proyecto. Estas historias de usuario, que forman parte de las especificaciones técnicas, sirven de guía para escribir el código. Las pruebas funcionales tienen como objetivo confirmar si el sistema cumple estos requisitos. Son importantes porque, aunque las pruebas unitarias y de integración se superen, el fallo en una prueba funcional significa que el sistema no cumple con la finalidad prevista. Por otro lado, si se superan todas las pruebas funcionales, es posible que unos pocos fallos en las pruebas unitarias o de integración no sean tan críticos.

En conclusión 

Las herramientas y técnicas de prueba son importantes para garantizar la fiabilidad, la seguridad y el cumplimiento normativo de los contratos inteligentes. La seguridad de los contratos inteligentes contribuye, en última instancia, a que las aplicaciones basadas en blockchain se adopten y utilicen con éxito. Por eso, las auditorías de contratos inteligentes, los programas de recompensas por errores y las revisiones son fundamentales en todas las fases del desarrollo. Aumentan el número de personas que buscan vulnerabilidades y reducen la probabilidad de que se pasen por alto vulnerabilidades críticas.

‍

Cuídate.
‍‍

Únete a AuditOne como auditor: https://www.auditone.io/auditors

Reserva tu consulta gratuita sobre seguridad:

Google Calendar: https://calendar.app.google/Ai15eyQhiV5c1pBXA
Telegram: https://t.me/m_ndr

‍
Artículos relacionados:

Auditoría de un contrato de Solidity: Episodio 1 — Ataque de reentrada

Auditoría de un contrato de Solidity: Episodio 2 - Delegatecall

Auditoría de un contrato de Solidity: Episodio 3 - Análisis de seguridad

Auditoría de un contrato de Solidity: Episodio 5 - Herramientas de pruebas automatizadas

Auditoría de un contrato de Solidity: Episodio 6 - Frontrunning

Auditoría de un contrato de Solidity: Episodio 7 — Documentación y elaboración de informes

Auditoría de un contrato de Solidity: Episodio 8 - Ventajas de la auditoría