Finally, we do not concur with the view, put forward by Bartoletti et al. (2024), that “transfer […] failing would make most contracts illiquid”. Contracts can be programmed in such a way that they are resilient against failing transfers. This article describes a method showing whether or not a contract implementation achieves resilience against failing transfers.
This section gives the background necessary to fully appreciate the rest of the paper. First a brief overview of Ethereum Smart Contracts and the programming language Solidity is given. This is followed by a description of the EFSM modeling formalism used for verification.
3.1 Smart contracts: Ethereum and Solidity
The first, and still major, blockchain framework for smart contracts is Ethereum (Wood 2023), with its built-in cryptocurrency Ether. Ethereum smart contracts can be thought of as objects, with fields making up the state space of the contract, and code offering functionalities to callers of the contract. In order to get a first impression, we suggest to glance at Fig. 2, showing an example contract with fields , , , , , and . The functions, here , , , and , offer functionality to callers of the contract. We will return to the details of the contract language, as well as this concrete contract, later on.
In Ethereum, every user and every contract has a unique address. Every address (user or contract) has an Ether balance, and can receive and send Ether in any direction (user to user, user to contract, contract to user, contract to contract). In contrast to user addresses, contract addresses have the additional feature of code being assigned to them, which is executed once the contract is called (by a user or by another contract). The executable code is stored on the blockchain in the form of EVM (Ethereum Virtual Machine) bytecode.
Contract execution in Ethereum features a transaction mechanism. Every call starts a transaction which is either completed successfully, or reverted if not successful. In the latter case, all effects so far, like Ether transfer or changes to fields, are undone. An unsuccessful transaction may revert for various reasons, like for instance running out of gas (see below), sending of unbacked funds, a failing runtime assertion, a statement in the code, a reverting call to another contract, or a reverting transfer, see below.
Ethereum miners look for transaction requests on the network. A transaction request contains the address of the contract to be called, the call data, and the amount of Ether to be sent. Miners execute the transaction requests locally on an EVM, one by one, in a fully sequential manner. Miners are paid for their efforts with units of Ether-prised gas, to be paid by the address that requested the transaction. A miner logs the transaction requests they executed, together with the respective effects of the transaction (Ether transfers and field value changes). When the log reaches a certain size, it is packaged by the miner as a new block, and suggested as the next block of the Ethereum blockchain. A consensus algorithm among other miners in the Ethereum network will then check whether the transactions and the effects reported in the block are in synch (by recomputing all effects and voting on the results). Once consensus is reached, the block is committed as the next block of the blockchain.
The by far most popular programming language for Ethereum smart contracts is Solidity. Accordingly, we target Solidity smart contracts in this work. Data types include (unsigned integer), (addresses of users and contracts), enums, structs, arrays, and mappings associating keys with values. For instance, the declaration declares a field which contains a mapping from addresses to unsigned integers. Fields marked are read-public, not write-public. In general, fields of a contract can only ever be modified by code of the same contract. Solidity offers also some cryptographic primitives, for instance the function computing a crypto-hash of its argument. The statement checks the boolean expression b, and reverts if b is false. If reverts, the entire transaction (function execution) reverts. The same is true for any other potentially reverting statement, like also , see below. The current caller, and the amount of Ether sent with the call, are always available via and , respectively. The default unit used for Ether balance and Ether payments is Wei (= (10^{-18}) Ether). Units can also be made explicit (like or ). Only functions accept payments.
Solidity further features programmable, potentially parameterised, modifiers. For instance, the Casino contract in Fig. 2 uses the modifiers , , and . They are implemented in the contract but their declarations are omitted from Fig. 2 for brevity. These modifiers expand to, respectively: The Solidity operations triggering payments and calls deserve special attention as they offer an attack surface addressed in this work. First of all, sending Ether to another contract, and calling another contract, is basically the same mechanism in Ethereum. In particular, sending Ether to an address passes control to the receiver (if the receiver is a contract). This can have problematic consequences of various kinds. One problem that is studied widely in the literature is re-entrancy, where the receiver of a call or payment calls back before returning. This can jeopardize the programmer’s attempt to fully reflect the external flow of Ether in the values of the internal fields. The problem of re-entrancy is addressed in other works, see for instance (Ahrendt and Bubel 2020). A different problem of control-passing calls and payments, in combination with the transaction concept, is unwanted effects of reverting calls and payments. This problem is much less discussed in the literature, and indeed the target of our work.
If an ongoing transaction executes a call or payment to another contract, this opens a nested transaction. Whether a revert in the nested transaction also reverts the outer transaction depends on the programming construct being used. The standard call statement (where c is a contract address and is a function of c) reverts if execution in c reverts. In contrast, the low-level call statement does not revert if execution in c reverts, but returns in that case. For payments, there is a similar distinction. The statement transfers the amount of v Wei from the caller to a. It reverts if a is a contract and the code of a reverts during execution of the transfer. In contrast, the statement does not revert if execution in a reverts, but returns in that case.
This means that the reverting of one’s own contract code is in the hands of an external party whenever we use statements like or , and can lead to a DoS of our contract to its users. To be clear, reverting of code does not have to result in a DoS. It is precisely the aim of this work to analyse whether or not an externally caused revert leads to a DoS.
3.2 Extended finite state machines
Extended finite-state machines (EFSM) (Cheng and Krishnakumar 1993; Skoldstam et al. 2007) extend finite-state machines (FSMs) with bounded, discrete variables, and guard and action expressions, collectively called updates, associated to the transitions. The guards and actions are formulas constructed from variables, integer constants, the Boolean literals (textrm{true }) ((textbf{T})) and (textrm{false }) ((textbf{F})), and the usual arithmetic and logic connectives. A guard is a predicate for the transition, which when true allows the transition to occur. The action, if specified for a transition, then updates the variables of the action.
A variable v takes values within a bounded discrete domain ({mathcal {D}}(v)), and has an initial value (v^{circ } in {mathcal {D}}(v)). Let (V ={v_0,ldots , v_n}) be the set of variables with domain ({mathcal {D}}(V) = {mathcal {D}}(v_0) times dots times {mathcal {D}}(v_n)). An element of ({mathcal {D}}(V)) is called a valuation and is denoted by (hat{v} = langle hat{v}_0, ldots , hat{v}_nrangle) with (hat{v}_i in {mathcal {D}}(v_i)), and the value associated to variable (v_iin V) is denoted (hat{v}[v_i]=hat{v}_i). The initial valuation is (v^{circ }=langle v_0^{circ }, ldots , v_n^{circ }rangle).
A second set of variables, called post-transition variables, denoted by (V’ = {, v’ mid v in V ,}) with ({mathcal {D}}(V’) = {mathcal {D}}(V)), is used to describe the values of the variables after a transition occurs. Variables in V are referred to as pre-transition variables to differentiate them from the post-transition variables in (V’). The set of all update formulas using variables in V and (V’) is denoted by (Pi _V).
For an update (p in Pi _V), the terms (text {vars}(p)) and (text {vars}'(p)) denote the set of all variables, and the set of post-transition variables, respectively, that occur in p. Updates (p in Pi _V) can thus be interpreted as predicates over their variables, evaluating to (textbf{T}) or (textbf{F}), i.e., (p :{mathcal {D}}(V)times {mathcal {D}}(V’) rightarrow {textbf{T},textbf{F}}).
Definition 1
An extended finite-state machine (EFSM) is a tuple (E = langle Sigma , S, S^{circ }, rightarrow , S^{omega } rangle), where (Sigma) is a set of events; S is a finite set of locations; (rightarrow, subseteq S times Sigma times Pi _{V} times S) is the conditional transition relation; (S^{circ } subseteq S) is the set of initial locations; and (S^{omega } subseteq S) is the set of marked locations.
A transition in E is given as (q overset{sigma :p}{longrightarrow } q’), which means that if update p evaluates to (textbf{T}), the system can transit from location q to location (q’) on the occurrence of the event (sigma). When the transition occurs the variables in (text {vars}'(p)) are updated while the variables not contained in (text {vars}'(p)) are unchanged.
EFSMs can be represented as directed graphs with nodes representing locations and arrows representing transitions. Events, guards and actions associated with a transition are represented by labels and expressions on the transition. In guards, the post-transition value of a variable is denoted by a prime, while the pre-transition value is un-primed. For instance, in Fig. 1, where ({texttt {S0, S1, S2, S3, S4, S5, S6, S7}}) is the set of locations, all marked as denoted by the filled circles, with ({texttt {S0}}) the initial location (shown by the small arrow), the transition ({texttt {S1}}) to ({texttt {S2}}) is labelled by the event placeBet2, and is guarded by the expression (_guess’ == HEADS | _guess’ == TAILS), which non-deterministically assigns HEADS or TAILS to the _guess variable. Thus, after the transition, in location ({texttt {S2}}), the value of _guess is either HEADS or TAILS.
Typically, EFSM models consist of several interacting components. Such a model is called an EFSM system, a collection of interacting EFSMs, (mathord {mathcal {E}} = { E_1, ldots , E_n}).
Component interaction in an EFSM system is modeled by synchronous composition (Hoare 1985), where shared events, that is, events that appear in more than one component EFSM, are lock-step synchronized, while other events are interleaved. A shared event is thus enabled in the composition if and only if it is enabled by all the EFSM containing that event in their alphabet. Furthermore, updates of transitions labeled by shared events are combined by conjunction.
Definition 2
Given two EFSMs (E_{1} = langle Sigma _{1}, S_{1}, S_{1}^{circ }, rightarrow _{1}, S_{1}^{omega } rangle) and (E_{2} = langle Sigma _{2}, S_{2}, S_{2}^{circ }, rightarrow _{2}, S_{2}^{omega } rangle), the synchronous composition of (E_1) and (E_2) is (E_{1} Vert E_2 = langle Sigma _{1} cup Sigma _{2}, S_{1} times S_{2}, rightarrow , S_{1}^{circ } times S_{2}^{circ }, S_{1}^{omega } times S_{2}^{omega } rangle), where:
Note that synchronous composition is associative.
For example, the event placeBet1 of Fig. 1 synchronizes with the same label in the EFSMs modeling the modifier shown in Fig. 8, right, and the assignSender of Fig. 9, so that the transition from S0 to S1 in Fig. 1 cannot occur unless is different from the (as required by Fig. 1), and (as required by Fig. 8), and assignSender is in its S0 location (see Fig. 9).
The global behavior of an EFSM system (mathord {mathcal {E}}={E_1, ldots , E_n}) is given by (E_1 Vert cdots Vert E_n).
Non-blocking of an EFSM system, is defined on the flattened system (Mohajerani et al. 2016), where the EFSMs and the variables have been converted into ordinary FSMs. For EFSMs each location becomes one state and the transitions are labeled by their respective events, but for variables this is more involved. Essentially each value that may be assigned to a variable is represented by an explicit state with transitions between these states corresponding to the updates (Mohajerani et al. 2016).
Definition 3
Let (E = langle Sigma , S, S^{circ }, rightarrow , S^{omega } rangle) be an EFSM with variable set (text {vars}(E)=V). The monolithic flattening of E is (U(E) = langle Sigma , S_{U}, rightarrow _{U}, S_{U}^{circ }, S_{U}^{omega } rangle) where
* (Q_U = Qtimes {mathcal {D}}(V));
* ((x,hat{v})overset{sigma ,}{rightarrow }_U(y,hat{w})) if E contains a transition (x overset{sigma :p,}{longrightarrow } y) such that (p(hat{v},hat{w}) = textbf{T});
* (Q{^circ }_U = Q{^circ }times {v{^circ }});
* (Q^omega _U = Q^omega times {mathcal {D}}(V)).
U(E) is the FSM representation of the EFSM, where all the values (hat{v}) of all the variables v have been embedded into the state set (Q_U). This ensures the correct sequencing of transitions in the FSM. The monolithic flattened EFSM system (mathord {mathcal {E}}) is denoted (U(mathord {mathcal {E}}) = U(E_1 Vert ldots Vert E_n)). Non-blocking for an EFSM system can be defined in multiple ways, for instance, based soleley on marked locations or also considering marked variables. In this work, we define non-blocking for an EFSM system considering both marked locations and marked variables which is equivalent to (U(mathord {mathcal {E}})) being non-blocking;
Definition 4
An EFSM system (mathord {mathcal {E}}) is non-blocking if (U(mathord {mathcal {E}})) is non-blocking.
So, the task of determining whether an EFSM system is non-blocking or not boils down to determining whether the synchronous composition of the flattened system can always reach some marked state. Though non-blocking verification is performed on the underlying flattened FSM, so that EFSM is just an intermediate representation between the Solidity source code and the FSM, there are benefits of using EFSMs. One benefit is the model compactness that comes from allowing bounded, discrete variables; for example, the FSM model of a variable with a 0..255 domain has 256 states, whereas in the EFSM formalism this can be a single variable with just that domain. Also, EFSMs allow to associate guards and actions to transitions, which aligns closely with the source code, making it easier to interpret counterexamples on the original source code.
In general, verifying non-blocking is computationally hard, but there exist tools that can perform this for systems of considerable sizes as measured by the number of states and transitions. One such tool is Supremica (Akesson et al. 2006).
3.3 Supremica
Supremica (Akesson et al. 2006) is a tool for synthesis, simulation, and verification of discrete event systems. Efficient algorithms for assessing and guaranteeing well-known SCT properties such as controllability and non-blocking are implemented in Supremica. In this paper, the compositional abstraction-based non-blocking (Malik et al. 2023) verification algorithm is used. Non-blocking is a progress property that, when fulfilled, guarantees that some significant marked state(s) of the system can always be reached. In the context of this paper, this aims to guarantee the ability of models of smart contracts to always be able to reach some state where certain properties hold, such as being able to pay out the funds held by the contract.
A benfit of using Supremica is that the flattening of the EFSM model is fully automatic, using partial unfolding (Mohajerani et al. 2013) which results in an FSM model structure beneficial for the verification procedure, thus potentially allowing to verify larger contracts within reasonable time and memory limits.
To verify non-blocking, conflict check (Mohajerani et al. 2016; Malik et al. 2023) of Supremica is used. If the verification determines that the system is blocking, a counterexample is provided, a trace that leads to a blocking state, that is, a state from where no marked state can be reached. This counterexample may be replayed in Supremica’s simulator to reveal the core of the problem.
