> For the complete documentation index, see [llms.txt](https://docs.ityfuzz.rs/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.ityfuzz.rs/tutorials/ctf-verilog-ctf-offchain.md).

# \[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:

```solidity
...

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


---

# Agent Instructions
This documentation is published with GitBook. GitBook is the documentation platform designed so that both humans and AI agents can read, navigate, and reason over technical content effectively. Learn more at gitbook.com.

## Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter, and the optional `goal` query parameter:

```
GET https://docs.ityfuzz.rs/tutorials/ctf-verilog-ctf-offchain.md?ask=<question>&goal=<endgoal>
```

`ask` is the immediate question: it should be specific, self-contained, and written in natural language.
`goal` is optional and describes the broader end goal you are ultimately trying to accomplish on behalf of the user. GitBook uses it to tailor the answer towards what is most useful for that goal.

The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.