Never Stop Improving Your Invariant Tests

Evolving Centrifuge's invariant testing suite to find new edge cases

After we proposed to improve their invariant testing suite (previously discussed in part 1 and part 2) using our newly developed best practices, the Centrifuge team quickly accepted, with the expectation that this would mostly help them write cleaner code by catching any bugs that might get accidentally introduced.

As it turned out, these new best practices helped uncover a yet-to-be-detected edge case.

We’ve further distilled these best practices into create-chimera-app 2 so you can use these as the starting point for your fuzzing suite.

In this post we’ll look at why we developed these best practices and how you can implement them in your own fuzzing suite using Centrifuge as an example.

Exclusively use assertions

At Recon, we now only use the assertion testing mode in Echidna and Medusa. This change makes managing properties easier by not mixing boolean properties with assertion properties. This change simplifies how we write properties. It also cuts down on design decisions and reduces mental effort.

Echidna can also only test in one mode at a time. So if you also want to use boolean properties, you'll need to run several tests. This is why we've chosen to stick with using only one property type.

Implementing these changes in the Centrifuge codebase was relatively straightforward, where we changed boolean properties:

The previous implementation of the invariant_global_1 property as a boolean property.

to simple assertion properties:

The new implementation of the same property using an assertion from the Chimera Assertion contract.

This also required changing the prefix that the echidna config would normally use to detect boolean properties which was previously set to “invariant_” back to the default “echidna_”.

Making these public functions with assertions lets the fuzzer call them randomly after any other target function. Allowing it to behave like a more efficient boolean property as it doesn’t get checked after each call to the target functions. If a breaking call sequence exists, we don't need to check the property after every function call. Instead, a random call following the correct breaking call sequence will still break the property and provide a reproducer.

Adding an ActorManager

Actors allow you to determine how many addresses interact with your test suite the way a user would. Previously, there was no standardized way to handle this and most people implemented a different solution for each suite, ourselves included.

We saw that this problem kept happening and added to our setup time. So, we created an ActorManager contract to track all actors in the fuzzing setup. At the time of the initial test suite creation it was determined that the extra overhead for tracking multiple actors wouldn’t be worth the extra state space exploration that it would provide, but now using the ActorManager we could do this with just a few changes.

The ActorManager implementation that allows more easily tracking all actors in a fuzz suite setup.

With the implementation of the ActorManager, which is inherited in the Setup contract, we were then able to add multiple actors directly in the setup function:

The _addActor function adds new actors to tracking in the ActorManager contract.

This also allows us to ensure that tested properties were only evaluated for the actors we set up. We did this by using the actors directly in each call to a target function handler using the useActor modifier which pranks the current actor. We also now pass in the current actor for any function arguments that a user’s address would be passed into:

Using the useActor modifiers allows the fuzzer to call each target function handler as the currently set actor returned by _getActor.

We could then loop through all actors and check that the property only holds for them, knowing that it wouldn’t be possible for other addresses to have interacted with the system as a user would:

An example of a property made possible by only minting to the actors in our test setup.

As a result of having more actors, the fuzzer was able to uncover an edge case that was previously unknown. This edge case is discussed more in the Trophies section below.

As a result of having more actors, the fuzzer was able to uncover an edge case that was previously unknown.

Simplifying reverts for stateless tests

Previously we had implemented a ERC7540CentrifugeProperties contract which was meant to test Centrifuge-specific properties on the ERC7540 vaults standard implementation.

Because these property checks included state changing operations, they included a call to a _doTestAndReturnResult function which allowed the functions defined in the contract to act as stateless tests by undoing any state changes made by the call to the target function.

The erc7540_9_withdraw property performs a withdraw operation which we don’t want to be maintained across other calls.

The erc7540_9_withdraw_call_target calls the property defined above and reverts the state changes using the _doTestAndReturnResult function.

By reverting the state changes, these functions would not contribute to a property breaking call sequence for global properties. This was done because the state changes they include would make it difficult to read a breaking call sequence, what we like to refer to as the “story”. This isolates their purpose to only serve as more elaborate stateful fuzz tests of certain properties.

For the above test this means that we can check that an actor can always withdraw their entire balance. But we don’t want this to contribute to our “story” because it would mean that we would have calls to other standard target functions as shown below mixed in with the call to erc7540_9_withdraw_call_target which makes it difficult to understand what’s actually happening in the call sequence.

The vault_withdraw target simply performs a state changing action with fuzzed inputs and its name is descriptive of what it does, making it simpler to understand what’s happening in the “story”.

With a recent discovery that any assertion test could be made stateless much more simply by just reverting at the end of the function call, the ERC7540CentrifugeProperties were refactored to implement the following modifier:

The statelessTest modifier reverts state changes while still allowing the called target function to be added to the corpus to increase coverage.

Which made the test implementations easier to read and maintain:

The simplified test implementation.

Simplifying properties with induction

In the original property implementations, many used ghost variables for tracking the system state.

The original property implementation where sumOfClaimedRedemptions and mintedByCurrencyPayout are ghost variables.

However, we've realized these types of implementations can often add unnecessary complexity by creating ghost variables that need to always be properly updated inside of their respective handlers.

These ghost variables had to be updated inside of multiple handlers and tracked values which were “ghosts” of the actual system state; they don’t actually exist in the system but are derived from its expected state update.

Now we tend to prefer properties that can be implemented inductively to prove the same thing which involves reading the state of the contracts directly before and after a given operation.

In proving a property by induction we first need to prove that the base case is true, in our case this is before any state changing operations are called on the contract, where the fuzzer can call one of these global properties. We then need to prove that the property is true for the inductive step which is simply a check that for any state-changing operation (call to a target handler), the statement is also true.

An example of one such implementation for the above mentioned property is shown here:

The refactored implementation of the invariant_global_2 property to be inductive.

In the inductive implementation we prove that for any decrease in pendingRedeemRequest that isn't a call to claimCancelRedeemRequest, the escrow correctly pays out the amount of trancheTokens redeemed by the actor.

Fork testing setup

The fork testing setup was added in the setupFork function for the existing invariant testing suite. This function just overrides the contracts deployed in the setup function with the actual deployed values.

Overriding the initially deployed contracts and actors with ones deployed on mainnet.

This allows direct testing of properties against the forked chain state on Ethereum Mainnet in addition to governance fuzzing which allows simulating the result of actions executed on the Centrifuge Chain that have side-effects on Ethereum Mainnet before they happen. This lets us more accurately test if there is any logic on Centrifuge that breaks assumptions on Mainnet because we can’t directly test properties end-to-end between the two chains.

Trophies

As mentioned above there was an edge case discovered by the fuzzer when multiple actors were added which is shown in a Foundry unit test below:

The foundry reproducer that gets automatically generated from broken properties using our scraper tool.

This previously unknown edge case indicates that a requester can request a redemption for a frozen (blocked) recipient. Given that a frozen recipient should not be able to redeem from the system this subverts the expected functionality and was therefore addressed by the Centrifuge team.

Next Steps

The next step that would allow for more effective forked testing would be what we call governance fuzzing. This would allow the suite to be run every time a valid request is created, as Centrifuge uses an asynchronous vault system where requests must first be created on Ethereum then approved on the Centrifuge Chain before they’re executed on Ethereum. This would allow verifying if the resulting fulfillment on the deployed contracts would result in any of the properties breaking.

This is an interesting possibility to test because we noted in the initial review that issues due to incorrect execution on Centrifuge Chain are very much a possibility as these actions are fully trusted. Having these tests in place would therefore allow us to systematically verify if the system can ever be in a state that allows this to happen.

This isn't possible with the standard fork testing setup as we're still fundamentally clamping fulfilled values by the requested amount as can be seen here:

The investmentManager_fulfillDepositRequest function simulates the execution of a message on Centrifuge Chain but relies on clamped values that may bias the fuzzer.

As a result there's still the possibility of a fulfillment execution that doesn't fit our modeling and so could break one of the properties. The best case in this situation is to therefore test against the actual fulfillment values received from Centrifuge Chain as this is what gets executed in the deployed system.

Conclusion

We’ve seen how we implemented our latest fuzzing best practices to revamp Centrifuge’s existing invariant testing suite, making it simpler and more robust.

The changes we made included: exclusively using assertion tests, implementing an ActorManager, simplifying stateless tests, simplifying properties with induction and creating a fork testing setup.

Implementing an ActorManager allowed us to discover an edge case that was previously unknown, demonstrating the benefits of always improving existing tests even if the underlying code they test hasn’t changed.

Going forward the Centrifuge team could additionally implement governance fuzzing which would give them greater guarantees that there is no logic implemented on the Centrifuge Chain that could break assumptions on Ethereum Mainnet.

---

If you've made it this far you value the security of your protocol.

At Recon we offer boutique audits powered by invariant testing. With this you get the best of both worlds, a security audit done by an elite researcher paired with a cutting edge invariant testing suite.

Sound interesting, talk to us here: