Título: Abstracciones mediante predicados para la validación de contratos inteligentes

Director: Dr. Juan Pablo Galeotti
Consejero de estudios: Dr. Ricardo O. Rodriguez

Jurados:
Dra. Alessandra Gorla , Associate Research Professor, IMDEA Software Institute.
Dr. German E. Regis, Profesor Adjunto, Universidad Nacional de Río Cuarto
Dr. Renzo Degiovanni, Senior Research Scientist, Luxembourg Institute of Science and Technology (LIST).

Link Youtube: Se compartirá unos días antes de la defensa.

Resumen:

La verificación y validación de contratos inteligentes es crucial debido a la naturaleza inmutable de la blockchain, donde los errores introducidos antes del despliegue no pueden corregirse posteriormente. Por esta razón, han surgido numerosas empresas especializadas en la auditoría de contratos inteligentes, y es frecuente que un mismo contrato sea auditado por múltiples equipos independientes, lo que evidencia tanto la criticidad como la complejidad del proceso. En la práctica, la auditoría de contratos inteligentes depende en gran medida del conocimiento y la experiencia de los auditores humanos, y continúa siendo en gran parte un proceso manual, a pesar de la disponibilidad creciente de herramientas automáticas y semi-automáticas. En general, muchas de las herramientas actuales se centran en la verificación, y requieren la especificación explícita de propiedades, invariantes o patrones de vulnerabilidades a ser analizados.

Esta tesis propone un enfoque basado en abstracciones por predicados para asistir la auditoría de contratos inteligentes, específicamente en la red Ethereum, aunque aplicable a otros entornos donde los contratos inteligentes implementan protocolos. A diferencia de otros enfoques, la tesis se centra en la validación, es decir, en ayudar a los auditores a comprender si se está cumpliendo con los requerimientos del contrato. Esto se logra mediante la construcción de modelos abstractos representados como máquinas de estados finitos, que capturan las posibles secuencias de llamadas a funciones y sus efectos en el estado del contrato. El método propuesto permite, a partir de predicados definidos por el auditor, generar diferentes visualizaciones del comportamiento de los contratos inteligentes.

Los principales aportes de esta tesis incluyen: (i) la formalización de dos tipos de abstracciones por predicados (may/must) aplicadas al análisis de contratos inteligentes; (ii) técnicas de refinamiento de transiciones y estados que permiten focalizar el análisis en escenarios específicos de interés; (iii) la incorporación de estados transitorios para capturar comportamientos intermedios relevantes, como aquellos asociados a vulnerabilidades de reentrada; (iv) la implementación de las técnicas propuestas en dos prototipos funcionales, uno basado en Alloy y otro en un verificador formal; y (v) una evaluación empírica de las abstracciones mediante benchmarks establecidos y estudios con auditores experimentados.

Los resultados obtenidos muestran que los modelos abstractos generados a partir de predicados permiten identificar defectos y patrones no detectados por herramientas existentes. Además, la evaluación aporta evidencia de que las abstracciones propuestas facilitan la comprensión del comportamiento de los contratos inteligentes por parte de los auditores.