https://x.com/Seecoalba/status/1760426413142761600?s=20

https://x.com/Seecoalba/status/1760649899975069774?s=20

https://x.com/Seecoalba/status/1766147963628159141?s=20

https://x.com/Seecoalba/status/1767485484912054617?s=20

https://x.com/Seecoalba/status/1767963227671990411?s=20

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.

A Guide to Formal Verification and Practical Tools delves into the world of Formal Verification in blockchain development. Here, we explore fundamental concepts, techniques, and essential tools instrumental in ensuring the security and accuracy of blockchain applications.

Formal Verification and Symbolic Execution:

Formal Verification (FV) uses mathematical modeling and logical analysis to ensure program security and correctness. A key aspect of FV is symbolic execution, which assigns symbolic values to inputs, allowing the exploration of various program paths in a single analysis. This technique helps verify if a program can violate certain conditions or reach risky states, using tools like SMT solvers for feasibility assessment. Symbolic execution thus enhances testing, offering a more comprehensive way to establish a program’s safety and correctness.

Theoretical Resources to Get Started:

Before diving into practical tools, it's important to have a solid theoretical foundation. The following resources are excellent starting points:

1. EVM Symbolic Execution: An introduction to symbolic execution in the EVM.

2. Ethereum Formal Verification Overview: A detailed overview of formal verification in Ethereum.

3. Formal Methods for DeFi Developers: This repository contains a course sequence for training developers in the use & development of formal methods and formal tools.

Let's explore some key tools in the formal verification of smart contracts:

1. Halmos:

   An open-source tool that allows developers to reuse unit test properties in formal specifications for the verification of Ethereum smart contract bytecode.

2. Certora:

   Certora Prover is a powerful tool that compares your smart contract bytecode against a rule detailing how you expect your code to behave.

3. Kontrol:

Provides a formal representation of the EVM and facilitates symbolic execution of smart contract bytecode, combining KEVM and Foundry.

4. hevm:

   An EVM implementation for symbolic execution, unit testing, and debugging of smart contracts.

5. Ityfuzz:

   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.

6. Heimdall:

   An advanced tool for smart contract bytecode analysis, specializing in disassembly, control flow graph generation, and decompilation.

7. Pyrometer:

   Combines symbolic execution, abstract interpretation, and static analysis, focused on Solidity but with the potential to be language-agnostic.

8. Ser:

   Ser is a Symbolic EVM implemented in Rust, designed with the notion that each instruction is a granular state transition. Ser treats instructions as functions over machine states. Each instruction has an exec method that takes a complete machine as an argument and produces a lightweight description of how the instruction would change the machine. Ser is intended to be used primarily as a library or backend for smart contract testing tools.

Resources for Developers: These resources are essential for developers interested in symbolic execution and formal verification:

1. EVM Symbolic Execution Notebook: An interactive guide to understanding EVM symbolic execution.

2. Formal Methods Curriculum - Symbolic Execution Exercises: Practical exercises for a hands-on experience in symbolic execution.

3. Z3 Tutorial: An extensive tutorial on using the Z3 solver for smart contract verification.

4. EVM Symbolic Execution Notebook (Spanish Version): A version of the EVM Symbolic Execution Notebook for Spanish-speaking developers.

5. Athena Language Learning Resources: A platform offering learning materials for Athena, a language designed for writing formal proofs.

6. Programming Z3: An online resource providing insights into programming with the Z3 Theorem Prover, authored by an expert in the field.

Conclusion: Formal Verification provides an in-depth and rigorous approach to ensuring the reliability and security of smart contracts, offering developers a way to confidently affirm the integrity and correctness of their code.

I am Sergio, also known as secoalba. My passion for blockchain technology has driven me to develop a deep interest in the security of smart contracts, focusing especially on areas such as formal verification and fuzz testing.

Through this blog, my goal is to immerse ourselves together in the fascinating world of blockchain security tools. We will approach this topic from both a theoretical and practical perspective, offering a balance between conceptual understanding and real application.

We will start with the basics, introducing each tool and its fundamentals. Gradually, we will delve into more complex examples and applications, in order to develop a deep and practical understanding.

Additionally, I plan to integrate the development of these tools into our discussions. This will not only allow us to understand how they work but also how they can be improved and adapted to our specific needs.

For now, I will focus on the following tools:

• Ityfuzz

• Halmos

• Kontrol

• Pyrometer

• Heimdall

As for the topics we will cover, they include:

1. Practical Uses: From simple applications to advanced techniques for each tool.

2. Theoretical Fundamentals: We will explore the internal workings of each tool, providing a more technical and developmental perspective.

3. Formal Verification: Theory and practice related to formal verification, a crucial aspect of smart contract security.