Analysis techniques for Smart contracts: generation of complete control flow graphs

Abstract

Ethereum is the most popular blockchain. It has become really well-known in the last few years because it lets users deploy their smart contracts on top of it. Gas is used to measure the computational effort when executing a transaction and to reward miners. Users set the gas limit when proposing a transaction, and if the miner runs out of gas before performing it, an out-of-gas exception is raised, reverting to the previous state before execution. Thus, inferring gas consumption is really important for not losing resources. Besides, some exploits have been found that have led to major economic losses, due to subtle bugs in the code. An example of it is the famous DAO attack. In order to tackle the efficiency and soundness problems mentioned above, we have to rely on formal methods that guarantee the soundness and accuracy of possible analysis. Research has been done previously in this topic, and it has led to the creation of tolos that analyze different features on Ethereum Virtual Machine(EVM) code. Among them, Gastap is one of the few tools based on static analysis that manages to infer gas upper bounds for transactions. Gastap is one of the most accurate tools in the field, having a great success rate. It generates a Control-Flow-Graph (CFG) as an intermediate representation of the analysis. However, the current algorithm used by Gastap is not precise. Therefore, a considerable number of smart contracts cannot be analyzed. This dissertation proposes a new algorithm for generating a Complete CFG from an EVM smart contract. We will prove that this algorithm is sound, and prove completeness is lost only in certain cases. It greatly improves the performance from the previous version. Experiments corroborate this fact: we have analyzed a total of 10,736 files, generating a CFG from roughly 90%, in contrast with the 80% of the contracts that could be analyzed before. From the 10% remaining, only less than 1% of the contracts still fail due to our analysis. Besides, we achieve a great efficiency: CFG generation time takes less than 0,01% of the total time for the analysis. Another key feature of the proposed algorithm is that it can be easily implemented and adapted to other stack-based programs.

Ethereum es la cadena de bloques más popular. Se ha convertido en una plataforma muy conocida en los últimos años, permitiendo a los usuarios desplegar sus dApps en ella. Ethereum utiliza el llamado Gas para medir el coste computacional de ejecutar una transacción y así recompensar a los mineros. Para ello, los usuarios tienen que fijar un límite de gas a la hora de proponer una transacción, de tal forma que, si se agota durante la ejecución, se genera una excepción, y se revierte al estado previo a la ejecución. Es por ello que determinar el consumo de gas es muy importante para no malgastar recursos. Además, se han encontrado algunas vulnerabilidades que pueden conducir a grandes pérdidas económicas. Un ejemplo de ello es el conocido DAO attack. Para abordar las situaciones de eficiencia y corrección descritas anteriormente, tenemos que recurrir a métodos formales que nos garanticen la precisión de posibles análisis. Se han llevado a cabo diversas investigaciones en este campo, que han llevado a la creación de distintas herramientas para el análisis de propiedades de los contratos inteligentes. Entre ellas, destaca Gastap, una herramienta que permite inferir cotas superiores del consumo de gas de transacciones. Es una de las herramientas con mayor porcentaje de contratos analizados con éxito. Para ello, genera un Grafo de control de flujo (CFG) en una de las etapas intermedias del análisis. Sin embargo, el algoritmo empleado actualmente no es preciso, por lo que hay un número considerable de contratos que no son analizados correctamente. Este trabajo propone un nuevo algoritmo para generar un Grafo de control de flujo completo de un contrato inteligente. Probaremos que este análisis es correcto, y que perdemos información únicamente en ciertos casos. Los resultados muestran como el nuevo algoritmo mejora bastante con respecto al anterior: hemos analizado un total de 10,736 archivos, de los que podemos generar su CFG para casi un 90%. Con el análisis anterior, éramos capaces de generar un 80% de los casos. Del 10% de contratos restantes, menos del 1% fallan por culpa de nuestro algoritmo. Además, este algoritmo es muy eficiente, pues supone menos de un 0,01% del tiempo de ejecución del análisis completo. Otro aspecto relevante de este algoritmo es que es fácilmente implementable, y que puede ser adaptado a otros lenguajes basados en la pila.