Reportaje a nuestros doctorandos: Javier Godoy

¿Cómo explicarías el tema de tu tesis doctoral?

Mi tesis doctoral se centra en la validación de smart contracts mediante abstracciones por predicado.

Los smart contracts (o contratos inteligentes) se ejecutan sobre una Blockchain inmutable, lo que significa que, si tienen un error, no se puede corregir. Por lo tanto, detectar errores antes de que el contrato esté ejecutándose en la blockchain es crucial.

Entonces, el objetivo de mi investigación es desarrollar un método para generar automáticamente abstracciones (que son máquinas de estado finitas), a partir de información relevante para un auditor. Esta información relevante son los predicados (por ejemplo, si una subasta está abierta o cerrada). De esta manera, un auditor, que tiene una idea clara del comportamiento esperado del contrato, puede comparar esta imagen mental del comportamiento esperado con las abstracciones generadas. A partir de distintos predicados, se pueden generar abstracciones que expliquen diversos aspectos del comportamiento de un contrato inteligente, lo que puede ayudar a su validación. Estas abstracciones además pueden servir para generar casos de tests automáticamente (por ejemplo, guiando un fuzzer para maximizar la cobertura de la abstracción).

¿Qué ejemplos de aplicaciones existen de este tema?

En los últimos años, debido a la expansión en el uso de los smart contracts, han surgido numerosas herramientas que buscan encontrar errores en estos contratos. Sin embargo, la mayoría de estas herramientas se enfocan en la verificación, es decir, en comprobar si un contrato satisface ciertas propiedades, que generalmente se expresan en un lenguaje matemático formal. La generación de abstracciones para smart contracts no ha sido muy explorada aún, aunque sí hay trabajos relacionados para software tradicional.