Formal Verification of WETH

I traveled back to China a couple of weeks ago. It is a beautiful time after the application period, and it is nice to return to my homeland after one year at Wisconsin-Madison; it is worth a blog to talk about recent days, but… you know, sleep first.

What is a smart contract?

I hate to copy formal explanations from some books or Chatgpt; it is misleading and filled with new concepts that I fall into infinite DFS. I talked in my own words and made it as correct as possible. (TODO: what are blockchains?) Usually, I will treat a smart contract as a bank; it is introduced by some organizations, and people can deposit, withdraw, sell, buy, and do similar things, like holding a bank account in real life. An abstract contract offers functions and maintains key variables; imagine a bank offering services and keeping money safe and easy. For example, suppose a user wants to deposit $k$ tokens. In that case, he will create a new contract instance, which imports the abstract contract; to deposit, he should use some other things to send $k$ tokens to his address. He submits the contract (assigned with an address) to blockchain nodes(EVM); after several hours, the contract is admitted by most nodes and thus succeeds. A noticeable thing is that the smart contract can not be modified once uploaded and public to the blockchain, so keeping the contract safe and sound is essential.

How to make a smart contract safe?

For now, the method is reimplemented the contract behavior in SMT equations, then used the Z3 theorem prover certain facts about the symbolized contract. Using Bounded-Model-Checking (BMC), we find a path that can lead the initial state to an incorrect state (like allowing transfer while claiming a refund). It makes me feel like a big state machine, and what we do is graph searching.

Invariant 1: internal accounting correctness

variables:

balanceOf: $BalanceOf$, a mapping from adress to uint256, tokens give a specific address
totalSupply: $WethBalance$, uint256, total token stored in the contract
ethSupply: $EthSupply$, uint256, the total supply of tokens outside of our contract

state tuple:

$(BalanceOf, WethSupply, EthSupply)$

functions:

Following $(state,parameters)|condition\rightarrow NewState$
deposit: $$((BalanceOf,WethBalance,EthSupply),(MsgSender, MsgValue))|MsgValue\leq EthSupply \rightarrow (Store(BalanceOf, src, BalanceOf[src]+MsgValue), WethBalance+MsgValue, EthSupply-MsgValue)$$
withdraw: $$((BalanceOf,WethBalance,EthSupply),(MsgSender, wad))|wad\leq BalanceOf[MsgSender] \rightarrow (Store(BalanceOf, MsgSender, BalanceOf[MsgSender]), WethBalance-wad, EthSupply+wad)$$
transferFrom: $$((BalanceOf,WethBalance,EthSupply),(src,dst,wad))|wad\leq BalanceOf[src] \rightarrow (Store(x,dst,x[dst]+wad),WethBalance,EthSupply), where\ x=Store(BalanceOf,src,BalanceOf[src]-wad)$$
selfdestruct: $$((BalanceOf,WethBalance,EthSupply),(value))|value \leq eth_supply \rightarrow (BalanceOf,weth_balance+value,eth_supply-value)$$
fallback: same as deposit
coinbase: essentially same as fallback (overapproximation)
where $Store(M,K,V)$ donates a mapping identical to $M$ but with $M[A]$ set to $V$

initial state:

$(K(0),0,120000000e18)$, where $K(0)$ denotes the mapping with all entries initialized to 0

Constrained Horn Clauses

1. $State(K(0),0,0)$ should be False, it is impossible for all of the outstanging ETH supply to disappear. More formally, we can say that given some $s=(BalanceOf,WethBalance,EthSupply)$, then $State(BalanceOf,WethBalance,EthSupply)$ necessarily implies that $WethSupply+EthSupply$ is always equal to some constant.
2. We need the read total supply equals to computed total supply. We could formulate this invariant as: $$\forall s=(BalanceOf,WethBalance,EthSupply):State(BalanceOf,WethBalance,EthSupply)\rightarrow\sum_{a}BalanceOf[a]=WethSupply$$

CHC formulation of WETH’s state transition rules

1. after the constructor returns $State(K(0), 0, 120000000e18)=True$
2. For more concrete, we have $\forall(s,p):(State(s)\wedge Pre(p))\rightarrow State(Post(s,p))$, where $s$ is a state tuple, $p$ is a parameters tuple. $Pre(p)$ is a boolean function that represents the preconditions that the parameters $p$ are checked against, $Post(s,p)$ represents the updated state after the transition.
3. example for withdraw, $$\forall(BalanceOf,WethBalance,MsgSener,wad): (State(BalanceOf,WethBalance,EthSupply \wedge (wad\leq BalanceOf[MsgSender]) \wedge (WethBalance\leq wad)) \rightarrow State(Store(BalanceOf,MsgSender,BalanceOf[MsgSender]-wad), WethBalance-wad, EthSupply+wad))$$

encoding sums over arrays

We want to encoding $\sum BalanceOf=WethBalance$, we introduce an additional “synthetic” variable first, $SumBalanceOf$ tracks the value of this sum. We also introduce several tips to Z3

$$\forall (BalanceOf,WethBalance,MsgSender,wad,SumBalanceOf,address):(State(BalanceOf,WethBalance,EthSupply,SumBalanceOf) \wedge (BalanceOf[address] \leq SumBalanceOf)) \rightarrow (SumBalanceOf\leq 120000000e18) \wedge (BalanceOf[address]\leq 120000000e18)$$

analysis

Using Z3py, we consider following,

1. The starting state $(K((BitVec(160), 0), 0, 120000000e18,0))$ is assumed to be reachable, so therefore, it is reachable.
2. Asserted that if a state is reachable, we can also do a SELFDESTRUCT to the WETH contract to reach a new state. Therefore, the state $(K(0), 12884901888,119999999e18,0)$ is reachable.
3. We asserted that if a state is reachable, $WethBalance$ must equal to $SumBalanceOf$, but for now, this is not statisfiable.

It is a bug, albeit minor. To overcome it, we can assume that the total number of WETH tokens is always less than or equal to the native ETH balance of WETH.

Invariant 2: Solvency

We want to prove additionally that WETH is solvent, meaning that a WETH holder is always able to withdraw their eth after depositing.

symbolic execution of solidity

Example 1: WETH function approve

function approve(address guy, uint wad) public returns (bool) {
    allowance[msg.sender][guy] = wad;   // 1
    Approval(msg.sender, guy, wad);     // 2
    return true;                        // 3
}

We translate this function to a Z3py function

def approve(s, state, msg_sender, guy, wad):
    eth_balances, balanceOf, allowance = state

    # allowance[msg.sender][guy] = wad; (1)
    allowance = Store(allowance, msg_sender, Store(allowance[msg_sender], guy, wad))

    # Approval(msg.sender, guy, wad);   (2)
    # return true;                      (3)
    return (eth_balances, balanceOf, allowance)

Example 2: WETH function deposit

function deposit() public payable {
    balanceOf[msg.sender] += msg.value
    Deposit(msg.sender, msg.value);
}

Corresponding symbolic implementation

def deposit(s, state, msg_sender, msg_value):
    eth_balance, balanceOf, allowance = state

    # transfer of native eth, as per msg_value
    s.add(UGE(eth_balance[msg_sender], msg_value)) # UGE: unsigned greater than
    eth_balances = Store(eth_balances, msg_sender, eth_balances[msg_sender] - msg_value)
    eth_balances = Store(eth_balances, WETH_Address, eth_balances[WETH_Address] + msg_value)

    # balanceOf[msg_sender] += msg.value; (1)
    balanceOf = Store(balanceOf, msg_sender, balanceOf[msg_sender] + msg_value)

    # Deposit(msg.sender, msg_value); (2)

    return (eth_valanes, balanceOf, allowance)

Example 3: WETH function transferFrom

function transferFrom(address src, address dst, uint wad) public returns (bool)
{
    require(balanceOf[src] >= wad);                   // (1)

    if (src != msg.sender && allowance[src][msg.sender] != uint(-1)) { // (2)
        require(allowance[src][msg.sender] >= wad);   // (3)
        allowance[src][msg.sender] -= wad;            // (4)
    }

    balanceOf[src] -= wad;                            // (5)
    balanceOf[dst] += wad;                            // (6)

    Transfer(src, dst, wad);

    return true;
}

Tranfer to

def transferFrom(s, state, msg_sender, src, dst, wad):
    eth_balances, balanceOf, allowance = state

    # (1)
    s.add(UGE(balanceOf[src], wad))

    # (2)
    p = And(src != msg_sender, allowance[src][msg_sender] != Uint
    (0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))

    # (3)
    s.add(Implies(p, UGE(allowance[src][msg_sender], wad)))

    # (4)
    allowance = If(p,
        Store(allowance, src, Store(allowance[src], msg_sender, allowance[src][msg_sender] - wad)),
        allowance)

    # (5)
    balanceOf = Store(balanceOf, src, balanceOf[src]-wad)

    # (6)
    balanceOf = Store(balanceOf, dst, balanceOf[dst]+wad)

    return (eth_balances, balanceOf, allowance)

Proving solvency

1. Base case: fisrt, show that there exists some state that is solvent.
2. Inductive case: Given an arbitary solvent state (inductive hypothesis), show that state remains solvent after any single transaction made to WETH.

Base case:

Start with WETH’s initial state (the one where it’s empty) and deposit some money. In this state, we can take some money out, this can be improved by using specific user addresses with a simple unit test. To prove that it’s valid for all user addresses, we can sue symbolic execution.

Inductive case:

1. We model an arbitrary starting state simply with unconstrained variables. balanceOf is an unconstrained SMT Array mapping from address to uint256.
2. We model a specific, arbitrary user and their initial deposit as an unconstrained address and uint256.
3. We model an arbitary global EVM state, for our purpose, we only really need to model a global mapping of native eth account balances.

balanceOf = Array('balanceOf', AddressSort, UintSort)
allowance = Array('allowance', AddressSort, ArraySort(AddressSort, UintSort))

myUser = Const('myUser', AddressSort)
initialDeposit = Const('initialDeposit', UintSort)

eth_balances = Array('eth_balances', AddressSort, UintSort)

To prevent “nonsense” counterexamples, we have

1. myUser != WETH_Address: the user isn’t the WETH contract itself
2. ForAll([a], ULE(eth_balances[a], 120000000e18)): no Ethereum address has more eth than the total supply of eth

We also need to “help” z3 out by providing some additional theorems

1. an entry in an array can never exceed the sum of all entries, sum of all entries in $balanceOf$ is less than or equal to the total eth balance of WETH, thus, all entries in $balanceOf$ are less than the balance of WETH: ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
2. balanceOf = Store(balanceOf, myUser, Uint(0)): the user starts out with no WETH before their deposit.
3. ForAll([a], allowance[myUser][a] == 0): the user hasn’t approved anyone already.

Next, we construct our brand-new state, and update it by doing a symbolic deposit with our brand-new depositor:

state = (eth_balance, balanceOf, allowance)
state = deposit(s, state, myUser, initialDeposit)

Notice, we do not impose any other assumptions on our state, so the variables could be in any (sane) cofiguration