How To Define Invariants
How to actually define the invariants that could save you from exploits
How To Define Invariants
Introduction
Invariants can mean the difference between finding a critical bug in your smart contracts before deployment and someone exploiting them in the wild. This is possible without having to be a security expert who understands all the possible attack vectors for your system.
Invariant testing is set it and forget it. It finds hard-to-find issues in your code and does the heavy lifting for you. You just need to ensure you've properly defined the invariants so bugs can be found by the fuzzer.
In the first post in this series, we covered how to set up an invariant testing scaffolding on an example repo using the Recon builder. We also defined a simple invariant test that let us disprove a claim we made about the system's behavior.
This post will examine what invariants are. It will outline how to define them on ERC4626 vaults.
First, we'll focus on four property types to define our invariants. Then, we'll look at examples of each type for ERC4626 vaults.
This is where the magic of invariant testing begins. It’s where we get to think critically about our codebase. We can then lay the groundwork for understanding what the code is actually doing.
What’s An Invariant Anyway?
In the first post in this series we threw around the term a lot and roughly defined it as “statements about a system that should always hold true”. But what does that really mean?
It means that, with a smart contract system and some specs, we can use invariants to define how it should behave. We can set boundaries on what it should or shouldn't do.
Properties are closely related but are statements that hold only in a specific context. For example if we have an ERC20 token:
Invariant: the sum of user balances should never be greater than the totalSupply
Property: a user’s balance should increase only after calls to the transfer and mint functions
The Four Types Of Properties
Because properties are less restrictive in their definition, we’ll discuss defining invariants in terms of properties. We can think of invariants as properties that always hold.
In this presentation, Certora lays out the four fundamental types of properties we’re interested in when writing invariants.
Namely these types of properties are:
Valid States
State Transitions
Variable Transitions
High-Level Properties
We’ll now look at what defines each of these property types and in the next section see how we can define them for vaults.
Valid States
Smart contracts are simple state machines where the contract’s variable values define its current state. Similarly the variable values of all contracts included in a system define the system state.
Smart contracts may depend on valid states for their logic. We test the system to ensure it only stays in those valid states. Any invalid states found are bugs that can cause unexpected behavior.
Example
The well know AMM invariant used in protocols like Uniswap is x*y = k, where we could define all other states in which this does not hold true as invalid. So if it’s possible to reach a state where x*y != k through external facing function calls, this would imply a bug in the system.
State Transitions
If we already have a set of valid states, as we defined above, we can also define correct behavior for the transitions between these valid states. On top of this we can add further preconditions to help us only check these state transitions if the precondition is met first.
Example
In a lending protocol a user shouldn’t be able to borrow funds (property) unless they have first deposited some amount of collateral (precondition).
The state transition in this case would be that the system shouldn’t be able to transition from a state where the user has no borrow position to one where they do have a borrow position unless the precondition of having deposited collateral is met.
This is a key property for a lending protocol. If it breaks, the system is likely insolvent and can't repay all lenders.
Variable Transitions
As we already mentioned, a system's state is defined by the values of its variables. Some of those variables must behave in certain ways. We can outline the expected behavior for these variables via properties for variable transitions.
Example
In any protocol that expects fees to be collected, the total fees collected should always increase. We could define such a property on the variable responsible for fee accounting.
A break in this property might imply that fees are not collected or can be stolen.
High-Level Properties
High-level properties describe broader system behavior. They often link multiple tangible elements. In contrast, specific properties, like the ones mentioned above, define expected behavior for tangible system elements.
Example
In an ERC4626 vault, the price per share should change only with deposit or withdrawal operations.
This high-level property encompasses variable transitions, and state transitions. Defining it as a high-level property makes it easier to implement. It removes the need to define complex relationships between each element that contributes to it.
Understanding The Target
Now that we know the different types of properties that we can define for any system, we’ll look at how we do this for a real system. The first step to this is understanding the expected behavior of the system.
Your knowledge as a developer, or the docs, will help. For external contributors: the READMEs, whitepaper, and NatSpec should help outline how the system should behave.
Knowing how the system is supposed to work does not require digging into each function's implementation details though. In fact, doing this too early can often take you off track and bias how you define your invariants.
Think of this as the golden rule of invariant testing: you want to define how the system should behave, not how it actually does.
For our example we’ll be using ERC4626 vaults as they are commonly implemented in many different DeFi projects and have properties that are widely applicable since they’re defined by a standard.
Defining The Properties
We’ll now define properties using each of the different types defined above.
Note that this is not a complete list of properties for ERC4626 vaults. You will need more to be confident that contracts implementing the standard work as expected.
If defining your own properties seems overwhelming, book a call with us where we can help you define them. Experience with defining properties can be the deciding factor between testing meaningful scenarios that can uncover vulnerabilities and implementing tests that are more elaborate unit tests. We'll leverage our experience to ensure yours are top-notch with our Invariant Writing Exercise!
Valid State
Since we know that a user must first deposit/mint in order to receive shares, we know that:
The totalSupply of the share tokens must be >= the sum of shares accounted to each user.
If this property doesn't hold, it means the shares aren't fully backed by the vault's assets. This would cause insolvency. The last users to withdraw from the vault would not get their share amount in assets.
Another valid state that we could define for a vault is that:
The totalAssets in the vault must be redeemable by the totalSupply of vault shares.
If this is not possible, this would mean that there is an issue with the accounting and dust amounts may get left over in the vault when users withdraw.
State Transition
We know users must deposit assets to receive shares. To confirm this, we can define a property. It states that:
The vault balance of the underlying asset must increase proportional to the amount of shares minted.
This ensures that users cannot mint more shares than they have deposited for which would also cause insolvency.
Similarly, we can state that:
If a user tries to deposit more than the value returned by maxDeposit, the function should revert.
This could imply that there is potentially unsafe math being used in the vault’s deposit function that could result in user balances overflowing and thus being reported incorrectly.
Variable Transition
Share accounting must reflect the redeemable underlying assets. So:
The vault's totalSupply must decrease proportional to the shares burned on a redemption.
If this property doesn’t hold, it could result in incorrect share price calculation where unbacked shares result in an inflated share price for new depositors.
If our vault implementation takes a withdrawal fee, we can state that:
The variable used for tracking the collected fees should never increase less than the expected fee amount.
This would imply that there is an inconsistency in the fee math being applied and result in the protocol receiving less fees than expected.
High-Level Property
For our high-level property, we will use the same property given as an example in our definition.
The price per share should not change, except for calls to deposit/withdraw.
If we add a function to donate the underlying asset to the vault, this property will allow us to catch the well known share price inflation bug by donating a minimal amount.
We can also broadly state that if our vault has no fees applied:
Deposits/mints and withdrawals/redemptions should be symmetrical.
In other words, for a given amount deposited, if the same amount is withdrawn, the original amount deposited should be received.
This type of broad specification can allow us to catch any irregularities that may exist in a deposit -> withdrawal flow. These can be indicative of underlying issues in vaults that have complicated deposit/withdraw logic.
Conclusion
The examples shown above demonstrate the breadth of behavior that can be covered by properties. After defining properties multiple times, you'll start to build an intuition for which properties to define on a system. You'll need to refer to each category definition less and less.
In this post we’ve looked at how at their core, invariants define how our system should behave by explicitly allowing us to test what it should or should not do. We then saw how we can narrow the definition of our expected behaviors into:
Properties - statements that hold under specific conditions
Invariants - statements that hold under all possible conditions
Then we looked at how we define each of these property types for an ERC4626 vault.
In the next post in this series we’ll see how we can implement some of these properties in Solidity so we can evaluate them with a fuzzer.
In the meantime, can you think of more properties that are required by the ERC4626 specification? Can you implement any of the properties defined here using the techniques we covered in the first post?
Are you convinced of the power of invariant testing but don’t want to have to do everything yourself? Reach out to us and we can take you from no invariants to having them always run against every commit you make, securing your code along every step of the development pipeline with our Invariant Testing Engagements.
Acknowledgement
The property definitions in this post are taken from this presentation created by Certora. While they explicitly define them in the context of being evaluated with formal verification, properties are by definition agnostic to the method used to evaluate them.