The Big Fuzz Theory: Multiverse Of Fuzz Madness

We already went through the primer of fuzzing. It's time for us to venture further into the depths of this fascinating realm.

The aim of this article is pretty straightforward. We will discuss various methodologies, including stateless and stateful fuzzing, bounded model checking, and end-to-end (E2E) testing. We will also explore renowned tools such as Echidna, Etheno, and Foundry, illuminating their unique differences and operation mechanisms.

So buckle up, and prepare for an enlightening journey into the intricate world of fuzz testing methodologies and frameworks!

Let’s get started, shall we?

Delving into the heart of fuzzing methodologies, we have a couple of points of interest! The two central pillars: Stateless Fuzzing and Stateful Fuzzing.

Given our solid foundation in the basics of fuzzing, exploring these two methodologies should be a manageable task. Let's initially grasp them through easy-to-understand hypothetical scenarios.

This time we take up an example of a glass! 

Stateless Fuzzing

Stateless fuzzing is like hosting a series of independent one-act plays, each involving a different glass. Picture this: you're the director of a zany experiment where the main objective is to find out if the glass will break under certain circumstances.

In the First act, we see our lead (a glass) being tapped by a teaspoon. Lights out, curtains close. 
For Act Two, instead of continuing with the same glass, you bring a brand new glass onto the stage. This time, you drop a small pebble into it. 
Third Act requires you to throw it on the ground, again you bring a new one of the set.

And so it goes, each act starting with a new glass and a new scenario.

Just like a forgotten Hollywood star, the glass from the previous act is disregarded. Each new act is oblivious to the fate of its predecessor. But you might wonder, "Hey, what if the teaspoon tap weakened the glass, and it was the pebble that pushed it to the edge? Shouldn't we consider this?"

Enter our next star, stateful fuzzing!!!!

Stateful Fuzzing

With stateful fuzzing, we switch from one-act plays to a gripping multi-episode drama. Now, instead of a new glass for each experiment, we have one protagonist glass that goes through every scenario in sequence.

Imagine act one starts with the same teaspoon tap. But in act two, instead of grabbing a new glass, we take the same one and drop the pebble into it. By act three, this brave little glass is starting to tell a story, its history reflected in every smudge and scratch from the previous episodes.

It's like a thrilling TV series. You can't just jump into season three without knowing what happened in the first two seasons. Everything is connected; past actions have repercussions. If that glass cracks or breaks, we'll know the full journey that led to its downfall.

To sum up, stateless fuzzing is a series of isolated, forgetful tests on different 'glasses', while stateful fuzzing follows a single 'glass' through all the trials and tribulations, carrying the history of each test into the next. It's the difference between speed dating and a long-term relationship, fr!

And remember, whether you're dealing with stateless or stateful fuzzing, always wear safety goggles. You know, for the 'shattering' results!

Now let's understand one more important thing before we jump into the necessary tooling.

Bounded Model Checking (BMC)

Bounded Model Checking is basically a technique used in testing, including fuzz testing, to verify systems against a set of specifications that are pre-defined. It does so by checking a system's behavior for a fixed number of steps, i.e., the "bound". If a bug or discrepancy can be found within this fixed number of steps, the model checker will report it. It's just one side. Let's talk about it a little more!

Common example

let's say depositing zero amount into AMM on a fresh contract will revert with the error “MIN_INITIAL_SHARES” remember when I say don't waste your call with inputs that revert, the obvious calls; for that, unit tests are enough. In that case, we know depositing such amounts will throw the same error, so I will guide my fuzzer not to generate inputs that lie outside those “bounds.”

Here's a simple analogy: Imagine you're in a maze (your software), and you're trying to find if there's a path that leads you to a cheese (the bug). The Bounded Model Checking process is like saying, "I'll only look for paths that take 10 steps or less". If the cheese can be found within those 10 steps, you'll find it. If not, BMC will report there's no cheese, at least within those 10 steps. Simple!

Some essence of E2E Testing

E2E testing is a testing methodology that validates the complete flow of an application from start to finish. It simulates a real-world user to ensure that the system behaves as expected. For instance, in a sign-up form scenario, E2E testing would validate all possible user actions, such as entering a blank email and password, a valid email and password, an invalid email and/ or password, followed by clicking the sign-up button. This ensures that all these actions work as a user might expect.

When we talk about mapping E2E testing onto fuzz testing, we're essentially combining the structured, scenario-based approach of E2E testing with the randomness and unpredictability of fuzz testing. E2E testing ensures the system works as expected under normal conditions, while fuzz testing checks the system's stability against unexpected conditions.

Example time: Imagine your smart contract is like a vending machine. End-to-End (E2E) testing is like checking the entire process of buying a snack: inserting the coin, choosing the snack, and receiving it. Everything should work as expected.

Now, fuzz testing is like a curious kid who starts pushing random buttons or inserting random objects instead of coins into the vending machine. The goal is to see if the machine can handle this unexpected behavior without breaking down.

So, when setting up your testing environment, you're preparing for both the regular snack buyer (E2E testing) and the curious kid (fuzz testing). This way, you ensure your vending machine (smart contract) can handle both expected and unexpected situations.

Open up the toolbox!

Lastly, we need to know which tools are best in the case of Solidity smart contracts. When I started working in the web3 space, I instantly became a huge Hardhat fan, only to discover Foundry and get distracted by it. 

As I came across fuzz testing, Echidna, a product by Trail of Bits, embraced me with open arms. It's good, does the job, is intelligent, and is based on HEVM, allowing more in-depth low-level controls. 

But tbh, when Foundry showed its fuzzing prowess, I fell in love hard, but it didn't mean that I and Echidna broke up, let's compare both tools, and you know what, I’ll let you guys judge!!

Framework benchmarking

TL;DR

This blog explores the fascinating world of fuzz testing methodologies and frameworks. We delve into stateless and stateful fuzzing. Bounded Model Checking (BMC) is introduced as a technique to verify systems against predefined specifications. Additionally, we discuss the essence of End-to-End (E2E) testing, combining structured scenarios with fuzz testing's unpredictability. Lastly, we compare renowned fuzzing tools, Echidna and Foundry, highlighting their unique features and differences.