Towards Property-Based Testing of Smart Contracts Using Gas Analysis

Property-Based Testing (PBT) [12] extends the classical testing paradigm to enable the specification of expected behaviors of code using a set of properties. Although the idea was proposed earlier, it is mainly known due to the QuickCheck [10] library implementation for the Haskell programming language. Over time, the same principles have been adopted in several other programming languages, including Erlang, Scala, Java, Python, and even smart contracts [21].

PBT occupies a useful middle ground between example-based unit testing and heavier-weight formal verification techniques [13]. This intermediate position is reflected in the way PBT is performed. In PBT, developers define formal specifications, called properties [13], that capture invariants or behavioral rules that a program should satisfy. For example, a property may specify that the balance of an account should never become negative, regardless of the sequence of operations applied to it. These properties are then automatically checked against a large number of inputs generated by randomized and structured generators [19, 20]. When a property violation is detected, testing frameworks typically report a counterexample, which is often minimized to a simpler failing input [10]. Such counterexamples provide concrete evidence of property violations and often offer valuable insight into the underlying causes of faulty behaviors. As a consequence, properties can be executed as specifications that both validate program behavior and document its intended semantics.

Because of having to systematically search over large input spaces, PBT has been observed to effectively discover corner cases which are less probable to be anticipated or manually expressed than other test cases [21]. This becomes even more significant when it concerns state transition behaviors, such as within smart contracts. Indeed, PBT is especially relevant in testing complex components and systems whose correctness depends on a sequence of operations [13]. Furthermore, when applied prior to verification, PBT aids in pointing out inconsistencies and errors in a system prior to start the verification process, which in turn lowers verification costs [9]. For instance, in the case of smart contracts, where vulnerabilities are widespread in complex execution paths as well as concurrent execution between contracts, traditional unit testing has been found inadequate by some studies. However, PBT has been successful in detecting vulnerabilities in smart contracts when paired with formal verification tools [17]. This naturally raises the question of whether PBT can be extended beyond functional correctness to also account for quantitative aspects of execution, such as resource usage and execution cost.

In this context, it is important to distinguish between functional properties, which describe the expected behavior of a program, and non-functional aspects, which concern quantitative characteristics of execution such as resource usage or cost [15]. In the context of blockchain applications, gas consumption represents a particularly relevant non-functional aspect.

Gas is a measure of the computational and persistent storage resources needed by a transaction to be executed on the Ethereum blockchain. The gas consumed by a function, invoked within a transaction, depends on the EVM opcodes it executes. The cost of each of the different opcodes is precisely specified by the Ethereum gas cost model [24, 2]. Those opcodes that are computationally more expensive or that access the replicated (persistent) storage consume more gas. For instance, storing a value to the persistent storage may consume up to 22,100 units of gas, while storing a value on the operational stack only consumes 3 units of gas. When executing a transaction, if the user provides less gas than the gas required to run the function invoked within the transaction, the execution is aborted and an out-of-gas exception is raised. Besides, the state is reverted and the user loses all gas provided. Hence, it is of utmost importance to have tools that are able to infer sound estimates on the gas consumption for each public function within a smart contract.

Gas analysis [5, 7] takes as input a smart contract and infers an upper bound for the gas consumed by its public functions. These upper bounds are parametric expressions defined in terms of the arguments of the function analyzed, the global contract variables and even certain blockchain information. Importantly, gas analyzers infer sound gas upper bounds, i.e., none execution of the public function will exceed the bound computed by the analysis. State-of-the-art gas analyzers [5, 7] compile the source level program into bytecode form and build a system of recurrence equations that define the gas consumption from the bytecode using the Ethereum cost model. After that, they use solvers [4, 22] to compute closed-form upper bounds from the recurrence equations. As an example, for a loop like for(uint i = 0; i < a; i++){ sum = sum + i; }, where a is an input parameter to the function, Gastap [5] infers 222+24276$\cdot$(a) as gas upper bound. While it is intuitive that the bound is linear on the value of a, the concrete constants that measure the cost of each iteration (24276) and the base case (222) require the understanding of the translation of the source level intructions into bytecode and also of the gas model of the opcodes. We refer to [5] for the technical details.

The complementary nature of PBT and static gas analysis lies in their different focuses. PBT aims to generate concrete executions that explore the various behaviours of a program, while static gas analysis aims to produce sound static characterizations of the gas consumption associated with a smart contract’s functions. The remainder of this section describes our approach to combine these two complementary techniques within an integrated testing framework. Specifically, PBT is intended to be used to generate test cases, while gas analysis is used to associate gas-related information with the generated tests, as we will illustrate along this section.

Smart contracts have different characteristics such as immutability, persistent state, and gas-limited execution, that make traditional testing techniques insufficient. In the last years, several tools [14, 3, 18, 8, 16, 6, 11, 23] and methods have been proposed to detect runtime errors, security vulnerabilities, and undesired behaviors. Several tools rely on property-based testing [14, 3, 16, 11]. These tools automatically generate inputs and transaction sequences to explore execution paths and find vulnerabilities. Examples include ContractFuzzer [16], Echidna [14], or Foundry [3] which allow specifying properties or invariants that must hold during execution. Although Echidna [14] and Foundry [3] allow gas consumption to be checked during the execution of test cases, they rely on executing concrete transactions on an EVM. As a result, gas is treated only at runtime, and these tools cannot exploit parametric information. SolAR [11] builds a test suite trying to maximize the path coverage. The generated test cases consist of concrete sequences of transactions executed on an EVM and do not check functional properties or reason about gas consumption. Method eth_estimateGas [1]
from Ethereum JSON-RPC API approximates the gas consumed by a transaction by performing an iterative binary search and simulating the transaction execution on the EVM. This simulation uses the blockchain state of the latest mined block. However, the gas inferred by this method may be imprecise, as the state of the blockchain can change between the time of estimation and the actual execution of the transaction.

Other approaches [18, 23] use symbolic execution and SMT solvers to reason about branch conditions and generate test cases where the executions are vulnerable. Mythril [18] and Solitor [23] identify security issues and control-flow errors. Mutation testing has also been applied to smart contracts [8, 6] to evaluate the quality of existing test suites. Tools like Deviant [8] introduce errors into the code and measure whether tests detect them. Other tools such as SuMo [6] define several mutation operators to modify the behavior of the contract and evaluate the quality of the code. However, they do not define any operator that takes into account the gas consumption of a smart contract.

As conclusion, we have proposed an integrated testing approach utilising both parametric gas bounds (inferred via static analysis) and automatically generated concrete test cases. Current testing approaches for smart contracts focus primarily on runtime gas usage, whereas we aim to systematically associate cost with a series of specific execution paths. By treating gas consumption as a first-class goal of testing, we are able to create a better basis for comparing equivalent but economically divergent execution paths. Future research will focus on implementing the gas-based testing framework following the proposed methods, as well as exploring its applicability to more complex smart contracts and their related costs.