[CTF] Verilog CTF (Offchain)

Introduction

Source code of the challenge: https://github.com/Verilog-Solutions/CTF-2022-wMaticV2

The project consists of a buggy WMATICv2 token contract containing a function redeem allowing reentrancy attack. Additionally, there is a Bounty.sol contract, which rewards the first person who successfully calls its getBounty function.

There are two trackers of the total supply of WMATICv2 tokens and our goal is to successfully call getBounty, which requires these two trackers to be significantly deviated.

Below is the intended solution that conducts flash loan and reentrancy attacks:

0. Borrow k MATIC such that k > balance() / 10
1. depositMATIC() with k MATIC
2. redeem(k * 1e18) -- reentrancy contract --> getBounty()
3. Return k MATIC

Using ItyFuzz to Solve

We have modified some code to make it easier to deploy: https://ityfuzz.assets.fuzz.land/verilog.zip

Step 1: Add Invariants

Download the above contracts and modify the contracts to insert an invariant, determining whether the logic breaks. Here, the logic holds if the two trackers are equal and break otherwise.

Modify Bounty.sol as follows:

...

+ event AssertionFailed(string message);

function getBounty() public returns (bool) {
    uint256 delta = WMATICV2.totalSupply() >= WMATICV2.balance()
        ? WMATICV2.totalSupply() - WMATICV2.balance()
        : WMATICV2.balance() - WMATICV2.totalSupply();
    uint256 tolerance = WMATICV2.balance() / 10;
    if (delta > tolerance) {
        // reward the first finder
        isHacked = true;
+       emit AssertionFailed("we hacked it!");

-       IERC20(WMATIC).transfer(msg.sender, IERC20(WMATIC).balanceOf(address((this))));
        winner = address(msg.sender);
    }
    return isHacked;
}

We inserted an event AssertionFailed to indicate that the invariant is broken and the challenge is solved. ItyFuzz uses AssertionFailed(string) events to determine whether the challenge is solved.

We also remove the transfer of WMATIC token to the winner since we will not deploy the WMATIC token contract. Instead, we will use ItyFuzz to simulate the execution of the contract and determine whether the invariant is broken.

Step 2: Build

Ensure you have installed solc >= 0.8.0. Then, run the following command to build the contracts:

solc *.sol -o . --bin --abi --overwrite

Step 3: Run ItyFuzz

Use the following command to run ItyFuzz:

ityfuzz evm -f -t "[YOUR BUILD DIRECTORY]/*"

The above command will run ItyFuzz in offchain mode and specify the target contracts (-t). -f enables the fuzzer to conduct flash loan operations. It will automatically detect the invariant violation and generate exploits in less than 10 seconds.