Skip to main content

4 posts tagged with "Ethereum"

View All Tags
Vlad Toie

A helpful guide for users and builders
Article heading

ERC-4337, or ”account abstraction”, is an Ethereum proposal that introduces “account” smart contracts. Account abstraction simplifies the handling of Ethereum accounts, providing a generalized interface for both traditional externally owned accounts (EOAs) and smart contract accounts. Social recovery, paying for gas, and transaction security are some of its proposed improvements. In this new approach, users are no longer bound to handle their private keys and enjoy the flexibility of setting up additional account rules, which improve their security posture.

In this post, we’ll break down the main advantages of account abstraction over current wallet solutions, as well as its security considerations for users and developers.

Current Wallet Management Solutions

Externally owned accounts (EOAs) are the fundamental type of account on the Ethereum blockchain. Whoever possesses the private key has complete control over the actions of the associated EOA. While it allows for straightforward interactions with the network, it also comes with the inherent challenge of managing private keys. A simple mistake could mean permanent loss of funds, and on chain, permanent really means permanent. Apart from that, there’s also the concept of gas fees. This is counterintuitive for most Web2 users, as there’s rarely any type of pay-per-action situation in a modern Web or mobile app.

Given these challenges, several alternatives and enhancements over the basic EOA structure have been implemented:

  • Web browser wallets: Integrated directly into Web browsers, either as extensions or plug-ins. Examples include the MetaMask and Coinbase browser extensions. They provide a user-friendly interface for viewing balances, performing transactions, and interacting with dApps directly from the browser. Operating within a browser makes them susceptible to various attacks, including phishing, XSS, social engineering, and so on.
  • Multi-signature (multi-sig) wallets: These are smart contract–based wallets that require multiple private keys to authorize a transaction. Thus, even if one key is compromised, the attacker still needs access to the other keys to move funds or execute critical actions. Examples here include Safe, Argent, and Armory multi-sigs.
  • Multiparty computation (MPC) wallets: Similar to multi-sig wallets, this type of wallet distributes the transaction authorization by dividing a singular private key among multiple actors. Some examples include ZenGo and Fireblocks. Some MPC implementations use the novel threshold signature, where only m of the n total signatures are necessary. Unlike multi-sig wallets, this threshold property is an intrinsic property of the cryptographic primitive itself, not a programmed smart contract constraint.
  • Hardware wallets: Devices like Ledger or Trezor provide a physical layer of security. They store private keys offline and require physical confirmation on the device to sign transactions. The keys in a properly designed hardware wallet should never leave the device. This makes them most resilient against online hacking attempts.

While these solutions partly address the challenges associated with vanilla EOAs, they also introduce complexities and trade-offs of their own. For example, none provide an actually effective account recovery mechanism. Some use a recovery passphrase that itself can be lost or even stolen, thus still leaving all the responsibility in the hands of users.

First, let’s start with the rationale behind the ERC-4337 proposal and discuss some of its benefits.

Account Abstraction In a Nutshell

At its core, account abstraction streamlines users’ interaction with the Ethereum network. It makes the learning curve gentler for new users, who may otherwise be intimidated by the technical aspects of Ethereum. They no longer need to handle private keys, and the transaction approval procedure can be delegated to other trusted parties.

Meanwhile, developers benefit from greater flexibility when designing and implementing dApps. Account abstraction enables new ways to improve the user experience. These include sponsoring gas fees, transaction legitimacy checks by whitelisting particular addresses, and authentication via social log-in (e.g., “Log-in with Google”), among others. Account rules like transaction spending limits can be set up to eliminate the potential of leftover approvals being misused when a protocol is compromised.

Despite the complexities involved in developing a feature-rich account abstraction wallet, the general architecture is transparent. In fact, there’s only one “off-chain” component, the new mempool. Everything else is handled in smart contracts. Without all the external components that previous solutions had, the attack vectors are significantly diminished.

We see great improvements in user experience with account abstraction, but when things sound overly promising there’s usually a catch. Let’s explore some of the need-to-knows for developers and users, including potential security pitfalls.

How an Account Abstraction Transaction Works Under the Hood

Under the hood, the following steps take place in a typical user interaction:

Step 0: The user sends a UserOperation to a special mempool customized for the ERC-4337. This new mempool is needed so that users don’t pay the gas fees upfront. Bundlers (which are essentially EOAs) will then pick up the newly added UserOperation from the mempool and add it to a bundle transaction.

Step 1: The bundle transaction is then forwarded to a singleton contract called “Entry Point”.

Step 2: Entry Point then individually calls validateUserOP on each user’s account contract (i.e., the wallet smart contract that inherits IAccount) for each transaction in the bundle. (For simplicity, we assume that the bundle only contains one UserOperation in the bundle transaction.)

Step 3: The user’s account contract returns whether the UserOperation it has been asked to verify is valid, according to the rules they set in the validateUserOp function.

Step 4: If valid, the Entry Point verifies that the user account has paid it enough for the gas fees and then calls execute back on the user’s account contract.

→ If invalid, terminate the execution and return the appropriate response back to the Entry Point contract.

Step 5: The user account contract then performs the low-level call with the calldata and target provided in the actual UserOperation, finalizing the execution chain.

There are several enhancements over this simple architecture. One is the usage of Paymasters, which handles sponsoring the transaction’s fees. In this scenario, at Step 4, the Entry Point will verify that the Paymaster has supplied enough for the gas fees to cover the particular UserOperation that’s being verified. This may be crucial for projects concerned about user adoption, as the interactions on the Ethereum blockchain will be more seamless, much like current Web and mobile apps. Alternatively, users could be allowed to pay in stablecoins for gas for a more familiar and convenient pricing scheme.

Moving the transaction execution logic into smart contracts increases developers’ security responsibilities. We present several security considerations when developing account abstraction wallets.

Need-to-Knows for Developers

As we just saw in the previous section, in order to support the ERC-4337 (i.e., account abstraction) standard, a wallet contract must implement the function validateUserOp.

interface IAccount {
function validateUserOp
(UserOperation calldata userOp, bytes32 userOpHash, uint256 missingAccountFunds)
external returns (uint256 validationData);

The validateUserOP function should ensure all of the following:

  • Assure that the function call originated from the singleton EntryPoint (i.e., require(msg.sender == EntryPoint);), to prevent forged calls.
  • Assure that the user operation is valid based on the userOpHash. This is mainly to prevent malicious UserOperations from being executed on behalf of the user account wallet. Also, return SIG_VALIDATION_FAILED (do not revert) on signature mismatch, as per the standard. Revert on any other type of error.
  • (In the case that the Paymaster is not supported) Pay the EntryPoint (msg.sender) at least the missingAccountFunds, thus ensuring that the gas fees are paid for the particularuserOp transaction.
  • The return value should be packed encoded of (authorizer, validUntil, validAfter).
    • authorizer - 0 for valid signature, 1 to mark signature failure. Otherwise, an address of an authorizer contract. The ERC defines “signature aggregator” as authorizer. More details on the signature aggregator can be found here.
    • validAfter and validUntil are six-byte timestamps. The UserOp is only valid either until validUntil or after validAfter, or within the validAfter ... validUntil range.

For reference, the ERC-4337 core team has implemented SimpleAccount.sol, a sample account contract, with all the necessary checks in place. Over time, developers will begin prototyping different improvements over the default ERC-4337, and we anticipate that the following security considerations will come in handy:

  • Upgradability: Since most of the account abstraction’s components are smart contracts, it’s safe to assume projects will make them upgradable. Bugs to look out for here include mismanaging storage variables against overwrites and mishandling the migration functions, business-logic wise. In this Twitter thread, we describe a storage collision hack that led to over $6,000,000 in lost funds. Recently, we also identified an issue that would permanently lock the contract after it was upgraded.
  • Reentrancy: Sponsoring gas is tricky to implement securely. Will there be a Vault that will pick up UserOperations, pay the gas, and forward the transactions? Or will there be some sort of permit-based transaction? Regardless, we anticipate that protocols will opt for custom Paymasters, maybe to allow for ERC-20 transfers, swaps, and so on. Considering this, the most likely attack vector here is reentrancy, as Paymasters will forward some sort of tokens, either native or ERC-20, via calls and callbacks to external contracts.
  • Front-running: Since transactions will be publicly available in the special mempool, front-running attacks will be prevalent, regardless of how transactions are eventually bundled and executed.
  • (For third-party contracts) Reliance on tx.origin: The user will transact via a contract rather than an actual EOA; thus, the tx.origin will no longer match msg.sender. Any EOA-only checks will thus be obsolete, and necessary modifications must be supported by all protocols wanting to offer support for account abstraction wallets. All smart contract developers, even those not directly working with ERC-4337, should be aware of this.

Need-to-Knows for Users

On its own, account abstraction does not come with more security risks for the users. As an ERC, the standard code will be heavily audited and the room for error is minimal. The default implementation, however, does not come with all the features we’ve talked about in this post. So, before any features like transaction spending limit, social recovery, or authentication and so forth are implemented, heavy development and customization are needed. As we all know, smart contracts often turn out to be insecure. Selecting a security-focused account abstraction wallet solution still requires careful diligence.

The Takeaway

The goal of account abstraction is to simplify the implementation of account abstraction–like user experiences. Centralized components are no longer needed to provide an effective alternative for the default EOA. It’s an opportunity for developers to onboard a larger audience to Ethereum, as less technical knowledge will be required to operate an account. This simplification doesn’t directly translate to bug-free code. By reducing the possible external attack vectors, however, developers now have a smaller sandbox to deal with; here, security invariants are more easily defined. We consider account abstraction to be an important step towards a more secure and resilient Ethereum ecosystem, paving the way for additional use cases and user experiences.

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. Real audits, not rubber stamps.

Stephen Tong

Proving the safety of the Wrapped ETH smart contract, using the Z3 Theorem Prover
Article heading


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.


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.


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) | conditionnew_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_valueeth_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))
    | wadbalanceOf[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))
    | wadbalanceOf[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_valueeth_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.

CHC formulation of WETH’s state transition rules

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) ∧ (wadbalanceOf[msg_sender]) ∧ (weth_balancewad))
⟹ 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.


Surprisingly, when we run our Z3Py code, we immediately discover a counterexample to our invariant:

mp(hyper-res( # "3"
asserted(ForAll([A, B, C, D], Implies(
state(A, B, C, D),
Not(D == B)
), query!1
hyper-res( # "2"
asserted(ForAll([A, B, C, D, E, F, G], Implies(
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)
asserted(Implies(query!1, False)),

To interpret this, we read it inside-out. In plain English, this is saying:

  1. 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”)
  2. 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.
  3. 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.
  4. 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))

Re-running our Z3Py code, we receive our desired sat result!

[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)
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)),

# (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.

Performing a symbolic transaction

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.


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.

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
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
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
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
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.


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.

Stephen Tong

Painless smart contract CTF challenges using Paradigm’s CTF framework
Article heading


Zellic recently sponsored CSAW 2022. CSAW is an annual cybersecurity event hosted by NYU in Brooklyn, New York. Over the years, it's become a centerpiece of the US/Canada CTF scene. Each year, CSAW CTF attracts the top high school and college CTF players. In fact, my cofounder, Jazzy, and I actually met at CSAW 2017—where we subsequently formed the team which would eventually go on to become perfect blue. Thus, we saw CSAW'22 as an opportunity to give back to the CTF community.

As a sponsor, we had the chance to contribute a challenge to the CTF. I decided to create a simple Ethereum smart contract challenge. The challenge would revolve around exploiting a vulnerable smart contract. However, the CTF players would need to be able to interact with the smart contract, without leaking their solution or exploit to other players. This is a common problem when creating blockchain CTF challenges.

Luckily, samczsun and the rest of the team at Paradigm have developed an excellent framework for deploying and hosting this kind of CTF challenge. It solves the problem by deploying a private, forked blockchain instance (with Anvil) for each participant on-demand. Here's what that looks like in practice:

$ nc 31337
1 - launch new instance
2 - kill instance
3 - get flag
action? 1
ticket please: ticket

your private blockchain has been deployed
it will automatically terminate in 30 minutes
here's some useful information
uuid: 12341234-12341234-12341234
rpc endpoint:")
private key: 0xabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcd
setup contract: 0x12341234123412341234

The framework is easy to use, albeit not thoroughly documented. Hopefully, this post will provide a practical example on setting up the framework for your own CTF.

The smart contract

Before we dive into using the CTF framework, let's also quickly discuss the smart contracts themselves. This will help provide useful context later.

The smart contract is a straightforward vault which allows users to deposit and withdraw both USDC and DAI. However, when withdrawing, if the vault's balance of the desired token is insufficient, it performs a swap on Uniswap to get more of it.

contract Chal {
// ...
function withdrawDAI(uint amountOut) public {
require(balanceOf[msg.sender] >= amountOut);
balanceOf[msg.sender] -= amountOut;

if (dai.balanceOf(address(this)) < amountOut*10e12) {
address[] memory path;
path = new address[](2);
path[0] = USDC;
path[1] = DAI;

uint[] memory amounts = router.swapExactTokensForTokens(
usdc.balanceOf(address(this)), 0, path, address(this), block.timestamp

dai.transfer(msg.sender, amountOut*10e12);
// ...

The problem here is the lack of slippage checks. An attacker can easily drain the contract by causing the contract to repeatedly make bad trades at unfavorable prices. For instance, this could be done through price manipulation. The attacker then profits off of the resulting price impact.

To exploit this contract, the attacker needs USDC and DAI. Thus, the testnet we host for CTF players should be a mainnet fork so the usual DeFi facilities (Uniswap, WETH, etc.) will be available to them.

Our challenge contract (Chal.sol) is deployed and set up by a setup contract. The following code gives an idea of how our on-chain contracts plug into the CTF framework, so please don't gloss over it:

pragma solidity ^0.8.13;

import "./Chal.sol";

contract Setup {
Chal public immutable TARGET; // Contract the player will hack

// Hardcoded constants (same as mainnet)
address private constant UNISWAP_V2_ROUTER = 0x7a250d5630B4cF539739dF2C5dAcb4c659F2488D;
address private constant WETH = 0xC02aaA39b223FE8D0A0e5C4F27eAD9083C756Cc2;
address private constant DAI = 0x6B175474E89094C44Da98b954EedeAC495271d0F;
address private constant USDC = 0xA0b86991c6218b36c1d19D4a2e9Eb0cE3606eB48;

IUniswapV2Router private router = IUniswapV2Router(UNISWAP_V2_ROUTER);
IERC20 private dai = IERC20(DAI);
IERC20 private usdc = IERC20(USDC);
IWETH9 private weth = IWETH9(WETH);

// Used for tracking if the player has solved the challenge or not
uint private initialBalance;

constructor() payable {
// Deploy the victim contract
TARGET = new Chal();

// Our setup contract will be called with 100 ether by our setup script in the CTF framework.
// Double-check that it's provided 100 ether.
// This also lets the CTF player know what the Setup contract is
// called with, thereby eliminating guessing from the challenge.
// We don't share the setup script with the player, but we do give them
// this setup contract as part of the challenge handout.
require(msg.value == 100 ether);

// We want some DAI and USDC in the vault initially for the player to steal.
// Turn the 100 ether into USDC and DAI using various Defi primitives.
weth.deposit{ value: 100 ether }();
weth.approve(address(router), type(uint256).max);
dai.approve(address(router), type(uint256).max);
usdc.approve(address(router), type(uint256).max);

address[] memory path;
path = new address[](2);

// swap half our initial eth to usdc on uniswap
path[0] = WETH; path[1] = USDC;
amounts = router.swapExactTokensForTokens(
50 ether, 0, path, address(TARGET), block.timestamp

// swap half our initial eth to dai on uniswap
path[0] = WETH; path[1] = DAI;
amounts = router.swapExactTokensForTokens(
50 ether, 0, path, address(TARGET), block.timestamp

initialBalance = curTargetBalance();

// Helper function
function curTargetBalance() public view returns (uint) {
return usdc.balanceOf(address(TARGET)) + dai.balanceOf(address(TARGET))/10e12;

// Our challenge in the CTF framework will call this function to
// check whether the player has solved the challenge or not.
function isSolved() public view returns (bool) {
return curTargetBalance() < (initialBalance / 10);

While developing the challenge's smart contracts, I used Foundry to test locally. It's easy to test my own solution to the challenge by just making a Foundry test.

pragma solidity ^0.8.13;

import "forge-std/Test.sol";
import "../src/Exploit.sol";

contract CSAWTest is Test {
Setup chal;

function setUp() public {
chal = new Setup{value: 100 ether}();

function testExploit() public {
Exploit exploit = new Exploit{value: 100 ether}(chal);

Setting up the CTF framework

First, I just made a new virtual server (for me, a new droplet on DigitalOcean). I overprovisioned the server a lot since it's cheap (will only last for 48 hours) and means I don't have to worry as much about players overloading it.

I also made a new project in Quicknode so I'd have a RPC endpoint to use. Alchemy/Infura/etc is fine too.

For all of this, I just did everything as root. I don't care because it's a single-purpose virtual machine and will be discarded after the CTF is over.

As per the instructions in the Paradigm CTF 2022 repo, install dependencies:

  • Installed Docker (copy pasted commands from here)
  • mpwn: git clone
  • python3: apt install -y python3 python3-dev python3-pip
  • libgmp: apt install -y libgmp-dev build-essential
  • other dependencies: pip install yaml ecdsa pysha3 web3

Each challenge is based on this Docker image. Clone this repo and copy that directory out.

$ git clone
$ mv paradigm-ctf-infrastructure/images/eth-challenge-base my-chal
$ cd my-chal

Add this to the end of the Dockerfile (taken from one of the challenges from Paradigm CTF):

COPY deploy/ /home/ctf/

COPY contracts /tmp/contracts

RUN true \
&& cd /tmp \
&& /root/.foundry/bin/forge build --out /home/ctf/compiled \
&& rm -rf /tmp/contracts \
&& true

Make a directory called contracts. This is where your contracts will live.

$ mkdir contracts

Also make a directory called deploy and put this in deploy/ This is your setup script that deploys your Setup contract.

import json
from pathlib import Path

import eth_sandbox
from web3 import Web3

def deploy(web3: Web3, deployer_address: str, player_address: str) -> str:
rcpt = eth_sandbox.sendTransaction(web3, {
"from": deployer_address,
"value": Web3.toWei(100, 'ether'), # our Setup contract expects 100 ether. So let's give it 100 ether.
"data": json.loads(Path("compiled/Setup.sol/Setup.json").read_text())["bytecode"]["object"],

return rcpt.contractAddress

eth_sandbox.new_get_flag_action() # the implementation of this calls isSolved() on Setup contract

Now you can build the Docker image like this:

$ docker buildx build --platform linux/amd64 -t mytag .

Note that mytag can be whatever you want. And '.' just refers to the current directory where the Dockerfile is living.

Now you can run the Docker image for our challenge with this command:

# adjust these as you see fit

exec docker run \
-e "PORT=$PORT" \
-e "FLAG=$FLAG" \
-p "$PORT:$PORT" \

Now you should have a working CTF challenge. You can netcat to the port the challenge is listening on (in this example, port 31337) and you should be greeted by the CTF framework.

Setting the secret key (important)

It is very important to set the environment variable SECRET_KEY to a random, secret value. Otherwise, participants can directly make RPC calls to the Anvil instance, cheesing the challenge. For more info, you'd want to look the implementations of and

Thanks to rkm0959 of Super Guesser for pointing this out!

Testing against the remote

All good CTFs must have health checks using real solve scripts on its challenges. This is extremely important for quality control and liveness during the CTF.

We can test our live, remote environment using an exploit contract with Forge:

RPC_URL="" \
PRIVATE_KEY="0xf42b8f8e5cbb128b54327182c5399c01dc90a0349239a86963aa7c94a2e1c4db" \
SETUP_CONTRACT="0xa56B24969e7f742e4EF721d5FD647896F0758A48" \
forge create Exploit.sol:Exploit --rpc-url $RPC_URL --private-key $PRIVATE_KEY --constructor-args $SETUP_CONTRACT --value 100ether

Note this doesn't implement any kind of interaction with the launcher netcat server (i.e., the one listening on port 31337). Ideally, you should also have a script to communicate with that, launch new instances, and parse the communications.

Customizing the ticket stuff (Anti-DoS)

In Paradigm CTF, they use a "ticket" system to prevent abuse / DoS. They do this by assigning each account in the CTF website (i.e.,, CTFd, whatever) a ticket. Then, each ticket can only have one blockchain instance deployed at a time. This means that you'd have to register multiple accounts for the CTF, which is presumably behind something like a Captcha.

The way this is hooked up to the CTF framework is that they call some web endpoint to check whether a ticket is valid. This code lives in eth_sandbox/

def check_ticket(ticket: str) -> Ticket:
if ENV == "dev":
return Ticket(challenge_id=CHALLENGE_ID, team_id="team")

ticket_info = requests.get(
if ticket_info["status"] != "VALID":
return None

return Ticket(
challenge_id=ticket_info["challengeId"], team_id=ticket_info["teamId"]

So you'd need to replace this hardcoded URL with your own endpoint.

For me, I didn't want to bother with that, so I just completely replaced this functionality with some generic CTF PoW stuff. This is provided purely as an illustrative example:

def check_ticket(ticket: str) -> Ticket:
if len(ticket) > 100 or len(ticket) < 8:
print('invalid ticket length')
return None
if not all(c in 'abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789' for c in ticket):
print('ticket must be alphanumeric')
return None
m = hashlib.sha256()
digest1 = m.digest()
m = hashlib.sha256()
m.update(digest1 + ticket.encode('ascii'))
if not m.hexdigest().startswith('0000000'):
print('PoW: sha256(sha256(ticket) + ticket) must start with 0000000')
print('(digest was ' + m.hexdigest() + ')')
return None
print('This ticket is your TEAM SECRET. Do NOT SHARE IT!')
return Ticket(challenge_id=CHALLENGE_ID, team_id=ticket)

Note that this PoW doesn't have a nonce. This is so that players only need to solve the PoW once, and then can just reuse their secret ticket thereafter, as a quality of life hack. With this basic scheme, there's nothing stopping players from parallelizing multiple instances of PoW solver and amassing a lot of valid tickets to DoS you.

If you wanted to, you could hack in some additional in-band registration/rate limiting mechanism (by IP address, by captcha, etc.). I didn't feel the need for this, so this is left as an exercise for the reader.


In this blog post, we looked at how Paradigm's CTF framework lets you easily host smart contract CTF challenges. We hope this helps anyone making a CTF challenge!

Finally, all of the code used in this blog post is publicly available here.

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.

Chad McDonald

A developer’s guide to writing secure smart contracts under The Merge
Article heading

When Ethereum changes from proof-of-work to proof-of-stake, there are a few changes to the application layer that developers should be aware of. Some of these changes could impact the security of protocols that are currently safe under ETH 1 but not on ETH 2.


  • Block time is decreasing from a variable ~13 seconds to exactly 12 seconds. If your contract relies on the average block time in its formula, consider updating it to reflect this change.
  • The 0x44 DIFFICULTY opcode is being supplanted by PREVRANDAO. This change is backwards compatible with contracts that use block.difficulty as a source of pseudorandomness, so developers do not have to make changes.
  • Most importantly, consecutive slot miner extractable value (MEV) may invalidate prior security assumptions. Developers should presume that an attacker may control two consecutive blocks and reassess their security logic with this in mind.

In this article, we’ll cover each of these changes in depth as well as potential scenarios in which they could cause problems. We will progress through the changes from the least to the most important because the last two are interrelated.

Block time

The simplest change for developers to consider is the reduction in block time. Block time refers to the amount of time it takes to mine a new block.

The average block time will change from ~13 seconds with a fair amount of variance to exactly 12 seconds except when a slot is missed due to a validator being offline or not submitting a block in time.

Suggestions for developers:

If your smart contract uses the average proof-of-work block time you may want to consider incorporating the 12-second proof-of-stake block time in your calculations.

Many popular DeFi applications use formulas that rely on the average block time. For example, Compound’s formula to calculate interest payments uses a blocksPerYear value that is derived from a ~15-second block time. After the merge, this formula could be updated to use a 12-second block time to calculate interest payments more accurately.

Randomness using block.difficulty

If your contract relies on block.difficulty to construct pseudorandomness, here’s another small change to be aware of.

Developers commonly use the value returned by block.difficulty as a source of pseudorandomness in their applications by mixing it with other values.

Most developers are aware that true randomness cannot be generated on-chain since the EVM is deterministic. However, sometimes a pseudorandom number is good enough if the economic value being protected is less than the amount an attacker receives by influencing the randomness.

Post merge, the EVM 0x44 opcode, which currently returns DIFFICULTY, will be supplanted by PREVRANDAO, which is the output of the randomness beacon provided by the beacon chain in the previous block. Be aware that PREVRANDAO should not be used as a source for true randomness. If the security of a contract relies on a truly random number, then an oracle service such as Chainlink VRF should be used to pull that data on-chain.

Suggestions for developers:

This update is backwards compatible, so contracts that use the DIFFICULTY opcode for pseudorandomness will work the same post merge.

There is an unlikely caveat: if your contract requires block.difficulty to return a value that is representable within 64 bits (i.e., \< 2^64), that will be problematic because PREVRANDAO will return a value within the full 256-bit field.

Multi-block miner extractable value

The most important change that developers should be aware of is the increased likelihood of a validator, which is akin to a miner in ETH 1, controlling two consecutive blocks.

In ETH 2, validators will take over the responsibility of transaction sequencing from miners. Validators will both propose and validate emerging blocks. According to research from Flashbots, it is likely that a large validator pool will produce two consecutive slots within one epoch. Quoting from the same article, “This could enable multi-block MEV extraction by creating a meta-slot out of the number of continuous slots held by a single entity, and might open up new vectors of attacks”.

Even with a low probability of producing two consecutive blocks, since proposer slots are assigned and known at the beginning of each epoch, a market may evolve for bribing a proposer to include or remove a transaction in a block.

This is an emerging area of research, so the security recommendations are still evolving. Let’s explore a few scenarios where multi-block MEV (MMEV) may impact the security of protocols that would otherwise be safe under ETH 1.

Time-weighted average price (TWAP) manipulation MMEV

One likely avenue for attack using MMEV is described in TWAP Oracle Attacks: Easier Done than Said?.

An attacker that controls two continuous blocks can profit by manipulating a TWAP price basically for free:

In block 1:

  • Deposit a large amount of tokens in a Uniswap V2 pool to manipulate the TWAP price. Uniswap V2 pools update the TWAP price at the end of the previous block to protect against flash-loan attacks.

In block 2 :

  • At the beginning of the block, withdraw the tokens you deposited in the previous block. Since you control the transaction ordering within this block, there is no risk of being front run by an arbitrageur.
  • Profit by liquidating users in a lending protocol that relies on the price data from the manipulated TWAP.

Torgin Mackinga, one of the authors of TWAP Oracle Attacks: Easier Done than Said?, points out that under POS, an attacker can perform this attack, given knowledge that they control the next block, by simply using Flashbots to submit their first transaction.

Since MMEV will create lucrative new value extraction scenarios, Flashbots will likely accommodate these new opportunities. Hence, this attack opportunity is likely to be incorporated into Flashbot searchers’ transaction-ordering algorithms.

Randomness manipulation MMEV

As a reminder from what we covered earlier, ETH 2 is replacing the 0x44 opcode DIFFICULTY with PREVRANDAO.

How does PREVRANDAO work?

The PREVRANDAO opcode, like its name suggests, returns the previous block’s RANDAO value.

From the eth2book, “A RANDAO is simply an accumulator that incrementally gathers randomness from contributors. So, with each block, the proposer mixes in a random contribution to the existing RANDAO value.”

The beacon chain uses RANDAO to generate reasonably random numbers, which are important for the security of proposer selection and committee assignments for each epoch. If you are interested in the particulars, I highly recommend reading the eth2book’s randomness chapter for a very digestible explanation.

MMEV opportunities using PREVRANDAO

It is possible for a proposer to influence PREVRANDAO for a limited amount of time until the first honest RANDAO reveal is made after the manipulation. The proposer’s influence is relative to the amount of slots they are able to control through honest proposal selection or bribery.

For example, suppose a proposer is selected for two consecutive blocks. Prior to their first block, they place a bet in a game contract that relies on block.prevrandao to generate pseudorandomness to select the winner. Since the proposer controls two consecutive slots, they can explore four possible outcomes of the value that relies on block.prevrandao and propose whichever is most advantageous to their profit. That could mean not proposing a block in slot 1 or proposing in both slot 1 and slot 2 or any permutation of these.

Furthermore, since proposers control which transactions are included in a block, they may censor a transaction “to force it to be included into the next block, thus force it to use a RANDAO mix that the proposer knows in advance.”

Suggestions for developers:

The EIP-4399 proposal suggests that developers “make your applications rely on future randomness with a reasonably high lookahead” by using the formula K + N + E where K is the end of an epoch, N is a lookahead in epochs, and E is a few slots into epoch N + 1.

In practice, developers should implement a time delay between committing (i.e., bidding) and using pseudorandomness (i.e., rolling a pair of dice) to choose a particular outcome.

The EIP uses an example of a four epoch lookahead, which is about 25 minutes. At this time it is unclear what the tradeoff is between using a shorter lookahead time.

If you are a developer who is planning on using PREVRANDAO, then the example portion of this presentation by Mikhail Kalinin, one of EIP-4399’s authors, may be helpful.

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.