Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Governance
11

Certora Continuous Formal Verification Report November 2022

Hi, Aave Friends!

Here’s a peek at what we have been up to in the past month.

Summary

Aave V3 deployment on Ethereum mainnet is fast approaching and all of Aave’s service providers are working in full force to support the development teams to deliver the new version of DeFi’s leading lending protocol as soon as possible, with high quality and great security in mind.

Here are a few of the projects we are working on to ensure the security of Aave’s new version release:

  • The Aave ERC20 Listing Checker strikes again! This time we used our checker to inspect and release the result of an additional ERC20 token, cbETH, on Avalanche, which is proposed to be listed on the Aave V3 platform.
    You can read the results on Github or on our dedicated dashboard.

  • We are formally verifying Aave’s PR of fixes to the live V3 core contracts named V3.0.1. During the month of November, we found and reported two issues:

    In addition, we decided to seize the opportunity and take advantage of new capabilities of Certora prover on the core-V3 repository from December 2021. In the revision process we were reconsidering and generalizing the assumptions we used in our specifications, tightening and expanding the existing checks, and verifying new properties. This project continues well into December, so stay tuned for more updates.

  • We proceed working on 4 high priority projects which are still under development - veToken, GHO, Proof Of Reserve, Price sync for stable coins

    So far, between these 4 projects, we’ve found and reported several issues to the developing entities and are in continuous talks with them to resolve the existing issues. We are looking for additional problems. Reports for each project will be published in the future, along with the publication and deployment of the contracts.

Aave ERC20 Listing Checker

We’re happy to release another token review using our AAVE ERC20 Listing Checker - BTCb on Avalanche:

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.

Aave Core V3.0.1

We’ve reported 2 low severity issues to Aave on the live V3 code:

  1. In the library WadRayMath, the functions rayDiv and wadDiv revert too eagerly due to an explicit check written in assembly. These functions revert for large input values due to heuristics used in the implementation.
    The check can be found in the specification written here, and the results can be found here.

  2. Following this incident with FEI, a fix of the condition in _updateIndexes() was suggested. To affirm that the change is indeed fixing the described bug, we wrote a simple property:
    “The debt index, retrieved by getNormalizedDebt(), should be monotonically increasing”.
    Trying to verify this property, we got a counter example from the Prover that shows an inconsistency in values acquired by getNormalizedDebt() due to an optimization done in _updateIndexes().

    Besides, we’ve revised our assumptions, documented and tightened the existing specifications and added additional checks for the following contracts:

General Note

Do you want to write some rules and help secure contracts for Aave? We are still open to licensing applications. If you’re 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:.

You can 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:30GMT: Zoom

4 Likes