ERC4626 Workshop Inflation Attack

Repository adapted from the Certora workshop on ERC4626 at TrustX @ Istanbul 2023.

The certora folder contains Certora CVL specification for the inflation attack on ERC4626 where the attack implemented in the specification aims to cover a more generalized version of the attack to make it more broadly applicable.

The verification is checked against OpenZeppelin's implementation of ERC4626.

Getting started

1. Sign-up for Certora Free Tier

• Note: It's important to also set the CERTORAKEY environment variable.

2. Install the Certora prover
3. Run the Vault specification by executing certoraRun certora/conf/Vault.conf from within the ERC4626_Workshop folder to view the initial rules verified for the vault. Follow the link returned and wait for the verification to be completed. Alternatively, open the pre-computed results.
4. Run the InflationAttack specification by executing certoraRun certora/conf/InflationAttack.conf from within the ERC4626_Workshop folder. Follow the link returned and wait for the verification to be completed. Alternatively, open the pre-computed results.

Additional Material

• Prover Documentation
• ERC-4626 Specifications
• Inflation Attack