Chunmiao Li, Shijie Nie, Yang Cao, Yijun Yu · 5 authors
Smart contracts on Ethereum can be used to encode business logic and have been applied to many different areas, such as token exchanges and games. Unlike general programs, the computations of contracts on Ethereum are restricted by the gas limit. If a transaction runs out of the gas limit before an execution finishes, the Ethereum virtual machine throws an out-of-gas exception, and the entire transaction fails, which reverts to the state before the transaction started, although the transaction fee is still deducted. It is therefore, essential to conduct a gas estimation before sending a transaction. Existing studies have mostly failed in estimating the gas for a loop function because the number of iterations of the loops cannot be statically determined. However, we found that a quarter of all contracts have loop functions, and the gas cost for the loops is higher than for the other functions. Therefore, it is necessary to apply a gas estimation for the loop functions. In this study, we propose a gas estimation approach based on the transaction trace to dynamically estimate the gas for the loop functions. Our belief is that we can learn the relationship between the historical transaction traces and their gas costs to estimate the gas for new transactions. We considered three different abstractions of the original transaction trace and fed them to different machine learning models. The results show that our approach is effective in gas estimation and that a random forest can achieve the most accurate estimation.
We address the absence of reliable tests on contract analyzers of smart contracts and present a systematic method to diversify test cases by combining smart-contract-specific bugs and static analysis barriers in this paper. Using contract analyzers is the most practical solution for building a secure blockchain service, but they are relatively immature and lacking stable performance metrics. Traditionally, performance reports only compare static contract analyzers with pre-defined test cases, such as the Juliet test suite. However, building such test suites is burdensome for smart contracts, which are frequently change. In this paper, we propose an automated method to assess contract analyzers of smart contracts by diversifying test cases. In the experimental results, we identified nine erroneous alarms in the state-of-the-art contract analyzers with automatically generated test cases on five vulnerabilities.
With the growing popularity of smart contracts, the problem of validation of their correctness becomes more and more relevant, but at the moment there are no universally recognized tools for their testing. In this paper, we propose to apply the mutational analysis to improve reliability of Solidity smart contracts. We identified wide spread errors in the source code of existing contracts and developed a RegularMutator tool for mutation analysis. It has shown its effectiveness in testing a large smart contracts project. As a result of our analysis, we managed to improve the test suites of the project to find the discovered defects and, increase the quality of the test suite.
Ethereum smart contracts are distributed programs running on top of the Ethereum blockchain. Since program flaws can cause significant monetary losses and can hardly be fixed due to the immutable nature of the blockchain, there is a strong need of automated analysis tools which provide formal security guarantees. Designing such analyzers, however, proved to be challenging and error-prone. We review the existing approaches to automated, sound, static analysis of Ethereum smart contracts and highlight prevalent issues in the state of the art. Finally, we overview eThor, a recent static analysis tool that we developed following a principled design and implementation approach based on rigorous semantic foundations to overcome the problems of past works.
Smart contracts can be regarded as one of the most popular blockchain-based applications. The decentralized nature of the blockchain introduces vulnerabilities absent in other programs. Furthermore, it is very difficult, if not impossible, to patch a smart contract after it has been deployed. Therefore, smart contracts must be formally verified before they are deployed on the blockchain to avoid attacks exploiting these vulnerabilities. There is a recent surge of interest in analyzing and verifying smart contracts. While most of the existing works either focus on EVM bytecode or translate Solidity contracts into programs in intermediate languages for analysis and verification, we believe that a direct executable formal semantics of the high-level programming language of smart contracts is necessary to guarantee the validity of the verification. In this work, we propose a generalized formal semantic framework based on a general semantic model of smart contracts. Furthermore, this framework can directly handle smart contracts written in different high-level programming languages through semantic extensions and facilitates the formal verification of security properties with the generated semantics.
Elvira Albert, Pablo Gordillo, Albert Rubio, Maria A. Schett
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 55.41 % of the blocks, and prove that 34.28 % were already optimal, for more than 61000 blocks from the most called 2500 Ethereum contracts.
Zero-knowledge (ZK) proofs (ZKP) have received wide attention, focusing on non-interactivity, short proof size, and fast verification time. We focus on the fastest total proof time, in particular for large Boolean circuits. Under this metric, Garbled Circuit (GC)-based ZKP (Jawurek et al., [JKO], CCS 2013) remained the state-of-the-art technique due to the low-constant linear scaling of computing the garbling.
Mauro C. Argañaraz, Mario Berón, Maria João Varanda Pereira, Pedro Rangel Henriques
Ethereum is the principal ecosystem based on blockchain that provides a suitable environment for coding and executing smart contracts, which have been receiving great attention due to the commercial apps and among the scientific community. The process of writing secure and well performing contracts in the Ethereum platform is a major challenge for developers. It consists of the application of non-conventional programming paradigms due to the inherent characteristics of the execution of distributed computing programs. Furthermore, the errors in the deployed contracts could have serious consequences because of the immediate linkage between the contract code and the financial transactions. The direct handling of the assets means that the errors can be more relevant for security and have greater economic consequences than a mistake in the conventional apps. In this paper, we propose a tool for the detection of vulnerabilities in high-level languages based on automatized static analysis.
Smart contracts are programs that reside within decentralized blockchains and are executed pursuant to triggered instructions. A smart contract acts in a similar way to a traditional agreement but negates the necessity for the involvement of a third party. Smart contracts are capable of initiating their commands automatically, thus eliminating the involvement of a regulatory body. As a consequence of blockchain's immutable feature, smart contracts are developed in a manner that is distinct from traditional software. Once deployed to the blockchain, a smart contract cannot be modified or updated for security patches, thus encouraging developers to implement strong security strategies before deployment in order to avoid potential exploitation at a later time. However, the most recent dreadful attacks and the multifarious existing vulnerabilities which result as a consequence of the absence of security patches have challenged the sustainability of this technology. Attacks such as the Decentralized Autonomous Organization (DAO) attack and the Parity Wallet hack have cost millions of dollars simply as a consequence of naïve bugs in the smart contract code. In this paper, we classify blockchain exploitation techniques into 4 categories based on the attack rationale; attacking consensus protocols, bugs in the smart contract, malware running in the operating system, and fraudulent users. We then focus on smart contract vulnerabilities, analyzing the 7 most important attack techniques to determine the real impact on smart contract technology. We reveal that even adopting the 10 most widely used tools to detect smart contract vulnerabilities, these still contain known vulnerabilities, providing a dangerously false sense of security. We conclude the paper with a discussion about recommendations and future research lines to progress towards a secure smart contract solution.
We report our experience in the formal verification of the deposit smart contract, whose correctness is critical for the security of Ethereum 2.0, a new Proof-of-Stake protocol for the Ethereum blockchain. The deposit contract implements an incremental Merkle tree algorithm whose correctness is highly nontrivial, and had not been proved before. We have verified the correctness of the compiled bytecode of the deposit contract to avoid the need to trust the underlying compiler. We found several critical issues of the deposit contract during the verification process, some of which were due to subtle hidden bugs of the compiler.
Ethereum is a kind of blockchain platform where developers may develop and run programs called smart contracts. It inherently relies on gas consumption within a specified allowance to constrain code execution, making every instruction along an execution path to be a location for raising an exception. In this paper, we present GasFuzzer, the first work in exploring the effects of gas allowance manipulation to expose gas-oriented exception security vulnerabilities. GasFuzzer consists of two phases. The first phase introduces a gas-greedy strategy to favor transactions having higher gas consumption for mutation to obtain test transactions with different gas consumptions. The second phase introduces a novel notion of fractional gas consumption coverage and a novel gas-leveling strategy. It applies them to mutate the gas allowances of some of these transactions resulting in the highest gas consumptions produced in the first phase followed by applying these allowance-mutated transactions together with those which remained non-mutated to fuzz test the smart contract. We report an evaluation of GasFuzzer via an experiment on 3170 real-world smart contracts deployed on the public Ethereum Blockchain between October 2017 and July 2019. The findings show that GasFuzzer with gas-greedy strategy can detect more Exceptions Disorder kind of security vulnerabilities (7 more cases) than the previous state-of-the-art black-box fuzzer, and GasFuzzer with gas-leveling strategy and gas coverage criterion can detect 6 additional cases of Exceptions Disorder security vulnerabilities, which is significant.
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.
Xiao Liang Yu, Omar I. Al-Bataineh, David Lo, Abhik Roychoudhury
Smart contracts are automated or self-enforcing contracts that can be used to exchange assets without having to place trust in third parties. Many commercial transactions use smart contracts due to their potential benefits in terms of secure peer-to-peer transactions independent of external parties. Experience shows that many commonly used smart contracts are vulnerable to serious malicious attacks, which may enable attackers to steal valuable assets of involving parties. There is, therefore, a need to apply analysis and automated repair techniques to detect and repair bugs in smart contracts before being deployed. In this work, we present the first general-purpose automated smart contract repair approach that is also gas-aware. Our repair method is search-based and searches among mutations of the buggy contract. Our method also considers the gas usage of the candidate patches by leveraging our novel notion of gas dominance relationship . We have made our smart contract repair tool SCRepair available open-source, for investigation by the wider community.
Smart contracts are appealing because they are self-executing business agreements between parties with the predefined and immutable obligations and rights. However, as with all software, smart contracts may contain vulnerabilities because of design flaws, which may be exploited by one of the parties to defraud the others. In this paper, we demonstrate a systematic approach to building secure design models for smart contracts using formal methods. To build the secure models, we first model the behaviors of participating parties as state machines, and then, we model the predefined obligations and rights of contracts, which specify the interactions among state machines for achieving the business goal. After that, we illustrate executable secure model design patterns in TLA+ (Temporal Logic of Actions) to against well-known smart contract vulnerabilities in terms of state machines and obligations and rights at the design level. These vulnerabilities are found in Ethereum contracts, including Call to the unknown, Gasless send, Reentrancy, Lost in the transfer, and Unpredictable state. The resultant TLA+ specifications are called secure models. We illustrate our approach to detect the vulnerabilities using a real-estate contract example at the design level.
Jonathan Myers, Leonardo Babun, Edward Yao, Sarah C. Helble · 5 authors
In the Internet of Things (IoT), applications hosted on resource-limited devices interact with the user and the physical world to provide digital connectivity and automation to daily activities, and frequently provide a point of entry into networks. However, many IoT applications are vulnerable to cyber attacks that can put networks, data, and connected devices at risk. Integrity measurement is an active defense technique used to detect malicious modification of software at runtime. While its usefulness has been well-demonstrated, integrity measurement is application-dependent and requires domain knowledge of the targeted software. Currently, adding integrity measurement to a platform requires substantial human effort, and thus application has been limited to usage on widely-deployed software such as the Linux kernel. Due to the diversity of IoT, vendors are unlikely to devote a substantial amount of effort to add integrity measurement systems to their devices. In this paper we introduce MAD- IOT (Memory Anomaly Detection for the Internet of Things), an integrity measurement framework for IoT. In order to provide low-cost integrity measurement agents and software anomaly detection for IoT platforms, MAD-IOT uses a process called IMAGE: Integrity Measurement Agent GEneration. The IMAGE process uses machine learning to automatically generate integrity measurement agents for arbitrary IoT devices. We demonstrated MAD-IOT and IMAGE on a proof-of-concept testbed and evaluated its performance with supervised and unsupervised machine learning models. Our results indicate that IMAGE is highly effective in recognizing known forms of misbehavior on IoT app operations, and very promising in identifying zero-day attacks. Finally, MAD-IOT introduces minimal overhead, making it feasible to implement on systems with very limited resources.