Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Governance
16

Certora Continuous Formal Verification Report for March and April 2023

Hi, Aave Friends!

Here’s a sneak peek at what we have been up to in the past couple of months.

Summary

  • StaticAToken - We’ve completed our review and published a report for BGD’s implementation of a static aToken. The review led to several changes and code fixes. The most significant issue we reported exploited the fact that the staticAToken keeps an internal track of the reward tokens, and the sync needs to be initiated manually. This opened an opportunity to trick the internal staticAToken accounting into owing the user more rewards than they deserve on account of other users. The full report with our review can be found here.

  • Community Contest - We are pleased to announce that the community contribution projects are back! On Wednesday, 17th of May, we will start verifying the staticATokenLM contract together in a community effort. Join us to secure Aave and win some prizes for your effort.

  • Safety Module - We are happy to share our report for the safety module with the community! In total, we reported 6 issues, 1 of which was high severity and live on the previous version of the code! All of the issues were promptly resolved by BGD, and the patches were proven using the Certora Prover. You can view the full report here.

  • GHO Stablecoin - GHO’s complete formal verification report is also publicly available! A total of 70 properties were proved and integrated into the repository’s CI during the review. See the full report here

  • PR #820 of V3 Core - We’ve reviewed a PR by BGD that addressed a potential griefing of users by others. The full report can be found here.

If you are interested in our work and would like to know more, feel free to ask us questions in the forum :)

General Note

Do you want to write some rules and help secure contracts for Aave? We are still accepting licensing applications. If interested, fill out this form to apply for a key.
We encourage every community member to join us on our mission to formally verify Aave contracts. Who knows, you could even earn some money along the way. :upside_down_face:.

Follow us on Twitter to hear about our latest grant announcements: Twitter
Join our Aave dedicated discord channel: Discord
Talk to us LIVE every Wednesday at 14:30 GMT: Zoom

1 Like