The Recon Extension: Now With More Halmos

Run Halmos, Echidna and Medusa, generate reports and convert broken tests into Foundry reproducers using the Recon extension

Introduction

The new version of the Recon Extension is out! Featuring Halmos, Vyper support and much more!

We created the Recon extension using our learnings from over a year of fuzzing to improve our workflows so we can get to the most important part of fuzzing faster: defining and breaking properties.

The first version of the extension did this by offering the following:

• Scaffolding your fuzzing suite (using Chimera)

• Integrating with Medusa, Echidna and Foundry for running tests

• Automatically generating mocks for select contracts

• Cleaning fuzzing coverage reports to only include the files of interest

• NEW: Automatically linking libraries in your Echidna/Medusa setup

• Automatically generating reproducer unit tests for broken properties

• Generating a markdown report for fuzzing runs with detailed information about what was tested

• NEW: Added Vyper support for Mocks and Target Functions

Now with more than 300 downloads and being used by teams like Centrifuge, Corn, Credit Coop, and many more it’s demonstrated its value to anyone implementing fuzzing for invariant testing with the Chimera framework.

Now With Halmos

With the current success of the extension in improving workflows we saw the need to support additional tools to make invariant testing via symbolic execution with Halmos better.

The Chimera template already works with Halmos out of the box, now with the new extension features you can automatically:

• Run Halmos from the extension.

• Generate a halmos.toml file automatically.

• Convert unit and invariant tests broken with Halmos into Foundry reproducers.

• Automatically generate a report from a Halmos run using the extension.

Running Halmos

From the Recon extension tab you can click the Verify with Halmos button to run Halmos on your Chimera suite.

The Recon Cockpit exposes the core configuration options to make running Halmos simpler..

Run Configuration

We’ve simplified the interface when running Halmos through the extension so that the only two configuration options you need to worry about for the majority of use cases are: the targeted contract and the number of loop unrollings to perform.

By default when using the Chimera framework the targeted contract is the CryticTester contract which inherits handler functions defined in the TargetFunctions contract to change the system state. When running with Halmos however the CryticToFoundry contract becomes the entrypoint which inherits from TargetFunctions.

Because Halmos is a symbolic execution tool, symbolic values used for loop evaluation need to be bounded so that the tool doesn’t run for an indefinite amount of time. The Loop parameter therefore allows us to easily bound the loop iterations to a fixed value for easier evaluation.

Halmos Configuration

Similar to Foundry, Halmos uses a toml configuration file format.

The automatically generated halmos.toml configuration file when using the extension.

Now when you run Halmos using the Recon extension this configuration file is automatically generated and preconfigured to work with the Chimera framework. The default settings checks assertions in functions prefixed with check_ or invariant_.

Foundry Reproducers

The core philosophy of the Chimera framework is that Foundry is the easiest tool for debugging issues with Solidity contracts but is limited in its ability to perform advanced testing like invariant testing and symbolic execution. This is why we automatically convert reproducers from other tools that are more powerful for testing invariants (Echidna, Medusa and now Halmos) into Foundry reproducer unit tests which can be run repeatedly and quickly with the same values for faster debugging.

If after running using the extension Halmos finds a counterexample, the extension will now automatically generate a Foundry reproducer that gets added to the CryticToFoundry contract.

A Foundry reproducer generated for a Halmos counterexample on the create-chimera-app repo.

These Foundry reproducers are generated for both Halmos unit tests and invariant tests.

Report Generation

All runs of tools using the extension also have the option of generating a markdown report which allows seeing which properties were tested as well as any counterexamples that generated Foundry unit tests.

The automatically generated markdown report after running Halmos with the extension.

Try It Out

The latest version of the Recon extension is live on the VS Code Marketplace or available for download directly from the github repo.