Título: Construcción de abstracciones de comportamiento para contratos inteligentes mediante ejecución simbólica

Directores: Javier Godoy, Diego Garbervetsky

Jurados: Dr. Ariel Waissbein, Dr. Sebastián Uchitel

Resumen:

Los smart contracts son programas inmutables que se despliegan en una blockchain. Dado que a menudo manejan activos de alto valor real, su verificación y validación antes de desplegarlos es de gran importancia. Por esta razón, es una práctica común contratar empresas de seguridad especializadas para auditar el código de los smart contracts. Sin embargo, se han explotado numerosas vulnerabilidades en los últimos años provocando pérdidas a miles de personas. Las Enabledness Preserving Abstractions (EPAs), son máquinas de estado finitas que abstraen el comportamiento de artefactos de código, basándose en predicados sobre la habilitación de los métodos disponibles. En general, han resultado útiles como herramienta para la validación de código tanto contra especificaciones formales como contra modelos informales o “mentales” del comportamiento esperado. Presentamos un prototipo que genera EPAs de contratos inteligentes a partir de código fuente, haciendo uso y extensión de una herramienta open source de ejecución simbólica dinámica: “Manticore”. Discutimos las optimizaciones implementadas y comparamos el prototipo desarrollado con otras estrategias alternativas.