Smart contracts are programs deployed on a blockchain. They are executed for a monetary fee paid in gas, a clear optimization target for smart contract compilers. Because smart contracts are a young, fast-moving field without (manually) fine-tuned compilers, they highly benefit from automated and adaptable approaches, especially as smart contracts are effectively immutable, and as-such need a high-level of assurance. This makes them an ideal domain for applying formal methods. Super-optimization is a technique to find the best translation of a block of instructions by trying all possible sequences of instructions which produce the same result. We present a framework for super-optimizing smart contracts based on Max-SMT with two main ingredients: (1) a stack functional specification extracted from the basic blocks of a smart contract, which is simplified using rules capturing the semantics of arithmetic, bit-wise, and relational operations, and (2) the synthesis of optimized blocks, which finds, by means of an efficient SMT encoding, basic blocks with minimal gas cost whose stack functional specification is equal (modulo commutativity) to the extracted one. We implemented our framework in the tool SYRUP. Through large-scale experiments on real-world smart contracts we analyze performance improvements for different SMT encodings, as well as trade-offs between quality of optimizations and required optimization time.

@article{AlbertGHRS22,
  author = {Elvira Albert and
               Pablo Gordillo and
               Alejandro Hern\'andez-Cerezo and
               Albert Rubio and
               Maria A. Schett},
  title = {{Super-Optimization of Smart Contracts}},
  journal = {{ACM Transactions on Software Engineering and Methodology}},
  year = {2022},
  note = {To appear}
}

Gas is a measurement unit of the computational effort that it will take to execute every single replicated operation that takes part in the Ethereum blockchain platform. Each transaction executed by the Ethereum Virtual Machine (EVM), has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised, interrupting the current execution. We present, to the best of our knowledge, the first static analysis that is able to infer parametric gas bounds for smart contracts. The inferred bounds are typically parametric on the sizes of the input parameters for the functions, but also they are often parametric on the contract state, and even sometimes they will be parametric on blockchain data. The analysis is implemented in a tool named GASTAP, Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers sound gas upper bounds for its public functions. GASTAP has been applied over the entire contents of the Ethereum blockchain, in total we have been able to analyze 318,397 functions, and succeeded to obtain gas bounds for 91.02% of them.

@article{AlbertCGRR21,
  author = {Elvira Albert and
               Jes\'us Correas and
               Pablo Gordillo and
               Guillermo Rom\'an-D\'iez and
               Albert Rubio},
  title = {{Don't Run on Fumes --- Parametric Gas Bounds for Smart Contracts}},
  journal = {{J}ournal of {S}ystems and {S}oftware},
  volume = {176},
  pages = {110923},
  issn = {0164-1212},
  doi = {https://doi.org/10.1016/j.jss.2021.110923},
  year = {2021},
  rank:jcr:q = {2}
}

Profiling tools have been widely used for studying the behavior of the programs with the objective of reducing the amount of resources consumed by them. Most profilers collect the information with dynamic techniques, i.e., execute an instrumented version of the program with some specific input arguments to profile the measures of interest. This article presents a novel static profiling technique for Ethereum smart contracts that, using static resource analysis, is able to generate upper-bound expressions that can be used to produce profiling information about the measure of interest. Unlike traditional profiling tools, we get upper-bounds on the measures of interest expressed in terms of the input arguments or the state variables of the smart contracts. The information that can be obtained by the upper-bounds allows us to detect gas-expensive fragments of a Solidity program or to spot resource-related vulnerabilities at specific program points of the program. Moreover, in this article we propose an automatic optimization of Solidity programs which reduces their gas consumption replacing the accesses to state variables by gas-efficient accesses to local variables. We have experimentally evaluated our technique and we have detected that 6.81% of the public functions analyzed can be optimized and 1.43% are vulnerable to execute arbitrary code.

@article{CorreasGR21,
  author = {Jes\'us Correas and
               Pablo Gordillo and
               Guillermo Rom\'an-D\'iez},
  title = {{Static Profiling and Optimization of Ethereum Smart Contracts Using Resource Analysis}},
  journal = {{IEEE Access}},
  volume = {9},
  pages = {25495-25507},
  issn = {2169-3536},
  doi = {10.1109/ACCESS.2021.3057565},
  year = {2021},
  rank:jcr:q = {1}
}

Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present GASOLv2, a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also w.r.t. memory and storage. GASOLv2 can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler solc, and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas w.r.t. the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by solc.

@inproceedings{AlbertGHR22,
  author = {Elvira Albert and
               Pablo Gordillo and
               Alejandro Hern\'andez-Cerezo and
               Albert Rubio},
  title = {{A} {M}ax-{SMT}  {S}uperoptimizer for {EVM}
  handling {M}emory and {S}torage},
  booktitle = {28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Proceedings},
  year = {2022},
  rank:grinscie:class = {1},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Dana Fisman and
               Grigore Rosu},
  note = {To appear}
}

With the advent of smart contracts that execute on the blockchain ecosystem, a new mode of reasoning is required for developers that must pay meticulous attention to the gas spent by their smart contracts, as well as for optimization tools that must be capable of effectively reducing the gas required by the smart contracts. Super-optimization is a technique which attempts to find the best translation of a block of code by trying all possible sequences of instructions that produce the same result. This paper presents a novel approach for super-optimization of smart contracts based on Max-SMT which is split into two main phases: (i) the extraction of a stack functional specification from the basic blocks of the smart contract, which is simplified using rules that capture the semantics of the arithmetic, bit-wise, relational operations, etc. (ii) the synthesis of optimized-blocks which, by means of an efficient Max-SMT encoding, finds the bytecode blocks with minimal gas cost whose stack functional specification is equal (modulo commutativity) to the extracted one. Our experimental results are very promising: we are able to optimize 52.78% of the blocks, and prove that 34.28% were already optimal, for more than 61,000 blocks from the most used 2,500 Ethereum contracts.

@inproceedings{AlbertGRS20,
  author = {Elvira Albert and
               Pablo Gordillo and
               Albert Rubio and
               Maria A. Schett},
  title = {{Synthesis of Super-Optimized Smart Contracts using Max-SMT}},
  booktitle = {32nd International Conference on Computer Aided Verification, {CAV}
               2020. Proceedings},
  year = {2020},
  series = {Lecture Notes in Computer Science},
  pages = {177-200},
  volume = {12224},
  doi = {10.1007/978-3-030-53288-8_10},
  isbn = {978-3-030-53288-8}
}

We present the main concepts, components, and usage of GASOL, a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. GASOL offers a wide variety of cost models that allow inferring the gas consumption associated to selected types of EVM instructions and/or inferring the number of times that such types of bytecode instructions are executed. Among others, we have cost models to measure only storage opcodes, to measure a selected family of gas-consumption opcodes following the Ethereum's classification, to estimate the cost of a selected program line, etc. After choosing the desired cost model and the function of interest, GASOL returns to the user an upper bound of the cost for this function. As the gas consumption is often dominated by the instructions that access the storage, GASOL uses the gas analysis to detect under-optimized storage patterns, and includes an (optional) automatic optimization of the selected function. Our tool can be used within an Eclipse plugin for Solidity which displays the gas and instructions bounds and, when applicable, the gas-optimized Solidity function.

@inproceedings{AlbertCGRR20,
  author = {Elvira Albert and
               Jes\'us Correas and
               Pablo Gordillo and
               Guillermo Rom\'an-D\'iez and
               Albert Rubio},
  title = {{GASOL}: {G}as {A}nalysis and {O}ptimization for {E}thereum {S}mart {C}ontracts},
  booktitle = {26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020. Proceedings},
  year = {2020},
  rank:grinscie:class = {1},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {Armin Biere and
               David Parker},
  doi = {10.1007/978-3-030-45237-7_7},
  pages = {118-125},
  volume = {12079},
  isbn = {978-3-030-45237-7}
}

@inproceedings{AlbertCGRR20-icst,
  author = {Elvira Albert and
               Jes\'us Correas and
               Pablo Gordillo and
               Guillermo Rom\'an-D\'iez and
               Albert Rubio},
  title = {{Smart, and also reliable and gas-efficient, contracts}},
  booktitle = {13th {IEEE} International Conference on Software Testing, Validation
               and Verification, {ICST} 2020. Proceedings},
  year = {2020},
  series = {IEEE},
  rank:grinscie:class = {2},
  doi = {10.1109/ICST46399.2020.00010}
}

Abstract. Gas is a measurement unit of the computational effort that it will take to execute every single operation that takes part in the Ethereum blockchain platform. Each instruction executed by the Ethereum Virtual Machine (EVM) has an associated gas consumption specified by Ethereum. If a transaction exceeds the amount of gas allotted by the user (known as gas limit), an out-of-gas exception is raised. There is a wide family of contract vulnerabilities due to out-of-gas behaviors. We report on the design and implementation of Gastap, a Gas-Aware Smart contracT Analysis Platform, which takes as input a smart contract (either in EVM, disassembled EVM, or in Solidity source code) and automatically infers gas upper bounds for all its public functions. Our bounds ensure that if the gas limit paid by the user is higher than our inferred gas bounds, the contract is free of out-of-gas vulnerabilities.

@inproceedings{AlbertGRS19,
  author = {Elvira Albert and
               Pablo Gordillo and
               Albert Rubio and Ilya Sergey},
  title = {{R}unning on {F}umes: {P}reventing {O}ut-{O}f-{G}as {V}ulnerabilities in {E}thereum {S}mart {C}ontracts using {S}tatic {R}esource {A}nalysis},
  booktitle = {13th International Conference on Verification and Evaluation of Computer and Communication Systems, {VECoS} 2019. Proceedings},
  year = {2019},
  publisher = {Springer},
  editor = {Pierre Ganty and
               Mohamed Ka\^aniche},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-35092-5_5},
  pages = {63-78},
  volume = {11847},
  isbn = {978-3-030-35092-5}
}

Ethereum smart contracts are public, immutable and distributed and, as such, they are prone to vulnerabilities sourcing from programming mistakes of developers. This paper presents SAFEVM, a verification tool for Ethereum smart contracts that makes use of state-of-the-art verification engines for C programs. SAFEVM takes as input an Ethereum smart contract (provided either in Solidity source code, or in compiled EVM bytecode), optionally with assert and require verification annotations, and produces in the output a report with the verification results. Besides general safety annotations, SAFEVM handles the verification of array accesses: it automatically generates SV-COMP verification assertions such that C verification engines can prove safety of array accesses. Our experimental evaluation has been undertaken on all contracts pulled from etherscan.io (more than 24,000) by using as back-end verifiers CPAchecker, SeaHorn and VeryMax.

@inproceedings{AlbertCGRR19,
  author = {Elvira Albert and
               Jes\'us Correas and
               Pablo Gordillo and
               Guillermo Rom\'an-D\'iez and
               Albert Rubio},
  title = {{SAFEVM}: {A} {S}afety {V}erifier for {E}thereum {S}mart {C}ontracts},
  booktitle = {ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019. Proceedings},
  year = {2019},
  series = {ACM},
  rank:grinscie:class = {1},
  pages = {386--389},
  editor = {Dongmei Zhang and
               Anders M{\o}ller},
  doi = {10.1145/3293882.3338999}
}

Abstract. Analyzing Ethereum bytecode, rather than the source code from which it was generated, is a necessity when: (1) the source code is not available (e.g., the blockchain only stores the bytecode), (2) the information to be gathered in the analysis is only visible at the level of bytecode (e.g., gas consumption is specified at the level of EVM instructions), (3) the analysis results may be affected by optimizations performed by the compiler (thus the analysis should be done ideally after compilation). This paper presents EthIR, a framework for analyzing Ethereum bytecode, which relies on (an extension of) OYENTE, a tool that generates CFGs; EthIR produces from the CFGs, a rule-based representation (RBR) of the bytecode that enables the application of (existing) high-level analyses to infer properties of EVM code.

@inproceedings{AlbertGLRS18,
  author = {Elvira Albert and Pablo Gordillo and Benjamin Livshits and Albert Rubio and Ilya Sergey},
  title = {EthIR: A {F}ramework for {H}igh-{L}evel {A}nalysis of {E}thereum {B}ytecode},
  editor = {Shuvendu Lahiri and Chao Wang},
  booktitle = {16th International Symposium on Automated Technology for Verification and Analysis, {ATVA} 2018. Proceedings},
  publisher = {Springer},
  year = {2018},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-030-01090-4_30},
  pages = {513-520},
  volume = {11138},
  isbn = {978-3-030-01089-8}
}

Abstract. May-Happen-in-Parallel (MHP) is a fundamental analysis to reason about concurrent programs. It infers the pairs of program points that may execute in parallel, or interleave their execution. This information is essential to prove, among other things, absence of data races, deadlock freeness, termination, and resource usage. This paper presents an MHP analysis for asynchronous programs that use futures as synchronization mechanism. Future variables are available in most concurrent languages (e.g., in the library concurrent of Java, in the standard thread library of C++, and in Scala and Python). The novelty of our analysis is that it is able to infer MHP relations that involve future variables that are returned by asynchronous tasks. Futures are returned when a task needs to await for another task created in an inner scope, e.g., task t needs to await for the termination of task p that is spawned by task q that is spawned during the execution of t (not necessarily by t). Thus, task p is awaited by task t which is in an outer scope. The challenge for the analysis is to (back)propagate the synchronization of tasks through future variables from inner to outer scopes.

@inproceedings{AlbertGG17,
  author = {Elvira Albert and Samir Genaim and Pablo Gordillo},
  title = {May-{H}appen-in-{P}arallel {A}nalysis with {R}eturned {F}utures},
  editor = {Deepak D'Souza and K.Narayan Kumar},
  booktitle = {15th International Symposium on Automated Technology for Verification and Analysis, {ATVA} 2017. Proceedings},
  publisher = {Springer},
  year = {2017},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-319-68167-2_3},
  pages = {42-58},
  volume = {10482},
  isbn = {978-3-319-68167-2}
}

Abstract. A may-happen-in-parallel (MHP) analysis computes pairs of program points that may execute in parallel across different distributed components. This information has been proven to be essential to infer both safety properties (e.g., deadlock freedom) and liveness properties (termination and resource boundedness) of asynchronous programs. Existing MHP analyses take advantage of the synchronization points to learn that one task has finished and thus will not happen in parallel with other tasks that are still active. Our starting point is an existing MHP analysis developed for intra-procedural synchronization, i.e., it only al- lows synchronizing with tasks that have been spawned inside the current task. This paper leverages such MHP analysis to handle inter-procedural synchronization, i.e., a task spawned by one task can be awaited within a different task. This is challenging because task synchronization goes beyond the boundaries of methods, and thus the inference of MHP relations requires novel extensions to capture inter-procedural dependencies. The analysis has been implemented and it can be tried online.

@inproceedings{AlbertGG15,
  author = {Elvira Albert and Samir Genaim and Pablo Gordillo},
  title = {May-{H}appen-in-{P}arallel {A}nalysis for {A}synchronous {P}rograms with {I}nter-{P}rocedural {S}ynchronization},
  booktitle = {Static Analysis - 22nd International Symposium, {SAS} 2015. Proceedings},
  editor = {Sandrine Blazy and
               Thomas P. Jensen},
  publisher = {Springer},
  year = {2015},
  rank:grinscie:class = {2},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-662-48288-9_5},
  url = {http://dx.doi.org/10.1007/978-3-662-48288-9_5},
  pages = {72-89},
  volume = {9291},
  isbn = {978-3-662-48287-2}
}

@techreport{AlbertCGRR20bTR,
  author = {Elvira Albert and
               Jes\'us Correas and
               Pablo Gordillo and
               Guillermo Rom\'an-D\'iez and
               Albert Rubio},
  title = {{A}nalyzing {S}mart {C}ontracts: {F}rom {EVM} to a {S}ound {C}ontrol-{F}low {G}raph},
  year = {2020}
}

Nowadays concurrency and distribution have become a fundamental part in the software development process. The Internet and the more extended use of multicore processors have influenced the type of the applications which are being developed. This has lead to the creation of several concurrency models. In particular, a concurrency model that is gaining popularity is the actor model, the basis for concurrent objects. In this model, the objects (actors) are the concurrent units. Each object has its own processor and a local state, and the communication between them is carried out using message passing. In response to receiving a message, an actor can update its local state, send messages or create new objects. Developing correct concurrent programs is known to be harder than writing sequential ones because of inherent aspects of concurrency such as data races or deadlocks. To ensure the correct behavior of concurrent programs, static analyses and verification techniques have been developed for the diverse existent concurrency models. The May-Happen-in-Parallel (MHP) analysis is a static analysis that infers pairs of program points that may execute in parallel across the different distributed components. In the actor model, the analysis uses the information from those program points where asynchronous calls to methods are made (i.e., the points where new tasks are spawned), and the synchronization primitives (i.e., the points where the tasks are awaited). This information has been proven to be essential to infer both safety properties (deadlock freedom) and liveness properties (termination and resource consumption) of asynchronous programs. Other aspects that have influenced the progress of distributed systems are the growth of technologies and platforms based on blockchain and consensus protocols. These technological advances have allowed the development of decentralized platforms such us Bitcoin and Ethereum with their respective cryptocurrencies: Bitcoin and Ether. In addition, thanks to the smart contracts, the applications of these blockchain-based technologies are increasing. Smart contracts are computing programs that contain the terms of a real contract and are able to react automatically to the various events specified on them. The contracts can be written by any user and, therefore, are prone to programming errors. These errors may abort the execution, which cause an economical cost to revert the state of each node of the system. Thus, analysis and verification techniques urge to ensure the correct behavior of smart contracts. Within this framework, the main objectives achieved by this thesis are: * Improving the existing MHP analyses. There are numerous MHP analyses developed for several languages and concurrency models. In particular, this thesis bases on the MHP analysis developed for the ABS language, a language based on the actor model and proposes improvements on the analysis to enhance its scalability and accuracy. It also studies how this analysis can be combined with others to increase its precision as well as its applicability to smart contracts. * Developing an intermediate representation for Ethereum bytecode. This representation allows applying existent high level analyses to infer properties over the bytecode. * Developing analyses to study vulnerabilities over Ethereum smart contracts. Specially, we have investigated vulnerabilities related to the gas consumption associated with the execution of smart contracts and those related to the execution of the bytecode instruction INVALID. The objectives mentioned above are reflected in the following publications: 1 - The paper published at SAS'15 presents an \mhp analysis with inter-procedural synchronization for languages based on concurrent objects. This work extends the basic MHP analysis introduced by Albert et al. in FORTE'12 to allow for the synchronization of a task in a distinct scope from the one where it was created, i.e., a task spawned by one task can be awaited within a different task. 2 - The paper published at ATVA'17 presents an MHP analysis for asynchronous programs that use future variables as synchronization mechanism. This analysis is able to infer the MHP relations that involve future variables that are returned by asynchronous tasks. As the previous analysis, it is based on the basic analysis presented in FORTE'12. 3 - The paper published at ATVA'18 presents the tool EthIR which decompiles the Ethereum bytecode into a high-level rule-based intermediate representation. This representation reconstructs the control and data flow of the bytecode from a low-level codification. 4 - The paper published at ISSTA'19 presents SAFEVM, a verifier of Ethereum smart contracts that makes use of state-of-the art verification engines for C programs. SAFEVM is able to verify conditions introduced in the original source code via assertions, array accesses and divisions by 0. 5 - Finally, the paper published at VECoS'19 presents GASTAP, a tool that is able to infer automatically overapproximations of the gas that a public function of a smart contract is going to consume during its execution. GASTAP implements a static analysis that infers gas upper bounds parameterized in terms of the size of the arguments of the functions of the contract, the state of the contract or blockchain data. Finally, all analyses and techniques developed are available online using a web interface.

Abstract. This work presents a May-Happen-in-Parallel (MHP) analysis with returned futures for languages based on concurrent objects. The concurrency model is based on the actor model where the objects are the concurrency units. The idea behind it is that each object has its own processor. MHP is a fundamental analysis to reason about concurrent programs. It infers the pairs of program points that may execute in parallel, or interleave their execution. This information is essential in order to prove, among other things, absence of data races, deadlock freeness, termination, and resource usage. The existing MHP analyses take advantage of the synchronization points. These points are used by the analysis to learn if a task has finished its execution and thus will not happen in parallel with the other tasks that are executing. This thesis presents an MHP analysis for asynchronous programs that use futures as synchronization mechanism. Future variables are available in most concurrent languages (e.g., in the library concurrent of Java, in the standard thread library of C++, and in Scala and Python). The novelty of our analysis is that it is able to infer MHP relations that involve future variables that are returned by asynchronous tasks. Futures are returned when a task needs to await for another task created in an inner scope, e.g., task t needs to await for the termination of task p that is spawned by task q that is spawned during the execution of t (not necessarily by t). Thus, task p is awaited by task t which is in an outer scope. The challenge for the analysis is to (back)propagate the synchronization of tasks through future variables from inner to outer scopes. The analysis presented over-approximates the real parallelism of a program and is carried out in two phases: (1) a local phase to infer the relations existing between the different methods and (2) a global phase where the information extracted from the local phase is composed. Finally, the implementation of the analysis has been integrated in SACO, a static analyzer of concurrent programs.

Abstract. This work presents a may-happen-in-parallel analysis with inter-procedural synchronization for languages based in concurrent objects. In this model of concurrency (based on actors) the objects are the concurrency units. The idea behind it is that each object has its own processor. A may-happen-in-parallel (MHP) analysis computes pairs of program points that may execute in parallel across different distributed components. This information has been proven to be essential to infer both safety properties (e.g., deadlock freedom) and liveness properties (termination and resource boundedness) of asynchronous programs. Existing MHP analyses take advantage of the synchronization points to learn that one task has finished and thus will not happen in parallel with other tasks that are still active. Our starting point is an existing MHP analysis developed for intra-procedural synchronization, i.e., it only allows synchronizing with tasks that have been spawned inside the current task. This paper leverages such MHP analysis to handle inter-procedural synchronization, i.e., a task spawned by one task can be awaited within a different task. This is challenging because task synchronization goes beyond the boundaries of methods, and thus the inference of MHP relations requires novel extensions to capture inter-procedural dependencies. We can distinguish different phases in the development of the analysis: The first one where MHF analysis is performed to infer the relations of synchronization that exist between the methods, a second local phase to analyze each method separately and a last phase to composed all information. As the problem is undecidable when considering a full concurrent objects programming language, the analysis over-approximates the real parallelism programs. Finally, the implementation of the analysis has been integrated in SACO, a static analyzer of concurrent programs.