Continuous Formal Verification

Governance
17

Certora Continuous Formal Verification Report June 2022

Hi Aave Friends! Here’s is a peek at what we have been up to in June 2022

Summary

  • A full verification project was conducted by Certora on 3 governance crosschain bridges - Polygon, Optimism and Arbitrum bridge executors on L2.
    The security report can be found here.

  • A verification and manual review was conducted on the sAVAX oracle adapter for AAVE and the Aave V3 sAVAX listing steward. Our audit found 1 issue in the latter contract, which was fast attended and fixed by BGD.
    The security report can be found here.

  • We concluded the second community driven project. The verification of AStETH on AAVE V2 has finished with 5 participants contributing to the security of the contract, writing a total of 25 quality rules and winning a combined 19.5k$ in grants.
    Certora has also contributed to the security of the AStETH by writing rules and verifying properties. Some of the best rules will be combined with our rules into one complete formal specification. The verification report will be published in the near future.

  • We’ve inspected and released the result of additional ERC20 tokens that were proposed to be listed on the Aave platform using our Aave ERC20 Listing Checker.
    You can read the results on Github or on our dedicated dashboard.

  • More licenses were distributed to the community to reach a total of over 140 keys since the beginning of the Certora-AAVE collaboration!

Governance Crosschain Bridges

Between the 5st-26th of June we conducted a verification project with the goal to secure the following contracts of the governance crosschain bridges:

The contracts are executors for the Aave governance system on the L2 chains.

In this project we’ve verified 24 rules and invariants and found 3 issues.

The spec can be found here, and the security report can be found here.

Our findings include an unexpected revert reason for queued actions, the impossibility to queue 2 identical actions, and a misleading emitting of events in case of a low-level call to a wrong contract.

All these findings have been discussed with the Aave dev team and accepted as low severity issues since they either have workarounds or are edge cases which are unlikely to occur.

Aave V3 sAVAX Listing Stewards

We’ve conducted a manual audit on 2 contracts:

During our audit, we’ve found that wAVAX was forgotten to be configured and set into the same eMode category on the platform. This missing piece was later added to the code before deployment.

You can read about the security audit, our findings and what we’ve checked on our report on the following link.

AStETH on AAVE V2

Between the 12th-29th of June we launched our second verification project. The goal was to verify the AStETH.sol contract, which is the AToken of StETH on the AAVE platform. 5 People helped us secure the contract by writing specifications and verifying them using the Certora Prover. In total 25 quality rules and invariants were generated by the community, resulting in a total of 19.5k$ in rewards given to the participants.

Thank you to all the participants and congratulations on your winnings.

In parallel to the community-driven project, Certora has audited and formally verified a set of rules and invariants. The best rules written by the community will be combined with ours into one complete specification. The report shall be released next month.

Aave ERC20 Listing Checker

In our second release we’re happy to share the results obtained by the Prover on the following tokens:

The results for the runs along with their analysis can be found here and on our dashboard

*** Reminder: The repo with the specifications, the inspected contracts, and a thorough explanation of the spec and the motive of each rule can be found here.

General Note

We are still open to licensing applications. If you’re interested in helping us secure Aave you can apply in this form for a key.

We encourage every community member to join us on our mission to formally verify Aave contracts and earn some money on the way :upside_down_face:.

You can follow us on Twitter to hear about our latest announcements on the grant plan: Twitter

Join us in our discord channel dedicated to the Aave Verification Project: Discord

And come talk to us every Wednesday on 14:30GMT: Zoom

3 Likes