Formal Verification in Solidity and Move: Insights from a Comparative Analysis

As observed in Section 2, Move enforces asset integrity by ensuring that assets cannot be duplicated but only moved between owners; by contrast, Solidity – except that for native tokens (ETH) – requires the management of assets to be implemented at a contract level. For example, in the bank use case, the credits are rendered in Move as a map from address to Coin (that are the actual assets), while in Solidity they are a map from address to int. This means that the Solidity code merely tracks the assets deposited by each user. However, implementation bugs can lead to a mismatch between the assets controlled by the contract and the overall amount of user credits, assigning more or fewer credits than they are entitled to. This significantly impacts the specification and verification of properties. First of all, in MSL, since credits are assets, such properties are implied by properties that concern assets. For example, in MSL the specification of the property

bank/deposit-assets-credit: “after a successful deposit of $n$ tokens, the credits of the sender are increased by $n$”

is exactly a sub-specification of the property

bank/deposit-assets-transfer: “after a successful deposit of $n$ tokens, $n$ tokens pass from the control of the sender to the control of the contract.”

In CVL, by contrast, these two properties are disjoint, and it is possible – in the presence of bugs related to the handling of credits – for the former to hold while the latter is violated. This shows that, to cover the same set of properties, Solidity requires a greater number of specifications than Move. Moreover, in Move, certain properties concerning credits trivially hold, while, in Solidity, they may be hardly verifiable, or even unexpressible. For example:

bank/credits-leq-balance: “the assets controlled by the contract are (at least) equal to the sum of all the credits”

trivially holds in Move, where credits coincide with the deposited assets, but not in Solidity, where credits just represent the deposited assets. In general, verifying such kind of properties is quite challenging, as they require to reason about quantities depending on an unbounded number of users.

Most smart contracts implement access control mechanisms to ensure that certain actions can only be performed by certain users under certain conditions. A typical check is that some resources can only be updated by functions called by the contract owner. Move inherently supports this kind of check: it suffices that all the functions that update the resource borrow it through a signer address. This is because, in Move, a resource can only be referenced through the address of its resource owner. This is a security pattern in Move to reduce the risks of access control errors [3]. In Solidity, instead, resource ownership is not a native notion, so it must be encoded by the contract logic. In particular, in order to implement the check above, the contract must first record the owner address in a variable, and each sensitive function must require that the transaction sender and the owner coincide. Forgetting even a single check can lead to vulnerabilities, as in the Parity Wallet hack, where the absence of such check in a function enabled the attacker to become the owner and steal all the contract funds [24]. In our dataset this difference in behaviour can be observed, e.g., for the property

vault/finalize-revert: “a call to finalize() aborts if the sender is not the owner.”

In CVL, we need to explicitly check that the address of the sender is equal to the owner field, while, in MSL, since the function directly accesses the Vault struct owned by the sender, and the owner is not determined by the value of a variable but by the address that owns the resource, then the property trivially holds, being enforced by the language. Another typical check is that some addresses used by the contract (e.g., its owner) do not change throughout the contract lifespan (e.g., vault/owner-immutable). In Solidity, it is possible to enforce that by declaring the addresses as immutable. In such a case, the property is directly enforced by the Solidity compiler, without having to resort to verification. Enforcing the same check in Move is less straightforward. A method is to record the concerned addresses as fields of some struct, and then verify with the MVP that these fields are invariant.

Solidity and Move render assets and their transfers differently, leading to different techniques for expressing and verifying properties related to them. In Solidity, while there is a clear dichotomy in how the native asset (i.e., ETH) and user-defined assets (e.g., ERC20 tokens) are handled, in both cases transfers are rendered as contract calls. The outcome of a contract call depends on whether the callee is an externally owned account (EOA) or a contract account. When the callee is an EOA, the transfer is guaranteed to succeed, whereas for contract accounts the effect of the call depends on the implementation of the function handling the call. For instance, assets may be returned to the caller if the call reverts, or they may be forwarded (either in full or in part) to other accounts if the function is designed to do so and has enough gas. Therefore, properties about asset transfers should either discriminate between EOAs and contract accounts, or add assumptions about the implementation of the receiver function. However, the first choice is not always viable, as detecting whether an address is an EOA or a contract account (either at contract or specification level) is possible only in limited cases [25, 8]. The second choice is problematic as well, since if the assumptions are false then the property may be violated at runtime. Unlike Solidity, Move offers linguistic primitives for transferring ownership of resources, enabling a more disciplined modelling of asset transfers. This reduces the effort required to incorporate the necessary assumptions when encoding properties. In our dataset, we have observed this, e.g., in the property

vault/finalize-not-revert: “a finalize() transaction sent by the contract owner, in state REQ, and after the wait time has passed, does not abort”

which holds in Move but not in Solidity, since the transfer may fail when the receiver is a contract. Furthermore, also

vault/finalize-assets-transfer: “after a successful finalize(), a given amount of assets pass from the contract to the receiver”

holds in Move but not in Solidity since, if the receiver is a contract, the assets can immediately be transferred to another address through the fallback function.

Solidity features a form of dynamic dispatching, in that the compiler does not always know, for a contract-to-contract call, the code that will be executed in the callee. This poses significant challenges to verification. Indeed, to avoid unsoundness, verification tools must assume that contract-to-contract calls can execute arbitrary code, which easily leads to false negatives. In order to address the issue, Certora allows users to specify a set of possible implementations of the callee, and verify the caller against each of them [12]. This technique can require considerable effort, and does not resolve the underlying unsoundness issue. Move, on the other hand, features static dispatching, i.e. the compiler (and, consequently, the verifier) know exactly the code that will be executed in the callee. In particular, Move does not support inheritance nor any form of method redefinition. We have observed the impact of these different dispatching designs, e.g., in

price-bet/win-revert: “a win transaction aborts if the oracle exchange rate is smaller than the bet exchange rate.”

In Certora, verifying the property requires the user to explicitly instruct the verifier to resolve the call with a given oracle implementation: leaving that unspecified would make verification fail. In practice, many Solidity contracts are written in a way that makes it impossible to predict the actual implementations of the callees (e.g., Solidity contracts using ERC20-compatible tokens usually define only their interface).

Immutability. In Solidity, the immutable keyword allows to enforce that certain variables cannot change value throughout the whole lifespan of the contract, making certain properties (e.g., the above-mentioned vault/owner-immutable) enforced by the Solidity compiler. In Aptos Move, since an equivalent modifier does not seem to be available, such properties have to be explicitly verified with a prover.²²2Note that, in SUI Move, it is possible to define frozen objects (i.e. objects that cannot be modified nor moved). It does not seem possible to define frozen fields of an object, though.

Self-destruct. In Solidity, contracts can receive native tokens at any time through the self-destruct method. This requires additional precautions during implementation to prevent funds from getting locked in the contract. For example, our Solidity implementation of the bank use case allows users to withdraw only the funds corresponding to their credits (i.e., funds that have been previously deposited). In contrast, funds received via self-destruct cannot be withdrawn from the contract and remain locked. This is not the case in Move, as no equivalent of the self-destruct method exists. For example, the property

bank/no-frozen-assets: “if the contract controls some assets, then it is always possible to transfer them to some user”

holds in Move, but not in Solidity, since the contract only allows creditor to withdraw the assets they have deposited, but does not provide any function to transfer funds received via self-destruct, resulting in funds getting stuck in the contract.

As discussed in Section 3, the translation of properties written in natural language to formal specification often requires the addition of low-level technical assumptions. Here, we report the cases that we have observed in our experiments.

Accepting incoming transfers. As observed in the “Assets transfer” paragraph, properties concerning the transfer of assets may need further assumptions on the receiver. In Move, the only technical assumption we had to add in our dataset is that the CoinStore of the receiving address is not frozen. In Solidity, one sufficient condition that can be used when the receiver equals to the transaction sender is that the sender is an EOA. Although this could be encoded in CVL by requiring that e.msg.sender==e.tx.origin, the Certora prover does not use this additional assumption, leading to a false negative. This is the case, e.g., of:

bank/withdraw-assets-transfer: “after a successful withdraw(amount), exactly amount units of T pass from the control of the contract to that of the sender”

Other conditions, such as ensuring that the receiver does not fail or does not perform further calls, do not appear to be expressible in CVL.

Coin-to-FungibleAsset. Aptos has recently introduced a “Fungible Asset” (FA) standard [2] that extends the Coin standard, enabling automatic migration from Coin to FA by default. This automatic migration can make certain properties concerning the transfer of Coins violated, since Coins are not preserved (but migrated to FA). This is the case, e.g., of:

bank/deposit-revert: “a transaction deposit(amount) aborts if amount is greater than the T balance of the transaction sender.”

In order to verify such properties, it is necessary to disable the automatic migration.

Sender is not the contract. In Solidity, it is possible that a contract calls itself. In certain cases, it may be necessary to assume that this is not the case, as, otherwise, certain properties might either not hold, or be unverifiable in practice. For example, bank/deposit-assets-transfer specifies that, after a successfull deposit of $n$ tokens, the balance of the sender is decreased by $n$. While this property is true without further assumptions (since the specific Bank contract cannot call itself), in Certora the verification will fail without adding the assumption that the sender is not the contract. This is because verification tools usually over-approximate the set of possible executions, thus considering also the impossible case in which the contract calls itself.

We denote by “function spec” properties that specifically target a given function. We divide these properties into “success conditions”, which characterize the conditions under which a function aborts or not, and “post-conditions”, which express properties regarding the state after the call, assuming that the call has not aborted. The Move Prover has an ad-hoc specification format for function specs. In Certora, function specs can be expressed as rules that explicitly mention the function being called, and using requires statements for pre-conditions, the expression lastReverted for checking abort conditions, and the statement assert for post-conditions. Listing 3 and Listing 4 presented in Section 2.2 are examples of function specs in CVL and MSL, respectively. Both tools perform well over properties of this kind in our dataset.

We denote by “state invariants” properties of the form “for every reachable state $\mathrm{s}$, it holds that $\mathrm{P}(\mathrm{s})$”, where $\mathrm{P}(\mathrm{s})$ is a property that only mentions variables in the state $\mathrm{s}$. In Move, state invariants can be proved in two ways: either using a struct invariant spec, in case an invariant only deals with a single structure (e.g., in any state, the vault state is IDLE or REQ, i.e. vault/state-idle-req-inter), or, otherwise, using a global invariant spec (e.g., the owner and the recovery keys are distinct, i.e. vault/keys-distinct). In Certora, there is a common way to write invariants. Both tools perform well over properties of this kind on our dataset.

We denote by “single-transition invariants” properties of the form “for every reachable state $\mathrm{s}$, and for every transaction $\mathrm{T}$, either $\mathrm{T}$ aborts, or it holds that $\mathrm{P}(\mathrm{s},\mathrm{next}(\mathrm{s},\mathrm{T}),\mathrm{T})$”, where $\mathrm{next}(\mathrm{s},\mathrm{T})$ is the state after a successful execution of $\mathrm{T}$ in $\mathrm{s}$. Note that function specs are a special case where the called function is fixed. Certora is quite flexible for the verification of such properties, and allows to express arbitrary (quantifier-free) conditions on the parameters of $\mathrm{T}$. In the Move Prover, there are two different ways to express single-transition invariants, both of which are less general than Certora rules. The first way is to use global invariant updates. This construct, however, does not allow to make explicit mention of the parameters of the transaction $\mathrm{T}$, restricting expressible properties to those of the form $\mathrm{P}(\mathrm{s},\mathrm{next}(\mathrm{s},\mathrm{T}))$, where $\mathrm{T}$ remains implicitly universally quantified. The second way is to use a schema of function specs (that is, syntactic sugar to group together a set of function specs with a common body). Writing a single-transition invariant this way, however, requires to write an instance of the schema for each method, making the MSL spec significantly more verbose than in CVL. As an example, consider the property:

bank/assets-dec-onlyif-deposit: “if the assets of a user A are decreased after a transaction, then that transaction must be a deposit() where A is the sender”

In CVL, it is possible to succinctly express such property as follows:

In MSL, it is only be possible to specify the contrapositive, i.e. that, for every transaction that is not a deposit(), or for which A is not the sender, then the assets of A are not decreased. This, however, requires to write a spec for each function except deposit(), and one further function spec for the deposit(), restricted to the case of A not being the sender.

Note that, in the case bank had a greater number of functions, the size of the MSL specification would grow proportionally, while the CVL spec size would remain constant.

We denote by “multiple-transition invariants” properties of the form “for every reachable state $\mathrm{s}$, and for every sequence of transactions $\overrightarrow{T}={\mathrm{T}}_1\mathrm{\dots }{\mathrm{T}}_n$, either one transaction aborts, or $\mathrm{P}(\mathrm{s},\mathrm{next}(\mathrm{s},\overrightarrow{T}[1:1]),\mathrm{\dots },\mathrm{next}(\mathrm{s},\overrightarrow{T}[1:n]),{\mathrm{T}}_1\mathrm{\dots }{\mathrm{T}}_n)$ holds”, where $\mathrm{next}(\mathrm{s},\overrightarrow{T}[1:i])$ denotes the state after the successful execution of ${\mathrm{T}}_1,\mathrm{\dots },{\mathrm{T}}_i$. In CVL, it is possible to express such specifications analogously to single-transition invariants, by subsequent function calls in the same rule. In MSL, this kind of specifications does not seem to be expressible. For example, consider the property:

vault/finalize-or-cancel-twice-revert: “a finalize() or a cancel() transaction aborts if performed immediately after another finalize() or cancel() transaction.”

This is not expressible in MSL, while Certora can verify the following CVL spec:

These are properties that involve multiple finite sequences of transactions [14]. A typical class of metamorphic property are additivity properties: e.g.:

bank/deposit-additivity: “two successful deposit() of $n_1$ and $n_2$ units of token T performed by the same sender are equivalent to a single deposit() of $n_1+n_2$ units of T”

In CVL, it is possible to express some metamorphic properties through the use of storage types, which allow to record the contract storage at different points of execution and to later compare them (see, e.g. Listing 10). This feature is not present in MSL, so metamorphic properties do not seem expressible.

Some classes of properties do not seem expressible in any of the two tools. Without claiming exhaustivity, we now briefly discuss some of the classes we have encountered, with particular attention to those that seem addressable by other tools.

Liveness. Liveness properties have the form “eventually a state that satisfies certain conditions is reached”. In price-bet, a desirable liveness property is

price-bet/eventually-balance-zero: “eventually the contract balance goes to $0$”

Note that this property is closely related to, but more abstract than, the property

price-bet/timeout-not-revert: “a transaction timeout() [which transfers the assets controlled by the contract to the owner] does not revert if the deadline has passed”

Tools able to handle such kind of properties, usually under the assumption of fairness conditions (in the example, that the timeout() function is called at least once after the deadline), are VeriSolid [19], VeriMove [21], and SmartPulse [31].

Liquidity/Enabledness. Liquidity [7] or Enabledness [29] properties are of the form “in every reachable state, certain users are always able to fire a (fixed) number of transactions to reach a desirable state”. In bank, an example of such properties is

bank/no-frozen-credits: “if the credits are strictly positive, it is possible to reduce them”

Note that this kind of property never mentions the function that should be called nor its parameters, as they are existentially quantified and determining them (as a function of the current state) is a task of the tool. A tool that addresses such kind of properties is Solvent [7].

CTL fragment: The specification language of VeriSolid (and, consequently, of VeriMove) covers an expressive fragment of Computational Tree Logic (CTL). Such expressivity comes at the expenses of soundness, as the verification process relies on a certain level of abstraction. Examples of CTL specifications include the Liveness seen before, as well as properties of the form “${\mathrm{P}}_1$ cannot happen after ${\mathrm{P}}_2$”, or “If ${\mathrm{P}}_1$ happens, then ${\mathrm{P}}_2$ can only happen after ${\mathrm{P}}_3$ happens”. These properties cannot be expressed in CVL, since it is not possible to talk about unbounded sequences of method calls, but only about sequences of states of finite length. E.g., a property not expressible in CVL but in the CTL fragment supported by VeriSolid is:

vault/finalize-after-withdraw-not-revert: “after a successful withdraw(), if no cancel() or finalize() have been called successfully, then finalize() does not abort”

All these properties have a higher level of abstraction than those discussed in the previous paragraphs. Although some of these properties, in certain cases, can be reformulated in terms of more concrete properties that imply them, doing so requires a more advanced knowledge of the low-level aspects, and reduces their generality. It has been observed that properties that abstract the system have a better return-on-investment than low-level properties [38].

We finally address specific features of properties that can appear in all previous classes, hence for which a separate discussion is needed.

Inter vs. Intra function invariants Invariants can be of two kinds: those that must be preserved across function calls (inter-function invariants) and those that must be preserved within the execution of a function (intra-function invariants). In the latter, the notion of reachable state is extended to intermediate states. In some cases, intra-function invariants give stronger security guarantees. For example, consider the invariant

vault/keys-invariant-inter: “the receiver key cannot be changed after initialization”

Requiring this invariant to only hold inter-function is not enough, as it does not capture attacks where an adversary (i) changes the receiver key within finalize() before the transfer, (ii) sends the contract tokens to her address, and (iii) restores the key to the original value before the end of the function. It is necessary to require the invariant to hold also intra-function (vault/keys-invariant-intra). In Certora, verification of intra-function invariants is possible through ghost variables and hooks [10]. In Move, on the contrary, verification of intra-function invariants is, in general, not possible. The MVP can check that an invariant holds globally, i.e. every time the global state is updated [4], but this cannot capture every change that occurs during the execution of a function. In the example attack mentioned above, the MVP is not able to detect that that the receiver key is changed within the execution of the finalize().

Nested quantifiers. Several interesting properties require the nesting of quantifiers. In Certora, quantifier nesting is limited to exists-forall fragments, whereas forall-exists fragments are disallowed. This makes not expressible in CVL properties such as:

bank/exists-at-least-one-credit-change: “after a successful transaction, the credits of at least one account have changed”

Although MSL allows arbitrary combinations of quantifiers, in practice the verification of such properties can be problematic, as the underlying SMT solvers often struggle with quantifiers. In our experiments, we managed to successfully verify the previous property, but got an inconsistent result in the case of bank/exists-unique-asset-change. This inconsistency may be caused by the version of the underlying SMT solver used.

Gas. As discussed in “Assets transfer” in Section 4.1, the truth of certain properties may depend on the amount of gas available to the involved functions. For instance, in Solidity the ground truths of bank/withdraw-assets-transfer and vault/finalize-assets-transfer differ because of the functions used in the respective contracts to transfer ETH from the contract to another address: in the implementation of bank, we are using transfer, which do not carry enough gas to perform further calls, while in vault we are using call, which instead transfers all the gas to the callee. Certora however over-approximates the amount of gas available, so it gives a false negative for bank/withdraw-assets-transfer.