Verifying Ethereum-flavored Wasm (Ewasm) Code

by Rikard Hjort and Stephen Skeirik

Welcome to the final installment in the series on formal verification brought to you by Runtime Verification and dlab. If you missed the first three parts, you can find them here:

• Introducing KWasm, and an intro to symbolic execution
• An intro to Formal Verification using WebAssembly (Wasm)
• Verifying a more complex Wasm function

This time around, we’ll be picking up the baton right where we left off as we explore how to verify programs written in Ethereum-flavored Wasm, or Ewasm. In particular, we are going to verify a function for querying the balance of an ERC20-type smart contract.

Ewasm is part of the Ethereum 2.0 roadmap. We expect to see people starting to write prototype smart contracts in Ewasm soon, and later real smart contracts, handling real money. There are other blockchains already using Wasm as a smart contract language, and even as a client language, for example by writing smart contracts in Rust. Wasm smart contracts are coming, and we are preparing our Wasm verification tools to be more powerful. And, we want to show you how to use them, and what features we are adding as we go along.

ERC20 and the balanceOf function

ERC (Ethereum Request for Comments) documents propose and define new applications/standards to be built on top of Ethereum. The ERC20 is one such proposal which defines a generic smart token API (defined as an instance of a smart contract that exports particular functions) built on top of the Ethereum blockchain. Even more advanced token APIs, such as ERC-721, are subtypes of it.

Every ERC20 contract has a balanceOf function.

function balanceOf(address _owner) external view returns (uint256 balance)

Recall from our previous post, we are verifying a handwritten “WRC20”, i.e. a ERC20 contract written in Ethereum-flavored WebAssembly (Ewasm). You can find the full contract here.

In plain English, this function does the following:

1. Checks that the Ewasm smart contract call-data is 24 bytes long (4 byte selector + 20 byte address)
2. If it is not, revert (i.e., undo all smart contract changes to memory and return)
3. Load 20 bytes starting at byte 4 from the contract call data into memory locations 0–19. Load a value from the contract storage (a 32 byte -> 32 byte map), using the 32 first memory bytes as key and store the result in bytes 32–63 of memory.
4. Return bytes 32–39 of memory to the smart contract caller.

Here’s a visualization of the Wasm memory layout after this function terminates. The ERC20 token account address is stored in the first 20 bytes of memory while the balance (encoded as a big-endian number) of that address is stored in bytes 32–39. All other bytes are zeroed out.

-----address--------000000000000--bal---000000000000000000000000 ...

Note that this function does not perform any arithmetic; it only looks up a value in the contract storage and returns it to the contract caller. Since integers in Ethereum are stored in big-endian format, and Wasm stores them in little-endian format, the order of bytes appearing in the value bal in Wasm memory is the opposite of how Wasm would store such an integer. If we were to load it into an 64-bit Wasm integer on the value stack, we would have to reverse the bytes (using the function we verified last time) in order to perform any arithmetic operations. For this particular contract call that won’t be necessary.

Verifying the do_balance function

The task at hand is to verify some possible invocation of this function. Those that come to mind are:

• If the call-data is not 24 bytes long, then the function reverts
• If the call-data is 24 bytes long and;

a. the ERC20 account address has a balance stored in the contract storage, then the balance is returned, OR;

b. the ERC20 account address does not have a balance stored in the contract storage, then the balance 0 is returned.

We will verify the results of specifically calling the do_balance function from inside the contract, instead of verifying the call to the WRC20 contract itself. This proof can then be composed with others to obtain a proof that the contract as a whole behaves correctly when invoked through some Ethereum transaction.

Extending KWasm to KEwasm

However, one issue remains. Within the body of the do_balance function are calls to a few other functions we have not yet defined. These are actually so-called “host functions” of Ewasm: they pass control outside of the Wasm interpreter to an Ethereum client. We already have a pure Wasm semantics, but it does not include these host functions. That means we need to build a new semantics — KEwasm.

Ewasm really consists of two parts: a subset of Wasm, and a host module. By “a subset of Wasm,” we mean that certain operations are forbidden. By “a host module,” we mean that an Ewasm contract can import a handful of special functions that break out of the Wasm sandbox and interact with the external Ethereum environment. Here is an example of how Ewasm host functions are imported into a Wasm module:

(func $storageLoad (import "ethereum" "storageLoad") (param i32 i32))

Imports provide a way for a Wasm code module to access external functions. This still leaves the matter of providing a semantics for these host functions. We already have a pure Wasm semantics as well as a semantics for a generic Ethereum client, called the “Ethereum Environment Interface” (EEI). Luckily for us, K lets us take two semantics and combine them into one, by combining their respective semantic configurations into one, like so:

The first two cells are the top level cells of the EEI semantics configuration and the Wasm semantics configuration respectively. By importing them, all semantic rules defined over them are imported as well. Now all we need to do is define the bridge between Wasm and the EEI.

For that purpose, we introduce a third cell. It’s a simple stack used to pass integer values to the EEI from Wasm. Ethereum operates on 32 byte words, whereas Wasm uses 1 byte words and integer sizes of 4 or 8 bytes. That means parameters and results cannot be passed directly between Wasm and the EEI. The Ewasm designers solved this problem by having the host functions make use of Wasm memory, similar to how registers and a stack are used in CPU calling conventions. When calling storageLoad, for example, we specify which 32 bytes of memory represent the key we are loading, and which 32 bytes of memory we want the result stored in. Therefore, storageLoad takes two i32 parameters, pointing to two memory locations.

To bridge the two semantics we introduce some special commands for host calls. Whenever the Wasm execution encounters the host call eei.storageLoad, for example, the 32 byte parameter is gathered from memory and put on the <paramStack> cell. Then control is passed to the EEI, and on the <k> cell of the Wasm semantics we put a #waiting(eei.storageLoad). When the EEI is done executing, it will put whatever result it produced in its <eeiK> cell in the form #result(eei.VALUE). At this point, control is returned to Wasm, which stores the result of the call into the correct memory location. Here are the rules that define the bridge for the storageLoad function.

revert and finish do not return control to the Wasm execution. Reverting in Ethereum means undoing all state changes made by the transaction, while still consuming all the gas. Finishing in Ethereum means committing the changes the transaction has made. Both functions can return bytes. In the case of the balance function, finish returns the 8 bytes representing the queried balance.

Interactive proving with kore-repl

The new Haskell backend for K comes with a wonderful tool that makes proving more interactive and intuitive: the kore-repl. It allows us to take steps along a proving path, observing the state, easily explore different branches, visualize the possible execution paths and see what rules are being applied at each step.

To set up our current proof, for example, we first set up a proof using the entire WRC20 contract. We then run it up to the point where the do_balance function has been called. We copy that state into our claim, and make that our initial state. The execution up to that point is mostly straightforward. From there, we start proving the expected behavior of the do_balance function.

One helpful feature of the REPL is the graphing tool. This presents a visual overview of the execution, showing where the prover branched, and on which branches the proof is complete.

This image can be obtained by running the proof with the following commands:

Here the prover gets stuck, which means we need to inspect the state, which we can do with the konfig command, which prints the current configuration state, and all side conditions, both initial and those that have been gathered along the way by either proving sequents, or making an assumption when branching.

Overcoming proof obstacles via adding lemmas

The first issue we run into is that the proof proceeds very, very slowly. On our first run of the proof we found that certain steps took up to 30 minutes. Closer inspection showed that this was due to the expansion of memory writes: the action of setting a range of memory is converted into a series of set operations on individual bytes. So something like #setRange(MEMORY, VALUE, START,2/*Number of bytes*/)would be converted into #set(#set(MEMORY, VALUE mod256, START), VALUE/256 mod 256, START+1. Since we were setting 32 bytes at a time, the expansion became unnecessarily slow when the prover had to reason about every step. Furthermore, simple programs will likely set a range of memory to store a variable there, and then get exactly that piece of memory later, when reading the variable. The do_balance function does this, but it also loads the 20 byte address into memory and then reads it as a 32 byte value when looking up the balance, and it loads a 32 byte balance into memory and returns it as an 8 byte value. In both instances, the value is read from and written to the same starting point, and we know certain things about the ranges of these values. So it is easier to write lemmas about #getRange(#setRange(...), ...) and #setRange(#getRange(...), ...) constructs directly than letting the prover churn for hours dealing with the more granular #get and #set functions.

Because of this we do something we generally avoid when proving things: we modify our semantics of Wasm. We modify it by restricting what the symbolic execution engine does. Specifically, we tell it to not expand #setRange. We can do so by adding the [concrete] annotation to the relevant rule, which means this rule should only apply when all the values are concrete, i.e not symbolic. When the values are concrete, they can be resolved easily, but when they are symbolic, things may become slow.

First we need a way to deal with reading the address from memory. The balance function loads the byte address, and then reads it as a 32 bit value. Since memory is little endian, we can add the following lemma:

So #getRange(#setRange(BM, 0, ADDRESS, 20), 0, 32) will change into #wrap(160, ADDRESS) +Int#getRange(BM, 20, 12) *Int...

We also add some lemmas that indicate that we can remove the wrapping operation (since we know the address is less than 160 bits) and get rid of the getRange on the right side of the addition. We also need to state that the byte map (the memory) was empty to begin with, otherwise there could have been some junk in it and it would not be safe to grab those extra bytes. All in all, that replaces #getRange(#setRange(BM, 0, ADDRESS, 20), 0, 32) with just ADDRESS.

We also add a lemma for the converse case, when the the accessed memory is already defined by a #setRange operation:

The input is encoded as bytes, so we also need a few lemmas to deal with symbolic bytes. The bytes are b”9993021a" +Bytes ADDRESS, and we add a side condition saying the address is exactly 20 bytes long. Loading the call-data uses a substring function that we give a few lemmas:

We state that the final return data should have the form Int2Bytes(8, BALANCE, LE), and that the contract storage has the form (Bytes2Int(ADDRESS, LE, Unsigned) |-> BALANCE:Int) CONTRACT_STORAGE, meaning that the function returns the byte representation, little endian, of the value stored in balances.

With these lemmas, and a few less interesting ones, the proof goes through.

Conclusion

To sum up, we have now formally verified one case of one public facing function of the WRC20, i.e., when the function is invoked properly and the ERC20 token account has a valid balance stored. The remaining cases — when the address has no balance stored, as well as the case when the call data is of the wrong size — are even simpler to verify. Next steps include using this proof as a lemma so that we can verify an entire Ethereum contract call as well as verifying the last function in the WRC20 contract. These next steps may require some fine-tuning of our K formal verification framework as well as several new lemmas. Together, these things all will improve KEwasm’s ability to reason about many kinds of programs and smart contracts.

That said, let’s step back for a moment to consider why we are doing in this first place. Formal verification is hard work; is it worth it? We believe it is. The discipline of formal verification ensures we describe our software system implementing our business logic with a sufficient level of detail. It ensures that we consider every possible situation our system might encounter. It provides the greatest possible assurance that our program will work as intended — which certainly gives peace of mind when our code is responsible for processing users’ hard-earned money.

The do_balance function only reads the state of the contract, so calling it won’t cause any catastrophic failures. Our proof does verify that the call doesn’t change contract state in any way, but that could be easily hand- or eye-ball verified. So what’s the point? One important benefit of verifying read-only functions is that we exactly specify their interface, and under what pre-conditions they are correct. For example, we have encoded that the stored balance must fit inside 8 bytes for the proof to go through, and that exactly 8 bytes are returned. If we verify another contract, say a DEX-style Ewasm contract, calling the WRC20, and that contract expects a 32 byte result, the pre- and post-conditions don’t match, the proof will fail. Or, if we want to verify a series of WRC20 contract interactions it would need to make sure that the do_transfer function can never modify the contract storage so that a balance can be larger than what fits in 8 bytes. Software has a tendency to break at the boundaries — between functions, contracts, systems — so this kind of verification, where we discover the implicit pre-conditions, is extremely important in practice.

Unfortunately, the fact that errors will happen isn’t mere speculation. Aggregators like the smart contract weakness repository and recent reports like this one from the Stanford Blockchain Conference 2020 show that smart contract bugs are still something we need to grapple with today.

We now conclude this series of blog posts about formal verification. We hope you learned a bit about what formal verification is, how to do it, and most importantly, why it is important for the health of the entire smart contract/blockchain ecosystem.

We have big plans for KWasm and are looking for new collaborators. It could be in the form of sponsorships, R&D fellowships, verification projects, education or development collaboration. If you are a blockchain project using Wasm, we should talk: send us an e-mail.

If you are interested in using KWasm yourself, want to help development, or if you have any questions whatsoever, you can find us on GitHub (KWasm is here, and KEwasm is here), Stack Overflow and our Riot channel. Don’t hesitate to drop by! Finally, if you are already using KWasm or just thinking about it — whether for your company, for a school project, or out of plain ol’ curiosity — please let us know! We’d love to help you build more secure, efficient, and reliable systems.

For more formal verification posts, follow Runtime Verification on Medium. And make sure to check out posts on other dlab-sponsored projects.