Recon’s Why
Recon’s goal is to make invariant testing the default for all Solidity developers because it can find bugs that are hard to reason about and can cost millions of dollars if exploited in production.
While trying to reach this goal we realized the primary thing stopping most developers from using invariant testing was the setup time. We created the Recon extension to reduce this setup time and make developers’ jobs easier, so that with one click you can: scaffold a new invariant testing suite, run fuzzers and formal verification tools and automatically convert broken invariant reproducers into Foundry unit tests, reducing the setup time from days to hours.
Continuing Development
The goal of our current fundraising round is to provide compensation to developers for their contributions to the extension and tooling used by the extension.
Below we detail low hanging fruits (problems which if solved contribute to marginal added value in the extension) for which we have a clear roadmap, as well as moonshot ideas (which would significantly increase the capabilities of the extension and advance the state of the art) but haven’t yet been fully explored.
Low hanging fruits - Extension
Some ideas for improvements to be made directly to the extension have been outlined in the following issues in the Recon extension repo:
Canary generation - allows proving a given function handler was called successfully
Selective Ignore - selectively ignore properties only used during certain phases, like canaries
Dynamic replacement - enable dynamic replacement directly from within the extension
Optimization mode recaps - format output of optimization mode runs to show the maximum values
ETAs - display estimated time remaining for a fuzzing/formal verification run to complete
Low Hanging Fruits - Solidity
We’ve also identified areas for improvement in our setup-helpers repo which is used by our extension when setting up a testing suite with our Chimera framework to simplify repetitive test suite setups. These would unlock new testing capabilities not currently easily accessible with invariant testing.
Our primary goals on this end are:
Simulating weird token behaviors in our existing AssetManager (for abnormal token behaviors like those described in this repo)
Simulating a reentrant actor in our ActorManager
Advanced Research
The following section describes research topics toward which received funding would be allocated in order to advance the state of the art of invariant testing.
OracleManager
Create a new manager contract that implements a token and an oracle, with the ability to set the price of the token. This unlocks the ability to more easily track and manage how the pricing mechanism used by a protocol can be used in economic attacks.
Corpus Scoring
An algorithm to score the quality and thoroughness of a corpus (a saved sequence of function calls which a fuzzer uses to explore the system state). Having a quantitative metric of corpus quality allows improving the feedback loop in AI powered workflows by generating an objective function which can be optimized for.
Standardizing Corpus Definitions and Reuse
Standardizing the corpuses generated by different tools (Echidna, Foundry, Halmos etc.) will help make all tools more compatible by allowing the output of one to be fed as the input into another. With the implementation of a shared corpus, the use of different tools becomes additive as they all can expand on the work of one another, this allows more easily switching between tools for specific use cases based on their strengths (e.g. formal verification for testing math libraries, fuzzing for finding truncation related issues).
Raycasting
Currently running the fuzzer for a nontrivial amount of time (1-2 hours) to determine the coverage (source lines accessed during a call) that a handler can reach. This is part of a slow feedback loop which requires first defining the function handlers, waiting for the fuzzer to run, then evaluating the coverage output to determine what changes need to be implemented to improve coverage.
The ability to directly determine the coverage that a handler can reach with statistical certainty using raycasting is a better feedback mechanism for invariant engineers as it’s immediate and allows them to determine the efficacy of the fuzzer before running it.
Autoclamping
Similar to the objective of raycasting to reduce the time spent in the feedback loop of running the fuzzer to evaluate coverage, the goal of autoclamping is to use formal methods to identify and explore the dependency between certain inputs and the state space exploration that they allow.
Using the output of formal methods allows generating clamped handlers (which reduce the search space explored by the fuzzer) that provably do not over-constrain the inputs passed to the targeted function. This ensures handlers can still fully explores the entire possible state-space, without making calls to the system that explore reverting paths.
Autoclamping has been researched extensively by Alex and the ideas behind it will be discussed in this presentation at DeFi Security Summit. This gist outlines the general ideas behind autoclamping which will be covered in the presentation.
ErrorManager Library
Currently with the standard implementation of properties that check for errors, only errors after a call to a given target function can be caught. This doesn’t allow sufficiently high specificity to identify where in a target function’s call trace a general error like an arithmetic panic may have occurred. The ability to catch a revert on a specific line however is useful for making assertions about how the system should behave in specific conditions.
A library that allows managing errors and assertions for production and development environments, making it easier to write properties that check for specific reverts at specific lines would therefore make implementing such properties significantly easier.
Storage Subscriptions
Performing static analysis can allow determining specific storage slots that a given function can modify. The fuzzer can then subscribe to these storage slots to determine if a given storage slot has been accessed.
This allows the fuzzer to programmatically target functions based on new theoretical coverage that can be explored by the storage slots that it modifies. This should allow significant optimization of a fuzzer’s performance by providing a better algorithm through which it can explore the entire state space.
Transparency
We will be putting 100% of the funds raised into a merit.systems account. This account will fund the development of the extension and additional repositories mentioned above that contribute to the overall objective of faster, more effective fuzzing.
The founders of Recon will receive no money from this merit systems account nor from their contributions to the above described tools as the funding is meant to reward developers that work on the extension, which can include developers at Recon (likely 0kn0t, creator and maintainer of the extension).
Methodology
First we will wait for the funding round to be completed and the payouts to be sent.
We will then sum the total of funding received and transfer it to the merit.systems account based on the nominal value at the day of transfer (this prevents having to collect multiple small donations) which will then be used to pay contributors and maintainers.
Support us
The funding page for the extension is here. Which is part of the Developer Tooling Quadratic Founding Round by Giveth and Gitcoin.