Continuous Formal Verification

Governance
20

Certora Continuous Formal Verification Report August 2022

Hi Aave Friends!

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

Summary

  • We’ve announced the results of AAVE Token V3 community verification project! A total of 19 participants contributed over 250 rules and uncovered two issues.
    More stats and details below.

  • Yet another community project started and concluded this month - verifying Aave-Starknet L1 bridge. 11 participants submitted their specifications, contributing a total of 175 security rules.
    The community’s rules are currently being processed to determine the deserved grants for each participant. The upcoming verification report will combine Certora rules with the best rules submitted by the community. We will publish this robust, rule-filled report in the coming month. Stay tuned

  • The Aave ERC20 Listing Checker is live! Using our checker, we inspected and released the result of an additional ERC20 token, BTCb on Avalanche, which is proposed to be listed on the Aave platform.
    You can read the results on Github or on our dedicated dashboard.

AAVE Token V3

After a comprehensive review of the specifications written by the community, here are some stats:

  • We had 25 community members reviewing the code, asking questions, and discussing functionalities.
  • 19 out of the 25 participants submitted spec files containing formal specifications resulting in 275 properties in total.
  • Out of the 275 correctness rules, 240 quality rules passed our professional review and credited their authors with grants. This is an incredible effort by the community!
  • The top 10 community correctness rules were added to the final spec in addition to Certora’s 40 rules to increase the coverage of the specification.
  • 18 of the 19 participants who submitted specs won a combined sum of 125.5K$, with 4 contributors winning 10K$ each and 3 more winning 9K$. Congratulations!

Aave-Starknet Bridge

Between the 15th of August to the 5th of September we conducted a community verification project to secure the Bridge.sol contract in the L1 side of the Aave-Starknet bridge.

The contract implements a bridge on the Ethereum side that acts as an intermediate between users and the Aave platform. The bridge enables transferring Atokens from the Aave platform on Ethereum mainnet to Starknet. The bridge handles deposits, withdrawals, and reward claims.
The verification report along with the community spec will be released in the near future.

In a collective effort, the community detected a low-severity issue where the initialize function of the bridge did not correctly check the validity of all of its input values. More details on this issue will be published in the official report.

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.

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 apply in this form for a key.
We encourage every community member to join us on our mission to formally verify Aave contracts. Who knows, you could 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

2 Likes