Título: Verificación de smart contracts en Ethereum: un estudio y un prototipo

Director: Diego Garbervetsky

Jurados: Juan Pablo Galeotti, Hernan Melgratti

Resumen:

Los contratos inteligentes, o smart contracts, son programas que pueden ser ejecutados consistentemente por una red de nodos que se desconfían mutuamente, sin el arbitraje de una autoridad centralizada. Debido a su resistencia a la manipulación, los smart contracts son atractivos en muchos escenarios, especialmente en aquellos que requieren transferencias de dinero respetando ciertas reglas acordadas. Desafortunadamente, programar smart contracts es una tarea delicada que requiere experiencia: sus aplicaciones y la semántica de los sistemas descentralizados inevitablemente introducen una gran cantidad de problemas de seguridad. Por lo tanto, surgieron métodos y herramientas para apoyar el desarrollo de smart contracts seguros. Evaluar la calidad de estas herramientas resulta difícil.
Esta tesis pretende ser una guía para quienes tienen la intención de analizar smart contracts, ya sea durante una auditoría o durante el desarrollo de aplicaciones descentralizadas. En particular, para los auditores de OpenZeppelin, que mostraron interés en el análisis automático y quieren aplicarlo en su trabajo diario. Además de realizar este estudio sobre técnicas de análisis automático para smart contracts, también desarrollamos una herramienta prototipo que combina dos enfoques existentes y agrega un lenguaje de especificación para crear un monitor para controles de seguridad. Este monitor se implementó como una instrumentación del contrato proporcionado, por lo que se puede evaluar con casi cualquier programa de análisis para así aprovechar sus capacidades, y al mismo tiempo expresar invariantes del contrato en un lenguaje inspirado en las lógicas temporales.