This guide serves as the inaugural article in a series dedicated to ityfuzz.

Here, I'll walk you through the process of getting started with this powerful tool. We'll adopt a straightforward, step-by-step approach to ensure a seamless initiation.

You'll gain insights into the essential installations necessary to kickstart your journey with ityfuzz

Additionally, I'll offer detailed instructions on how to utilize it across different project types, ensuring flexibility and straightforward integration.

Short introduction

ItyFuzz is a hybrid fuzzer for smart contracts that combines symbolic execution and fuzzing to find errors in smart contracts.

Technically, it uses formal verification (concolic execution) assisted by fuzzing algorithms guided by data flow patterns and comparisons.

Installation

The first thing you need to have installed is:

• ityfuzz

• blazo

Init

Once you have both ityfuzz and blazo installed, we'll begin by creating a new Foundry project.

We copy the contract we want to test and make the following modifications:

• Manually imported the solidity_utils/lib.sol library into the "lib" folder.

• Imported the lib/solidity_utils/lib.sol library into our contract.

• Introduced the "bug()" keyword where we believe it could break the invariant.

  • ItyFuzz also supports bug(), which indicates the current code shall not be reached.

Once we have all this available, let's move on to the second part.

We need to create a .json file, for which we'll need to identify the address of our contract along with its constructor if it's in bytes32 format.

To do this, we'll write a small script to obtain the necessary data.

Script

forge script “contract name” -vvvvvv

We create the 1st file called tt.json that we need:

• We copy the address obtained from the script into our tt.json file.

{
    "src/PostExample.sol": {
      "PostExample": {
        "address": "0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f",
        "constructor_args": ""
      }
    }
}

It would look something like this:

Blazo

Once we have all this, we'll start using the Blazo tool.

We'll navigate out of our main repository using cd .. as we need to run it from outside the main repository.

Then, we'll use the command:

• blazo “project name”

Once we've obtained the result, another JSON file named results.json should have been created.

It would look like this:

Ityfuzz

Once we've confirmed that we have the two files created correctly, we'll proceed with running ityfuzz to see if we can find any results within the code.

• ityfuzz evm --builder-artifacts-file './results.json' --offchain-config-file './tt.json' -t "a" -f

And as we can see, ityfuzz has managed to find a code violation for this contract.