Abstract
Wrapped ETH, or
WETH,
is one of Ethereum’s most popular smart contracts. While WETH serves a
simple purpose, a significant portion of all Ethereum transactions
depend on it. WETH now underpins large parts of DeFi. In this blog post,
we prove critical safety guarantees and invariants within the WETH
contract. We do so by leveraging Z3, a battle-tested SMT solver.
We prove two critical invariants: (1) correctness of accounting, and (2)
solvency. For accounting, we prove that the total supply of WETH is
always equal to its balance of native Ether. For solvency, we prove
that, regardless of other users’ actions, a user is always able to
unstake Wrapped ETH. In the process, we also identified a minor,
harmless bug in the contract. Our work enables the community to continue
using WETH with increased confidence in its correctness.
Background
WETH is a straightforward token that wraps native Ether into the
ERC20-compatible WETH token. The contract allows anyone to deposit
native Ether for WETH tokens 1:1, or conversely, redeem WETH for native
Ether. The contract also supports the standard ERC20 functionality, like
approvals, transfers, totalSupply, and transferFrom.
WETH is useful because native Ether is inconvenient for use in smart
contracts. First, native Ether is not ERC20 compatible. This
necessitates additional code paths, increasing complexity. Not only does
this add developmental burdens, it increases the likelihood for security
vulnerabilities. Native Ether interactions also introduce the risk of
re-entrancy vulnerabilities, which are absent when dealing with ERC20
tokens. Hence, WETH has seen widespread adoption in DeFi applications,
like Uniswap, Compound, etc.
As of the time of writing, WETH has been involved in over 125 million
transactions[1].
On the entire Ethereum blockchain, there have been 1.7 billion
transactions so far. In other words, over 7% of all Ethereum
transactions involve Wrapped ETH. Furthermore, Wrapped ETH has become
more pervasive over time. In the past year, 48M of 420M Ethereum
transactions called WETH. This represents 11.5% of all Ethereum
transactions this year. Since WETH is heavily used in DeFi applications,
and DeFi has become a centerpiece of the Web3 ecosystem, this is a
natural outcome.
A smart contract bug in WETH would be deadly. Countless DeFi protocols
use WETH as as a compatibility layer for native ETH. For instance,
Uniswap relies on
WETH
internally when dealing with native ETH. Should WETH have a solvency or
accounting error, the downstream effects on DeFi would be massive. Not
only would WETH holders be affected, so would all of the DeFi protocols
which are hardcoded to use WETH internally.
The WETH contract itself is relatively simple. Excluding blank lines and
comments, WETH9 is comprised of only 51 lines of code in total.
Excluding getters, there are only 7 functions, and each of these
functions are relatively simple. That being said, simplicity is no
guarantee of correctness. In fact, the first ever known instance of a
reentrancy attack was performed on a WETH-style wrapper
contract.
Incidents like this reveal the importance of formal verification of
critical smart contracts.
That being said, let’s quickly review the most important functions in
WETH:
- balanceOf: A mapping from addresses to uint256 that tracks how
much WETH a given address “owns”.
- deposit: Payable function. Accepts native ETH in msg.value
and mints new WETH to msg.sender by adding to their account
entry in balanceOf.
- withdraw: Function. Burns WETH by subtracting from the sender’s
entry in balanceOf, and disburses an equal amount of native ETH.
- totalSupply: View function. Computes the total amount of
outstanding WETH issued by taking the native ETH balance of the WETH
contract itself.
- transferFrom: Function. Transfers WETH tokens among different
accounts. It also enforces ERC20 token allowance rules, blocking
unauthorized transfers.
As we verify the correctness of WETH, we will need to keep each of these
functions in mind.
Methods
Using Z3Py, we reimplemented the WETH contract behavior in SMT
equations. We then used the Z3 theorem prover to prove certain facts
about the symbolized WETH contract. First, we proved a key invariant
concerning the correctness of WETH’s internal accounting. Second, we
proved an invariant guaranteeing that WETH holders can always withdraw
their locked ETH.
Invariant 1: Internal accounting correctness
A key invariant of WETH is that totalSupply must equal the sum of
all entries in balanceOf. In other words, WETH must correctly track
its total supply. This is reinforced in the ERC-20 standard. According
to EIP-20, a token’s totalSupply function must “return the total
token supply”. It seems important for a widely-used contract like WETH
to obey the ERC20 token standard.
The WETH contract computes totalSupply by simply using
address(this).balance, which returns the native ETH stored in the
contract total. This amount should match up with the total supply of
WETH ERC20 token, since balanceOf and native ETH are always added
and subtracted commensurately, simultaneously (in the functions
deposit and withdraw, respectively).
Interestingly, while I was formally verifying this property, I
discovered that this invariant doesn’t actually
hold. It’s
possible to cause WETH to return a totalSupply that’s unequal to the
total number of WETH tokens. So technically, WETH’s totalSupply
function is wrong! But we’ll see later why that doesn’t really matter.
Let’s first begin by formalizing the various properties of WETH that
have to do with this invariant. First, the invariant only depends on
totalSupply, balanceOf, and the contract’s native ETH balance.
For the purposes of this invariant, we can summarize the relevant global
state in a 2-tuple: (balanceOf, weth_balance). Here, balanceOf is
a mapping from address to uint256, and weth_balance is a
uint256.
Next, because the WETH contract may not operate properly under
conditions where there is an infinite supply of native ETH in
circulation, we augment our state tuple with a third variable,
eth_supply: uint256 which represents (overapproximates) the total
supply of native ETH outside of our WETH contract (in wei). The new
variable, eth_supply will constrain any native ETH values in
transactions. Thus, our state tuple is (balanceOf, weth_balance,
eth_supply).
Since the invariant is fully parameterized by our state tuple, we need
only consider the ways the components of the state tuple can be
affected. Enumerating them, we have:
- deposit, fallback, and withdraw: updates balanceOf
and the native ETH balance
- transferFrom: updates balanceOf
- SELFDESTRUCT or block reward
coinbase:
updates the native ETH balance (applies to any address, not just
WETH)
We can formalize each of these state transitions as a guarded transition
rule. Each rule takes the form (state, parameters) |
condition ⟶ new_state, where state and new_state are
state tuples, parameters is a tuple of arguments for the transition,
and condition is a predicate required for the transition to be
valid. We have the following rules:
- deposit: ((balanceOf, weth_balance, eth_supply),
(msg_sender, msg_value))
| msg_value ≤ eth_supply
⟶ (Store(balanceOf, src, balanceOf[src] + msg_value),
weth_balance + msg_value, eth_supply - msg_value) - withdraw: ((balanceOf, weth_balance, eth_supply),
(msg_sender, wad))
| wad ≤ balanceOf[msg_sender]
⟶ (Store(balanceOf, msg_sender, balanceOf[msg_sender] -
wad), weth_balance - wad, eth_supply + wad) - transferFrom: ((balanceOf, weth_balance, eth_supply),
(src, dst, wad))
| wad ≤ balanceOf[src]
⟶ (Store(x, dst, x[dst] + wad), weth_balance),
where x = Store(balanceOf, src, balanceOf[src] - wad,
eth_supply) - selfdestruct: ((balanceOf, weth_balance, eth_supply),
(value))
| msg_value ≤ eth_supply
⟶ (balanceOf, weth_balance + value, eth_supply - value) - fallback: same as deposit
- coinbase: essentially same as fallback (overapproximation)
where Store(M, K, V) denotes a mapping identical to M but with
M[A] set to V.
We’ll also define an initial state for the contract:
- (K(0), 0, 120000000e18), where K(0) denotes the mapping with all
entries initialized to 0.
We choose 120000000e18 as the concrete value for eth_supply here, as
there are roughly 120M ether in circulation. Since a large portion of
the total eth supply is locked up elsewhere already, this is a sound
overapproximation.
Constrained Horn Clauses
Since our invariant is an inductive property, it’s tricky for a SMT
solver like Z3 to prove directly. We’ll solve this by formulating the
contract’s semantics as Constrained Horn
Clauses, or CHC for short
[1]
[2]
[3].
Conveniently, Z3 features a relatively robust CHC engine. CHC is also
used by solc’s
SMTchecker.
However, I could not get the CHC engine built into SMTchecker to work
for our purposes. This is likely due to limitations in the Z3 solver,
which we explore later in the article. Instead, we used Z3 directly with
our own hand-written CHCs.
Although there is already a decent amount of literature surrounding
Constrained Horn Clauses, for the sake of accessibility, we’ll walk
through a brief introduction of them in this section. We’ll also go
through a few examples at each step to keep things friendly.
First, we define a function, State(s), which is true iff s is a
valid state tuple that can be reached from a starting state using our
predefined set of state transition rules. In other words, State(s)
enumerates all of the possible states our smart contract could get to.
For instance, State(K(0), 0, 0) should be False, because it’s impossible
for all of the outstanding ETH supply to disappear; it either has to go
into the WETH contract or it either stays circulating. More formally,
you could say, that given some s = (balanceOf, weth_balance,
eth_supply), then State(balanceOf, weth_balance, eth_supply)
necessarily implies that weth_balance + eth_supply is always equal
to some constant. While doing our formal verification, we’d like to
assume as few things as possible beyond our predefined state transitions
and initial states. To prove this property, we could add this
implication in the SMT solver as an additional assertion.
Keep in mind that our goal here is to verify that the sum of all entries
in balanceOf (the real total supply) equals to weth_balance (the
computed total supply). We would formulate this invariant as a CHC
assertion that:
For all s = (balanceOf, weth_balance, eth_supply),
State(balanceOf, weth_balance, eth_supply) implies that the sum
of balanceOf entries = weth_balance.
If it’s possible to reach a state where the constraint does not hold,
then our implication assertion will be violated. As a result, the SMT
solver will report that our constraints are unsatisfiable. In other
words, the solver is reporting that it’s impossible to synthesize a
function State such that it obeys both our state transition (i.e.,
reachability) rules as well as the additional constraints we’re aiming
to prove. Furthermore, we can query the prover for an unsatisfiability
proof, which provides us a logical sequence from our starting set of
assertions to a violating state. This sequence is often a path from our
initial state, through a series of state transitions, to an illegal
state. This is helpful for debugging why our assumptions or invariants
are invalid.
On the other hand, if our invariants hold in all reachable states, then
our assertions will hold. The SMT solver will report that the system is
satisfiable. In other words, it’s possible to synthesize the
function State consistent with both our state transition rules and
our invariants. It also means our invariants are consistent with the
state transition rules. In that case, we can query the solver for a
model, which will actually have a concrete definition for a possible
synthesization of State. This definition will essentially be a
predicate outlining all reachable states.
We start by asserting a set of valid initial “starting” states and
transition rules constraining State(s). For WETH, this is essentially
the contract state after the constructor returns.
State(K(0), 0, 120000000e18) = True.
Then, for each transition rule, we formulate it as a CHC, and assert it.
More concretely, each of our formulae will take a form like:
For all (s, p), (State(s) ∧ Pre(p)) ⟹ 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, and Post(s, p) represents the updated state
after the transition. Intuitively, this means: “for each state s and
parameter vector p, if s is a reachable state, and p are valid
parameters, then we can also reach the updated state Post(s, p)”.
For example, here is our formula for the withdraw transition:
For all (balanceOf, weth_balance, msg_sender, wad),
(State(balanceOf, weth_balance, eth_supply) ∧ (wad ≤
balanceOf[msg_sender]) ∧ (weth_balance ≤ wad))
⟹ State(Store(balanceOf, msg_sender, balanceOf[msg_sender] -
wad), weth_balance - wad, eth_supply + wad).
Here, the preconditions check that the user has sufficient WETH balance
(enforced in the smart contract), and that the WETH contract has
sufficient native ETH to send (enforced in the EVM). The updated state
is identical to the input state, except the user’s balance has been
updated, the WETH contract has less native ETH, and the user has more
native ETH.
Encoding sums over arrays
The invariant that we wish to check is that the sum of all values in
balanceOf is equal to weth_balance; i.e., ΣbalanceOf =
weth_balance. Encoding this sum in SMT is difficult, as there is no
natural way to express the sum within the standard SMT Array
theories.
To resolve this, we introduce an additional “synthetic” variable,
sum_balanceOf that tracks the value of this sum; i.e., sum_balanceOf
= ΣbalanceOf. We augment the state tuple with this additional
synthetic variable. This trick is correct as long as we accordingly
update sum_balanceOf wherever balanceOf is updated. For example,
when adding or subtracting to any elements of balanceOf, we will
correspondingly add or subtract to sum_balanceOf.
As a CHC, our invariant can be formulated as such:
For all (balanceOf, weth_balance, msg_sender, wad,
sum_totalSupply),
(State(balanceOf, weth_balance, eth_supply,
sum_totalSupply))
⟹ sum_totalSupply == weth_balance.
However, this fix alone is not sufficient in “strengthening” Z3’s Arrays
theory implementation enough to prove our constraint systems in a timely
fashion. As an implementation detail, since Z3 does not “understand”
that sum_balanceOf is a sum over balanceOf, it is unable to easily
prove global properties about the values in balanceOf. If forced, it
will generally resort to brute force proofs enumerating all possible
addresses. Clearly, this is not feasible for Ethereum (addresses are
160-bit). Thus, we also augment all transition rules with the additional
precondition that balanceOf[x] ≤ sum_balanceOf, when the
transition uses some value balanceOf[x]. This approximation is
sound, because by definition, sum_balanceOf is a sum over all values
in balanceOf, and a sum is always greater than or equal to an
individual component. Most importantly, these additional constraints
enable the solver to complete much more quickly. It can easily rule out
unreachable states that involve an individual entry greater than our
synthetic sum variable.
Furthermore, to help the solver complete more quickly, we “guide” the
solver by prompting it to prove an additional lemma. The lemma asserts
that both sum_balanceOf, as well as all values in balanceOf are less
than our total eth supply of 120000000e18:
For all (balanceOf, weth_balance, msg_sender, wad,
sum_totalSupply, address),
(State(balanceOf, weth_balance, eth_supply, sum_totalSupply))
∧ (balanceOf[address] ≤ sum_balanceOf)
⟹ (sum_balanceOf ≤ 120000000e18) ∧ (balanceOf[address] ≤
12000000e18).
In our experiments, we determined that this lemma is necessary to make
Z3 avoid brute force proofs.
Results
Surprisingly, when we run our Z3Py code, we immediately discover a
counterexample to our invariant:
unsat
mp(hyper-res( # "3"
asserted(ForAll([A, B, C, D], Implies(
And(
state(A, B, C, D),
Not(D == B)
), query!1
))),
hyper-res( # "2"
asserted(ForAll([A, B, C, D, E, F, G], Implies(
And(
state(C, D, E, F),
B == D + G,
ULE(G, E),
A == E + 115792089237316195423570985008687907853269984665640564039457584007913129639935*G # Note: this large constant is 2^256-1
),
state(C, B, A, F)
))),
hyper-res( # "1"
asserted(state(K(BitVec(160), 0), 0, 120000000000000002281701376, 0)),
state(K(BitVec(160), 0), 0, 120000000000000002281701376, 0)
),
state(K(BitVec(160), 0), 12884901888, 119999999999999989396799488, 0)
),
query!1
),
asserted(Implies(query!1, False)),
False)
To interpret this, we read it inside-out. In plain English, this is
saying:
- The starting state (K(BitVec(160), 0), 0, 120000000e18, 0) is
assumed to be reachable. So therefore, it’s reachable. (Note: this
is the hyper-res marked with “1”)
- You’ve asserted that if a state is reachable, I can also do a
SELFDESTRUCT to the WETH contract to reach a new state. Therefore,
the state (K(0), 12884901888, 119999999e18, 0) is reachable.
- You’ve asserted that if a state is reachable, weth_balance must
equal sum_balanceOf. But we know that a state where weth_balance
= 12884901888, and sum_balanceOf = 0 is reachable.
- This is a contradiction, so what you’ve asked me for is logically
inconsistent. This isn’t satisfiable.
As we alluded to earlier, this is essentially a bug (albeit minor) in
WETH! It’s possible for the totalSupply to not actually be the total
number of WETH tokens in existence! And that’s because, as Z3’s proof
indicates, that you can SELFDESTRUCT eth into the WETH contract. That
increases the eth balance of the contract, but doesn’t mint any new
tokens. This desyncs the totalSupply variable! This is a common bug
pattern
that has been documented before, but it’s surprising for such a popular
smart contract to have such a bug. It may be an intended gas
optimization, or it could be that the WETH developers found this issue
to be insignificant.
In any case, we can still prove a different, but equally valuable
invariant about WETH: that the total number of WETH tokens is always
less than or equal to the native eth balance of WETH. Note that we’ve
relaxed the constraint here to less than or equal constraint, from the
originally strictly equals to constraint. Our new CHC invariant
formulation would be:
For all (balanceOf, weth_balance, msg_sender, wad,
sum_totalSupply),
(State(balanceOf, weth_balance, eth_supply,
sum_totalSupply))
⟹ sum_totalSupply ≤ weth_balance.
Re-running our Z3Py code, we receive our desired sat result!
sat
[state = [else ->
And(Var(1) == 120000000000000002281701376 + 115792089237316195423570985008687907853269984665640564039457584007913129639935*Var(2),
ULE(Var(3), Var(1)),
Extract(255, 87, Var(2)) == 0,
ULE(154742504910672534362390527*Extract(86, 0, Var(3)) + Extract(86, 0, Var(1)), 120000000000000002281701376),
Extract(255, 87, Var(1)) == 0
)
]]
That wraps up this invariant.
Invariant 2: Solvency
In the previous section, we proved that the total number of WETH tokens
is always less than the eth balance of the WETH contract. However, that
does not necessarily prove that WETH holders can actually withdraw their
eth. In this section, we prove additionally that WETH is solvent,
meaning that a WETH holder is always able to withdraw their eth after
depositing. In other words, we show that regardless of what happens to
the WETH contract in between the deposit and the withdrawal, the
depositor is always able to withdraw their eth.
While we can prove this invariant by extending our CHC formulation, that
formulation is not very well suited to the line-by-line conditions,
statements, and control flow in the WETH contract code. For instance,
our CHC formulation simply describes preconditions in state transitions,
without any attention paid to the order those preconditions are checked
in. This is generally OK since Ethereum transactions are atomic, but it
illustrates the general problem that our CHC formulation is a
simplification of the full semantics of the WETH contract’s code.
Furthermore, the CHC formulation does not model the approve function
or any of the ERC20 allowance functionality in transferFrom. This
was previously OK, as we were only interested in proving one specific
property of WETH state. However, for a rigorous guarantee of solvency
(i.e., ability to withdraw after depositing), we need a more
fine-grained approach that more precisely models the semantics of the
WETH contract code. More specifically, we will adopt a symbolic
execution-based approach.
Symbolic execution of Solidity
The best way to explain our approach is through an example. Let’s take
the WETH function approve as an example. Here is the Solidity code
for that function:
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 Solidity function to a Z3Py function. The function
takes, as input, a state tuple like the one described in the previous
section. It then symbolically executes each statement. Finally, it
returns an updated state tuple. Here is our translated code:
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)
We symbolically execute statement (1) as two symbolic stores. Here,
allowance is symbolized as a SMT Array from addresses to Array of
addresses to uint256.
We ignore statements (2) and (3), as we are modeling external calls to
the WETH contract. Since logs and return values do not affect the WETH
state, we don’t care about them. They are essentially side effects that
cannot affect WETH’s solvency.
For a more in-depth example, let’s take the deposit function. Here
is the Solidity code:
function deposit() public payable {
balanceOf[msg.sender] += msg.value; // 1
Deposit(msg.sender, msg.value); // 2
}
And here is the corresponding symbolic implementation:
def deposit(s, state, msg_sender, msg_value):
eth_balances, balanceOf, allowance = state
# transfer of native eth, as per msg_value
s.add(UGE(eth_balances[msg_sender], msg_value)) # note: UGE means "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_balances, balanceOf, allowance)
First, since deposit is a payable function, we must model the
transfer of native eth into the function in msg_value. We impose the
constraint that the sender must have sufficient balance for
msg_value. Those three Z3Py statements are implicit from the rules
of the EVM.
Next, we symbolically execute line (1), updating balanceOf. Lastly, we
can ignore line (2) as it simply emits an event, which we don’t care
about.
Finally, let’s look at how we handle branching control flow in the
transferFrom function. Here’s the Solidity code:
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;
}
And here is how we symbolically execute that:
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)
When we symbolically execute code in this style, we effectively must
symbolize the values of variables on both paths of all branches. In
statement (4), allowance receives either an updated value if the branch
is taken (p is true) and otherwise remains unchanged (p is false).
It should be noted that in the presence of loops, this style of symbolic
execution can lead to what is known as the path explosion
problem,
where each loop iteration creates an additional If-else term. If the
loop is unbounded, then theoretically the formula complexity is
infinite. Luckily, in Ethereum smart contracts, loops are typically
bounded (e.g., due to gas constrants). Thus, loops may be handled in a
symbolic executor by unrolling the loops. This technique is part of a
family of model checking approaches known as bounded model
checking (BMC). This sort
of bounding is an underapproximation. SMTchecker supports BMC, but
doesn’t support unrolling loops as of the time of writing, which is a
weakness (in my opinion).
Finally, note that we aren’t modeling any view functions. We aren’t
really interested in them here, because view functions can’t affect
contract state. Thus, calls to a view function can never cause WETH
to become insolvent.
Proving solvency
We apply the principle of induction to prove solvency in the general
sense. In short, our argument for solvency takes the following form:
- Base case: first, show that there exists some state that is
solvent.
- Inductive case: Given an arbitrary solvent starting state
(inductive hypothesis), show that state remains solvent after any
single transaction made to WETH.
One possible initial reaction to this argument could be: “Well, you
showed that it remains solvent after one transaction. But what about
exploits involving two or more transactions?”
This counter-argument isn’t valid, because in our inductive case, the
starting state is any arbitrary solvent state. Consider a
hypothetical “two-transaction” exploit. Clearly, the exploit would not
render WETH insolvent after the first transaction, as otherwise the
exploit would just be a single-transaction exploit. But since the state
post the first transaction is solvent, our proof for the inductive case
rules out the possibility that some transaction can suddenly render WETH
insolvent. Thus, the hypothetical second transaction in this exploit
could not exist. This argument applies to three-transaction, etc.
exploits as well.
However, this counterargument does show that it is essential that we
don’t make any extraneous assumptions or assertions about the
arbitrary starting state in the inductive case.
Base case
The base case is trivial. We start with WETH’s initial state (the one
where it’s empty) and deposit some money. Obviously, we can still take
the money out. We can prove this for specific user addresses with a
simple unit test. To prove that it’s valid for all user addresses, we
can use symbolic execution.
Inductive case
We model an arbitrary starting state simply with unconstrained
variables. For example, balanceOf is just an unconstrained SMT Array
mapping from address to uint256. We also model a specific, arbitrary
user and their initial deposit (who we will prove to remain solvent) as
an unconstrained address and uint256. Lastly, we also model an
arbitrary global EVM state. For our purposes, 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 the solver from generating “nonsense” counterexamples (i.e.,
ones which are obviously impossible because they are impossible to
attain without breaking the rules of the EVM or violating basic
mathematic principles), we enforce the following assumptions about our
otherwise-unconstrained state:
- myUser != WETH_Address: the user isn’t the WETH contract itself.
- ForAll([a], ULE(eth_balances[a], 120000000e18)): no Ethereum
address has more eth than the total supply of eth.
As with our CHC model, we need to “help” Z3 out by providing some
additional theorems about sums over arrays. First, an entry in an array
can never exceed the sum of all entries. Second, we already proved with
our CHC model that the 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]))
Note that as a result of this assertion, our model for this second
invariant relies on the properties we proved in the first invariant.
This assertion is extremely important for guiding Z3 away from “brute
force” proofs that are unfeasible to complete for full sized contracts.
We also assert some rules to set up our hypothetical depositor:
- balanceOf = Store(balanceOf, myUser, Uint(0)): The user starts
out with no WETH before their deposit. (this is OK because WLOG we
can always get to this “known safe state” in real life by simply
withdrawing all our WETH)
- ForAll([a], allowance[myUser][a] == 0): The user hasn’t
approved anyone already. (otherwise Z3 will generate a
counterexample where some approved user steals the WETH)
Next, we construct our brand-new state, and update it by doing a
symbolic deposit with our brand-new depositor:
state = (eth_balances, balanceOf, allowance)
state = deposit(s, state, myUser, initialDeposit)
Now we have a starting state that we can prove theorems with. Note that
for the reasons discussed previously, we do not impose any other
assumptions on our state–meaning that the variables could be in any
(sane) configuration.
Now that we have a starting state, we perform a symbolic transaction on
it. This is fairly straightforward. Here is how we model an arbitrary,
symbolic deposit call:
def symbolic_deposit(s, state, myUser):
user = FreshConst(AddressSort, 'user')
value = FreshConst(UintSort, 'value')
s.add(user != WETH_Address)
s.add(user != myUser)
state = deposit(s, state, user, value)
return state
We call our symbolized deposit implementation with an unconstrained
msg_sender and msg_value. Note that we do require that the msg_sender
isn’t WETH itself (impossible because WETH never calls any of its own
functions), and that the user isn’t our hypothetical depositor. Note
that we’re implicitly assuming here that the depositor isn’t touching
his funds before he withdraws. If we didn’t have this constraint,
however, the solver will generate spurious counterexamples, as this
constraint is part of the final unsat
core.
We apply a similar approach to all of the external functions:
deposit, withdraw, approve, transfer, and
transferFrom.
For each of these functions, we first perform the symbolic transaction.
Then we simulate a symbolic withdrawal from our hypothetical depositor
in the updated state. Finally, we ask the solver to prove that it is
unsatisfiable for the depositor’s withdrawal to have failed, or for
the depositor to not end up with the same amount of funds they started
with.
Note that in our CHC model, a sat result was desirable, whereas in
this BMC model, a unsat result is desirable. Furthermore, in CHC, we
started with a concrete initial state, and incrementally expanded
our reachable states set through recursive application of the state
transition rules. Whereas in this BMC model, our starting state is
symbolic, but we only perform a single symbolic transaction.
There is some interesting duality here between the two modeling
approaches.
Results
Running our Z3Py code, we prove that any potential external transaction
on a solvent state will keep that state solvent. In other words,
solvency is invariant. We can also query the solver for an unsat
core, which is a
minimized subset of assertions that are all needed to achieve the unsat
result.
deposit
Unsat core:
* b!1 line 157 initial_state ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2 line 161 initial_state myUser != WETH_Address
* b!4 line 77 deposit UGE(eth_balances[msg_sender], msg_value)
* b!9 line 190 symbolic_deposit user != WETH_Address
* b!10 line 191 symbolic_deposit user != myUser
* b!11 line 77 deposit UGE(eth_balances[msg_sender], msg_value)
* b!14 line 267 proof_deposit Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
withdraw
Unsat core:
* b!0 line 156 initial_state ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1 line 157 initial_state ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2 line 161 initial_state myUser != WETH_Address
* b!4 line 77 deposit UGE(eth_balances[msg_sender], msg_value)
* b!20 line 99 withdraw UGE(eth_balances[WETH_Address], wad)
* b!18 line 202 symbolic_withdraw user != myUser
* b!17 line 201 symbolic_withdraw user != WETH_Address
* b!19 line 94 withdraw UGE(balanceOf[msg_sender], wad)
* b!23 line 272 proof_withdraw Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
approve
Unsat core:
* b!1 line 157 initial_state ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2 line 161 initial_state myUser != WETH_Address
* b!4 line 77 deposit UGE(eth_balances[msg_sender], msg_value)
* b!31 line 277 proof_approve Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
transfer
Unsat core:
* b!0 line 156 initial_state ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1 line 157 initial_state ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2 line 161 initial_state myUser != WETH_Address
* b!4 line 77 deposit UGE(eth_balances[msg_sender], msg_value)
* b!37 line 126 transferFrom UGE(balanceOf[src], wad)
* b!36 line 224 symbolic_transfer user != myUser
* b!41 line 282 proof_transfer Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
transferFrom
Unsat core:
* b!0 line 156 initial_state ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1 line 157 initial_state ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2 line 161 initial_state myUser != WETH_Address
* b!3 line 162 initial_state ForAll([a], allowance[myUser][a] == 0)
* b!4 line 77 deposit UGE(eth_balances[msg_sender], msg_value)
* b!47 line 236 symbolic_transferFrom user != myUser
* b!48 line 126 transferFrom UGE(balanceOf[src], wad)
* b!49 line 130 transferFrom Implies(p, UGE(allowance[src][msg_sender], wad))
* b!52 line 287 proof_transferFrom Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
The unsat core is interesting because it tells us exactly which
assertions were essential for the security of the smart contract, and
thus cannot be removed!
Future Work
There are several limitations in this work, which are potential avenues
for future research.
First, because the WETH contract is extremely simple, we symbolized the
various functionalities by hand. Large parts of the manual modeling and
symbolization could be automated by a formal verification framework.
This would also reduce the potential for human error while constructing
a model.
Second, we did not consider events or return values in our BMC model.
These are important for checking whether WETH is ERC-20 compliant. We
consider this outside of the scope of this work, as here we are only
interested in safety properties of WETH, not strict ERC-20 compliance.
Third, we did not precisely model reentrancy or interprocedural control
flow. In BMC, interprocedural control flow is generally resolved through
bounded inlining. However, WETH did not contain any interprocedural
calls, thus we did not have to consider that. Additionally, while there
is the potential for reentrancy due to the use of native ether, WETH
sends ether using .transfer, which imposes a gas limit of 2300,
which is too low for reentrancy to be a real concern. Reentrancy may be
modeled by considering the additional potential transitions and starting
states that reentrancy affords.
Conclusion
WETH is an extremely widespread, popular, and critical smart contract.
We proved two important properties about WETH: that (1) its totalSupply
is always greater than or equal to the sum of the total number of WETH
tokens in existence, and (2) that a new user depositing eth into WETH
will always be able to withdraw it later, regardless of what
transactions happen to WETH in between. We also identified an
interesting, albeit harmless, peculiarity with WETH’s totalSupply
implementation, because it does not consider SELFDESTRUCT/coinbase eth
transfers.
We proved the two invariants using two different, but complimentary
approaches. For the first, we used Constrained Horn Clauses
(CHC).
For the second, we adopted an approach akin to Bounded Model Checking
(BMC). Last but not
least, we have open sourced the artifacts associated with our research
on GitHub.
Formal verification via SMT solving is a widespread approach. For
example, it’s part of solc’s built-in SMTchecker and also seems to be
heavily used in frameworks like Certora. This approach is extremely
enticing, because qualitatively, it often feels as if SMT solvers are
able to “magically” prove theorems in time polynomial to the bit size of
the various formulas. In general, however, a major challenge when
following such an approach is unacceptably slow proof times. Even though
a constraint system may be “correct”, it may be unreasonably slow to
solve because the specific SMT solver (e.g., Z3) isn’t “finding” the
proof. Nonetheless, there are a few heuristic solutions we may use to
remedy this during proof development.
While developing proofs, it is often useful to significantly reduce the
bit sizes of address and uint256 (160 and 256 bits, respectively) to,
say, 4 and 8 bits. This aids in debugging proofs, as even if Z3 gets
caught in a “dumb” brute-force solution, it’s still likely to complete
in a timely fashion–and the sat model or unsat proof will make the
brute-force nature of the solution obvious (the proof or model will be
huge). The issues causing a brute-force proof can then be readily
debugged and addressed in this scaled-down model.
After working with a “scaled down” toy model which the solver quickly
resolves, it can then be gradually “scaled back up”, all the while
carefully measuring how proving runtime is scaling with the size of the
model. For example, you’d prove a toy model where addresses are 4 bits,
and uints are 8 bits–then maybe 16 and 16 bits, then 32 and 32 bits,
etc. If you notice that proof time is remaining linear (hopefully) or
polynomial (less fortunate) with bit sizes, this is generally promising.
Overall, this approach can help identify where the bottlenecks are in
proving. Those bottlenecks can then be targetted by manually adding
“helpful” lemmas to the solver.
Yet another hack is to minimize the model until the minimal set of
constraints leading to pathological solver behavior is isolated. For
example, you might have 5 transition rules (or constraints), and the
solver isn’t finishing. You can try peeling off constraints that, when
removed, don’t seem to help the solver finish any quicker. Repeating
this until a minimal “core” is isolated, it’s possible to narrow down
where a logical bottleneck in the model is. Then, human intuition can be
applied to reason about this bottleneck core, and consider whether there
are important lemmas that are missing from the model.
All in all, a fully-automatic solution seems out of the question for the
forseeable future. For all but the simplest theorems, SMT solvers are
not generally sophisticated enough to prove all desired invariants
without human intervention or guidance. For example, to prove the first
invariant, we had to manually provide helpful intermediate lemmas to Z3
to guide it towards a proof. While proving the second invariant, we had
to manually provide a key lemma proved in the first invariant. Without
some degree of human intervention, it would seem very unlikely that a
fully-automatic solution would have been able to prove the desired
invariants for WETH.
WETH is an extremely simple contract. It is an interesting question
whether SMT-based formal verification will scale to larger protocols,
especially those involving multiple, mutually-interacting smart
contracts. It is desirable to formally verify larger protocols, as there
are many “critical” contracts beyond just WETH. To name a few, these
include Uniswap, Compound, Aave, and Curve. In the future, we hope to
see additional formal verification of smart contracts adopted.
[1]: As of block 15934960 (November 9, 2022), WETH has been in
125,581,756 transactions. This count includes all “top-level”
transactions which call the WETH contract at any point, including via an
internal transaction. Transactions are not double counted.
About Us
Zellic is a smart contract auditing firm founded
by hackers, for hackers. Our security researchers have uncovered
vulnerabilities in the most valuable targets, from Fortune 500s to DeFi
giants. Whether you’re developing or deploying smart contracts, Zellic’s
experienced team can prevent you from being hacked.
Contact us for an audit that’s better than
the rest.
