How Formal Verification Could Help to Prevent Gridlock Bug

Yet another smart contract bug

Recently, a hidden DoS bug (called Gridlock) was revealed in Edgeware's Lockdrop smart contract that has locked hundreds of millions of dollars worth of Ether. Because of this bug, Edgeware had to newly deploy the fixed version of the contract, and as a result, two Lockdrop contracts (old version and new version) currently live in parallel on mainnet. (This means that you can send a transaction to either of these contracts to lock your Ether, until the old one is attacked and becomes incapable.)

In this article, we will review the Gridlock bug and discuss how formal verification can help to prevent this type of bugs.

As nicely described in Neil McLaren's blog post, the bug originated from an incorrect (but very plausible) assumption that the balance of a newly created account is always zero.

To get into more detail, let's take a look at the following (simplified) code snippet of the original buggy contract:

function lock(...) {
  // Create ETH lock contract
  Lock lockAddr = (new Lock).value(msg.value)(...);
  // ensure lock contract has all ETH, or fail
  assert(address(lockAddr).balance == msg.value);
}

Essentially, the lock function creates a new Lock contract account with bypassing the amount of Ether received (i.e., msg.value), and ensures that the newly created account (lockAddr) has the balance of the bypassed amount of Ether.

Although it looks fine at first glance, this code works only when the newly created account has the zero balance, which is unfortunately not always the case. (What?!) This is because the address of a new account can be pre-computed, and thus a malicious user can send some Ether to it even before being created by the lock function. Once this happens, the assert statement will keep failing for any further lock function invocation, which means that the function will never be able to do what it is supposed to do, becoming entirely unusable.

(Note that this behavior is specific to the EVM. The bug may not exist in different VMs that can identify nonexisting accounts and forbid them from receiving funds.)

Could formal verification help?

Now let us explain how the Gridlock bug could have been found by formal verification, especially one at the EVM bytecode level.

One of the essential processes of formal verification is to explore all possible behaviors of a given program (the EVM bytecode of the Lockdrop contract in this case) via symbolic execution. Here we use our KEVM verifier to symbolically execute the bytecode. To make a long story short, the symbolic execution of the above lock function bytecode will yield the following behaviors among others (e.g., function failures due to running out of gas).

1. Reverted (due to the new contract creation failure at line 3), if there already exists an account at the new account address, where the existing account's code is non-empty or its nonce is non-zero.
2. Reverted (due to the assertion failure at line 5), if there already exists an account at the new account address, where the existing account's code is empty, its nonce is zero, and its balance is non-zero.
3. Successfully terminated, if there already exists an account at the new account address, where the existing account's code is empty, its nonce is zero, and its balance is zero. (The storage of the existing account is cleared if it was non-empty.)
4. Successfully terminated, if there exists no account at the new account address.

(Note that the third and fourth behaviors require more conditions, e.g., no running out of gas, or enum-type arguments being given correctly, but we omit them here for simplicity.)

Once we have explored all possible behaviors of the contract, the next important step is to carefully examine each of those behaviors to ensure that it is intended or desired, and if not, it is hardly exploitable. Indeed, among the above four possible behaviors, only the fourth one is desired, and we need to analyze the others to check whether they are exploitable or not.

The first and the second behaviors, if exploitable, can be utilized for DoS attacks. However, to the best of our knowledge, the first behavior is hardly exploitable since it is cryptographically hard to create a contract account (i.e., an account with non-empty code) at a given specific address. (To do that using the CREATE2 opcode, one needs to find the salt that corresponds to the specific address, which is as hard as finding a preimage of the SHA3 hash.) The second behavior, however, is exploitable because one can easily initiate a non-contract account (i.e., an account with no code) at any specific address by simply sending some Ether to it, as we explained earlier.

On the other hand, the third behavior, if exploitable, could be utilized to drain others' "locked" Ether, which would be really fatal. However, to the best of our knowledge, it is hardly exploitable because of the similar reason to that of the first case. (One can easily "initiate" an account at a specific address, but it is hard to "own" the account, as it requires to find the secret key.)

To sum up, the symbolic execution of the lock function bytecode could have revealed the three undesirable behaviors, and close scrutiny of them could have found that one of them is exploitable for DoS attacks, fixing the Gridlock bug before deployment.

(If you are interested in learning more about how formal verification works, please take a look at our previous blog posts: "How Formal Verification of Smart Contracts Works" and "Formal Verification of ERC20 Contracts".)

Lessons (should be) learned

The EVM is often unintuitive.

The Gridlock bug originated from the incorrect understanding of some non-obvious part of the EVM design. Without reasoning about smart contracts at the EVM level, one could easily miss such EVM quirks, and similar bugs could be introduced again.

Formal verification can help.

Exploring all possible behaviors, especially at the EVM level, is not straightforward without employing principled approaches. Formal verification, in particular, its symbolic execution process, can systematically explore all possible behaviors of given smart contracts, which is much more rigorous than just manual code reviews.

Specifically, our KEVM verifier uses an exact specification of the EVM (a.k.a. KEVM), and will not let you get away with faulty assumptions. As seen above, it will find even the execution paths that are incredibly unlikely, such as the case when an attacker has found a pre-image of a hash and deployed their contract to the next address.

Formal verification is not a silver bullet.

Although formal verification guides us to systematically explore and rigorously reason about all possible behaviors of given programs, and indeed, is the ultimate way to find critical issues of the programs if any, it still requires significant manual effort, sometimes quite intellectually challenging. For example, even if we automatically found the three undesired behaviors of the lock function, we still needed to manually reason about their exploitability, which is non-trivial and requires security expertise. It is critical to ensure that no crucial details are missed in the manual reasoning process.

To learn more about our formal verification tools and techniques, please visit https://github.com/runtimeverification/verified-smart-contracts/.