Abstracción de contratos inteligentes mediante ejecución simbólica dinámica

Resumen

Los contratos inteligentes 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 contratos inteligentes. Sin embargo, se han explotado numerosas vulnerabilidades en los últimos años provocando pérdidas a miles de personas. En este trabajo presentamos el desarrollo de un prototipo que, dado el código fuente de un contrato inteligente, genera máquinas de estado finitas que abstraen el comportamiento del contrato. Estas abstracciones que se basan en predicados sobre la habilitación de los métodos del contrato han resultado útiles anteriormente como herramienta para la validación de código contra especificaciones informales y para descubrir errores latentes. El prototipo implementado hace uso y extensión de una herramienta open source de ejecución simbólica dinámica denominada Manticore. Además, hacemos pública la implementación del prototipo, junto con las pruebas realizadas contra contratos ejemplo.