Input Output demuestra Blaster para la verificación de contratos inteligentes de Cardano

Cardano Community ha publicado una presentación de Blaster, una herramienta de verificación automatizada diseñada para comprobar si los contratos inteligentes de Cardano siguen las reglas especificadas. Los ingenieros de Input Output Romain Soulat y Jean-Frédéric Etienne demuestran cómo la herramienta examina esas propiedades y puede producir un contraejemplo cuando detecta una infracción. También comentan el trabajo en curso sobre la reconstrucción de pruebas y formas de hacer que los resultados sean más fáciles de inspeccionar.

Definir lo que debe hacer un contrato de Cardano

Los contratos inteligentes establecen condiciones para las transacciones en la blockchain y determinan cómo las aplicaciones gestionan los activos. Un desarrollador podría especificar, por ejemplo, que solo un usuario autorizado puede desbloquear fondos retenidos por un contrato. La verificación formal utiliza métodos matemáticos para comprobar si un sistema satisface propiedades escritas en una especificación. Mientras que una prueba convencional examina casos seleccionados, la verificación formal busca establecer si una propiedad indicada se cumple en los casos contemplados por el modelo.

Soulat, líder técnico de Cardano High Assurance, explicó que Blaster está pensado para automatizar buena parte del trabajo de demostración. Los desarrolladores aún deben definir el comportamiento que quieren comprobar y proporcionar la especificación correspondiente. Cuando la herramienta encuentra una infracción, puede producir un contraejemplo para su inspección. Soulat describió una transacción o una secuencia de transacciones que podría mostrar a alguien distinto del usuario autorizado desbloqueando una salida.

Cómo Blaster verifica las propiedades de los contratos

Blaster utiliza Lean 4, un sistema para expresar enunciados matemáticos y trabajar con demostraciones, junto con un solucionador automatizado. Primero simplifica el problema; si la propiedad no se resuelve durante esa fase, el problema restante puede enviarse al solucionador. Para que las comprobaciones sean pertinentes para Cardano, el equipo ha formalizado partes del entorno en el que se ejecutan los contratos, incluida la ejecución de scripts y las reglas de transacciones.

Etienne, ingeniero sénior de métodos formales, describió tres posibles resultados: una propiedad puede declararse válida, falsada o indeterminada. Un contraejemplo asociado a un resultado falsado puede ayudar a los desarrolladores a identificar un error en el contrato, una suposición ausente o un fallo en la especificación. Un resultado indeterminado significa que el solucionador no ha establecido si la propiedad se cumple. El alcance de una comprobación depende de las propiedades que los desarrolladores elijan expresar.

[NEWSBREAK]

La reconstrucción de pruebas está en desarrollo

Los desarrolladores pueden compilar contratos escritos en lenguajes como Plinth, Aiken o Plutarch a Untyped Plutus Core, la representación utilizada para ejecutar scripts de Cardano. Luego pueden importar el código compilado en Lean 4 y especificar las propiedades que se van a comprobar. Input Output publicó anteriormente dos bibliotecas de código abierto que proporcionan los modelos específicos de Cardano para este proceso. En una demostración anterior, el equipo utilizó la canalización en un contrato de práctica de un desafío de seguridad, generando un contexto de transacción que mostró cómo podía explotarse el contrato.

Etienne explicó que la reconstrucción de pruebas sigue en desarrollo. El objetivo es permitir que Lean verifique de forma independiente la evidencia que respalda un resultado válido; la herramienta actual aún no produce una demostración de Lean reconstruida cuando el solucionador devuelve ese resultado. Soulat también expuso planes para vistas de contraejemplos más claras, que permitan a los desarrolladores inspeccionar los detalles de la transacción detrás de una propiedad fallida.