Hybrid fuzzing: Sharpening the spikes of Echidna

By Tom Malcolm, University of Queensland, Australia

Smart contract fuzzing is an effective bug-finding technique that is largely used at Trail Of Bits during audits. During my internship at Trail of Bits, I contributed to expand our fuzzing capabilities by working on Hybrid Echidna, a “hybrid fuzzer” that couples our smart contract fuzzer, Echidna, with our symbolic execution framework, Maat, to improve the process of finding bugs. While Echidna is a great tool, it still struggles to discover some bugs. With Hybrid Echidna, we enhance the process to find even more!

Echidna is a property-based fuzzer built by Trail of Bits that is widely used in smart contract bug hunting. (See its README for a list of notable uses of Echidna and some of the vulnerabilities it has found.) It lies in the category of “smart fuzzers,” which use the ABI of a contract and perform static analysis of its source code to make decisions on how best to generate input data.

In this post, we’ll look at an example of a contract with bugs that can be triggered only with very specific 256-bit integer inputs (e.g. 0xee250cacdb8de774585208b1e85445fca3bd09da95683133ed06742b71ec2434). We will first show how Echidna, which uses random fuzzing techniques, struggles to discover the bugs. We’ll then examine how Hybrid Echidna improves upon traditional random fuzzing and see the results for ourselves!

The problem

The following contract contains two bugs (represented as assertion failures). Triggering the bugs requires finding inputs that consist in specific 256-bit integers, which are not hardcoded into the contract’s code. The chance of randomly finding the right input is 1/115792089237316195423570985008687907853269984665640564039457584007913129639936 — which means that the bugs that are impossible to find by relying on random fuzzing only.

pragma solidity ^0.7.1;
 
contract VulnerableContract {
 
   function func_one(int128 x) public pure {
       if (x / 4 == -20) {
           assert(false); // BUG
       }
   }
 
   function func_two(int128 x) public pure {
       if ((x >> 30) / 7 == 2) {
           assert(false); // BUG
       }
   }
}

When we run Echidna on the contract (by executing the command echidna VulnerableContract.sol --test-mode assertion), it locally saves certain information about its findings. A summary is displayed in the friendly ncurses-esque interface that it greets us with, as shown below:

Although Echidna identified three “interesting” inputs and added them to the fuzzing corpus, none of them resulted in an assertion failure (i.e., a bug). In other words, Echidna failed to trigger the bugs in the contract.

What happened is that Echidna couldn’t find inputs that would meet the conditions required to trigger the buggy execution paths. This is understandable, as the bug conditions are arithmetic equations, and Echidna can only be so smart when it comes to solving such equations. Looking at the coverage files generated by Echidna, we can clearly see the code paths that weren’t covered:

    | pragma solidity ^0.7.1;
*r  |
    | contract VulnerableContract {
    |
*   |    function func_one(int128 x) public pure {
*   |        if (x / 4 == -20) {
    |            assert(false); // BUG
    |        }
    |    }
    |
*   |    function func_two(int128 x) public pure {
*   |        if ((x >> 30) / 7 == 2) {
    |            assert(false); // BUG
    |        }
    |    }
    | }

Echidna can successfully find bugs (and has on many occasions), and at the end of the day, a bug found is a bug found. However, as this example shows, its results could be improved. How, you ask? Well, if only there were a mutation of the tool, some Frankenstein version that combined Echidna with something that could sharpen its ability, forming one super bug-finder—something like a Hybrid Echidna.

Hybrid Echidna to the rescue

Note: If you’d like to follow along here, install the Optik suite of tools by running the following command:

pip install optik-tools

Hybrid Echidna is part of Optik, a new suite of tools for analysis of Ethereum smart contracts. Optik is intended to comprise both standalone tools and tools that improve upon existing ones (typically fuzzers) for dynamically analyzing smart contracts. So far, its sole tool is Hybrid Echidna, which improves upon Echidna by coupling it with Maat, a symbolic execution framework also developed in-house by Trail of Bits. At the beginning of the summer, the Hybrid Echidna codebase was a minimal one that simply ran Echidna. Now, Hybrid Echidna is a complete tool (albeit one still under development) that consistently improves upon Echidna.

How does it work?

At a high level, Hybrid Echidna simply runs Echidna multiple times, interweaving those runs with symbolic analysis to generate new fuzzing inputs. A more in-depthprocess for fuzzing a contract now looks like this:

Execute an initial run of Echidna to collect a fuzzing corpus.
For every unique input that is found, symbolically execute the contract with that input and record its coverage.
Review the coverage information for any missed paths.
Use Maat to solve inputs for those paths, and record any new inputs that would lead to the execution of a missed path.
Repeat the process until there are no more inputs that can be found.

So Hybrid Echidna takes the data that Echidna finds, uses Maat to figure out how to change its input to reach difficult paths, and then fuzzes the program again (with the newfound inputs) until it can’t improve upon the findings. Think of Echidna as a contestant on Who Wants to Be a Millionaire?: when Echidna needs a hand, it can “phone a friend” in Maat (and make an unlimited number of calls).

Show me!

Let’s revisit the contract we looked at earlier—the one with two bugs that Echidna overlooked—and see how Hybrid Echidna fares.

We use the following command to run Hybrid Echidna:

hybrid-echidna VulnerableContract.sol --test-mode assertion --corpus-dir hybrid_echidna_output --contract VulnerableContract

Upon running Hybrid Echidna, we are greeted with another friendly UI that provides insight into its performance. This includes timing information and the following key takeaways:

Hybrid Echidna found seven unique inputs (five through fuzzing and two through symbolic execution).
Two of those inputs resulted in assertion failures (i.e., bugs).
The assertion failures occurred in the func_one and func_two functions

We can quickly verify the inputs that triggered these failures (which are shown in the “Results” section). Take Hybrid Echidna’s input to func_one, 15032385536, and recall that a result of 2 indicates an assertion failure:

$ python -c 'print((15032385536 >> 30) // 7)'
2

As we can see, Hybrid Echidna found random input that meets the very specific condition in func_one, improving upon Echidna’s performance. In other words, it found more bugs!

What’s next?

Despite its current limitations (such as its lack of support for symbolic keccak operations and its inability to account for gas usage), we are already seeing promising results with Hybrid Echidna. These results reinforce our confidence in our approach to fuzzing and make us hopeful that we’ll have even more exciting results to share in the future.

Optik is still under active development. Going forward, we plan to improve the project’s symbolic executor and, more importantly, increase Hybrid Echidna’s scalability by testing it on real-world codebases. Our end goal is for every engineer at Trail of Bits to use Hybrid Echidna when auditing smart contracts.

Try installing Optik and testing out Hybrid Echidna on the VulnerableContract.sol example (or on your own contracts), and let us know what you think!