# [CTF] Solving Verilog CTF Offchain (Advanced)

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 total supply of WMATICv2 token and our goal is to successfully call getBounty, which requires these two trackers to be significantly deviated.

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

Download the above contracts and modify the contracts to insert a invariant, which determines whether the logic breaks. Here, the logic holds if the two trackers are equal and breaks 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. Blaz uses AssertionFailed(string) event to determine whether the challenge is solved.

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

Create an onchain task, selecting Solidity Folder. Then, upload the source code of the modified challenge as a zip file.

Select the function to conduct dynamic analysis. Here, we select Bouty.sol and WMATICv2.sol. Note that we don't deploy the WMATIC token contract and we removed the code related to it in previous step, so in the constructor of Bounty.sol, we can use whatever address we want for _WMATIC. However, we need to make sure that the _WMATICV2 address matches its exact address.

In the next step, you shall see that there is one FuzzLand invariant registered.

You can find the concrete exploit in the Issue Found section.