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.
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.
From the Recon extension tab you can click the Verify with Halmos button to run Halmos on your Chimera suite.
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.
Similar to Foundry, Halmos uses a toml configuration file format.
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_.
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.
These Foundry reproducers are generated for both Halmos unit tests and invariant tests.
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 latest version of the Recon extension is live on the VS Code Marketplace or available for download directly from the github repo.
No posts
Comments
Nothing yet. Say the first thing.
Sign in to join the conversation.