Análisis estático de sistemas concurrentes y distribuidosobjetos concurrentes y bytecode de Ethereum

Laburpena

Hoy en día la concurrencia y la distribución se han convertido en una parte fundamental del proceso de desarrollo de software. Internet y el uso cada vez más extendido de los procesadores multicore ha influido en el tipo de aplicaciones que se desarrollan. Esto ha dado lugar a la creación de distintos modelos de concurrencia. En particular, uno de los modelos de concurrencia que está ganando importancia es el modelo de objetos concurrentes basado en actores. En este modelo, los objetos (denominados actores) son las unidades de concurrencia. Cada objeto tiene su propio procesador y un estado local. La comunicación entre los mismos se lleva a cabo mediante el paso de mensajes. Cuando un objeto recibe un mensaje puede: actualizar su estado, mandar mensajes o crear nuevos objetos. Además la creación de programas concurrentes correctos es más compleja que la de programas secuenciales ya que es necesario tener en cuenta distintos aspectos inherentes a la concurrencia como los errores asociados a las carreras de datos o a los interbloqueos. El análisis de May-Happen-in-Parallel (Puede-Ocurrir-en-Paralelo) es un análisis estático que infiere pares de puntos del programa que pueden ejecutarse en paralelo en distintas componentes distribuidas. En el modelo basado en actores, el análisis utiliza la información de los puntos del programa en los que se producen las llamadas asíncronas a métodos (es decir, los puntos donde se crean nuevas tareas), y las primitivas de sincronización (es decir, los puntos donde se espera a que las tareas terminen para continuar con su ejecución). Esta información ha resultado ser esencial para inferir propiedades de corrección (ausencia de bloqueo) y propiedades de viveza (terminación y consumo de recursos) de programas asíncronos. Otro de los aspectos que ha influido en el desarrollo de sistemas distribuidos ha sido el auge de tecnologías y plataformas basadas en cadena de bloques (en adelante blockchain) y los protocolos de consenso. Estos avances tecnológicos han permitido el desarrollo de plataformas descentralizadas como Bitcoin o Ethereum junto a sus respectivas criptomonedas. Los contratos inteligentes son programas informáticos donde se recogen los términos de un contrato y son capaces de reaccionar de forma automática ante los distintos eventos especificados en los mismos. Los contratos pueden ser creados por cualquier usuario, y por tanto son susceptibles a errores de programación. Estos errores pueden provocar que se aborte la ejecución, lo que supone un coste económico necesario para revertir el estado de todos los nodos del sistema. Es por ello que el desarrollo de técnicas de análisis y verificación que permitan asegurar el correcto funcionamiento de los contratos inteligentes se ha convertido en un tema de investigación de gran interés y relevancia. Dentro de este marco, los principales objetivos que se han perseguido con el desarrollo de esta tesis son: Estudiar los análisis de May-Happen-in-Parallel (MHP) existentes para distintos lenguajes y modelos de concurrencia. Concretamente se ha profundizado en el análisis MHP desarrollado para el lenguaje ABS, un lenguaje que implementa el modelo basado en actores y se han investigado mejoras en el análisis para mejorar su precisión y escalabilidad. También se ha estudiado la combinación de otros análisis para incrementar su precisión así como su aplicación a los contratos inteligentes. Desarrollar una representación intermedia para el bytecode de Ethereum. Esta representación permite la aplicación de análisis de alto nivel para inferir propiedades sobre el bytecode de Ethereum. Desarrollar análisis que permitan estudiar vulnerabilidades sobre contratos inteligentes de Ethereum. En particular se han estudiado las vulnerabilidades derivadas del consumo de gas asociado a la ejecución de los contratos inteligentes y las provocadas por la ejecución del bytecode INVALID.