Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Governance
1

Executive Summary

This is a continuation of proposal 6308 to improve the security of smart contracts built on top of Aave using a combination of formal verification and manual code review. In the last six months, Certora has improved the security of the Aave protocol and played a significant role in increasing the security community’s involvement in Aave’s development. We want to continue to improve Aave’s security and enable agile development of new products. This proposal will give a brief overview of Certora and formal verification, outline what we’ve accomplished in the last six months, and discuss our goals for ensuring Aave’s security.

Overview

Certora is a security company focused on delivering tools that enable developers to mathematically prove the correctness of DeFi protocols. In the last six months, Certora worked closely with the Aave community, Aave developers, BGD labs, and external communities, including The Secureum, to guarantee the security of the Aave protocol and enable massive innovation.

We engaged twenty external security researchers who, along with our team of security engineers and researchers, helped Aave safely develop 16 new products and list 12 new tokens. A total of 51 smart contracts were reviewed which contained over 25,000 lines of Solidity code. One critical and two high-severity bugs were prevented using the hundreds of correctness rules written by the community and the Certora team.

As we continue our collaboration, we plan to improve on the current proposal in five significant ways: (1) allocate more resources, (2) improve the Certora Prover, (3) develop new open source technology for automatically checking rules written by the community, (4) drastically improve the collaboration with auditors and the security research community, and (5) develop a monitoring framework for checking the CVL rules before every transaction.

About Certora

Our technical team of over 80 people consists of formal verification experts, compiler experts, static analysis experts, research and development engineers, security engineers, and security researchers. Many have PhDs in their fields, decades of security experience, and a strong history of significantly increasing the security of the most significant protocols in DeFi [Aave, OpenZeppelin, MakerDAO, Euler, Compound, TrueFi].

Project Highlights: March 13, 2022 - September 12, 2022

The Aave protocol is leading DeFi in innovation and security, supported by Certora’s technology and the security research community. The Certora team worked closely with BGD labs and the Aave protocol team to ensure code security using funding from the previous continuous verification proposal. We outline the main highlights of Certora’s contributions during the six months of the project:

  • Certora allocated six R&D personnel and engaged twenty external community security researchers to review protocol contracts, most new to the Aave community. Secureum was very helpful in developing this community.
  • 16 new Aave products were developed under our security review, and 12 new tokens were listed, all checked by the Certora Prover for bugs and nonstandard behavior.
  • 51 smart contracts were reviewed, totaling 25,000 Solidity lines of checked code (the Certora Prover checks the generated EVM byte code, which is much larger).
  • A total of 380 correctness rules were selected out of 600 submitted rules by the Certora team and the Aave community. Unlike traditional security audits, these specifications continue to be useful as protocols continue to evolve.
  • Certora provided three workshops to familiarize the community with our tools.
  • $283,500 were awarded in grants to the community. $151,000 of these awards came from the grants allocated by Aave in the original proposal; Certora provided the additional $132,500. As of September, twenty security researchers composed over 550 security rules for Aave and won 35 grants.
  • One critical, Two high-severity, One medium-severity and Ten low-severity bugs were prevented before the code was deployed.
  • No major bugs were identified in manual audits by Chain Security and Sigma Prime after formal verification and in the deployed code.
  • A dedicated dashboard for verified smart contracts is maintained here.
  • A dedicated dashboard for checked listed tokens is maintained here.
  • Three complementary papers are being written by The Secureum, BGD Labs, and Certora which describe the main lessons learned from the three-way collaboration. The first article is titled “Aave-Certora-Secureum: A DeFi Security Collaboration”.

The New Proposal: Keeping Aave Agile and Safe

We propose to continue the current engagement. Below are the highlights of what we will accomplish:

  • Allocate six R&D personnel to lead the community in specification development for the Aave protocol.
  • Write specifications and verify new Aave products and listed tokens.
  • Provide free access to our SaaS tooling (Certora Prover) to members of the Aave community.
  • Develop and improve our technology to address needs raised by the Aave verification efforts. We will continue to provide new tools to the Aave community as they are developed.
  • Develop our education materials and be available to the community to help them learn to use our tools.
  • Continue to grow Aave’s security community and incentivize the best of this community to engage with Aave more closely. We propose to award several fellowships to the best security researchers to work closely with Aave and Certora. We have identified leading candidates who contributed to this year’s program.
  • Certora will collaborate with Sigma Prime to help them use the Certora Prover as part of their ongoing security review. We will also collaborate with other third parties such as Secureum, who are working to ensure the security of Aave and building the Aave community. Additionally, Code4rena and Spearbit security researchers are proficient in rule writing. For example, Kurt Barry, who works as an independent security researcher through Spearbit, was able to find a 4 year old bug in the MakeDao tool using the Certora Prover. Therefore, for major code revisions, we will conduct Code4rena competitions for finding bugs and writing correctness rules.

Pricing

The previous proposal cost $1.7M per 6 months. A 20% discount is given for an annual contract ($3.4M), bringing the total to $2,700,000 for a year while maintaining the level of service provided by Certora. In addition, Aave will provide 400,000 USDC for fellowships and community grants. The total cost to AAVE will be $3,100,000.

This community grant will be partially used to support designated fellowships to security engineers who are engaging with the Aave DAO on a part-time basis and potentially long-term collaborations with the DAO. We have identified several candidates who participated in the previous grant program and contributed significant rules throughout the project and expressed interest in participating in the fellowship program.

The price for the project is per annum, and vested linearly over one year. 30-day termination is possible with a vote. $1,890,000 is paid in USDC and $810,000 is paid in Aave tokens. 400,000 USDC are awarded to security researchers from the Aave community for reviewing code and writing security rules, as well as the fellowships. The receivers of the fellowship will be selected by a community with two people from Aave BGD, one person from the Aave team, and two people from Certora. Unutilized grants will be returned to Aave.

UPDATE 30 October 2022:

Following the community’s feedback, Certora decided to fund the grant program in the original sum of $400K per year. No fellowships will be awarded as part of the grant.

This reduces the total cost of this proposal to the Aave community to $2.7M.

3 Likes
2

It seems multiple service organizations are pursuing renewals or new contracts all at once…

There is nothing wrong with this but it leads to more scrutiny and proposal-to-proposal comparison - and can be an expensive time for the DAO.

This seems like a waste:

Given the mandate of Aave Grants DAO and Aave DAO’s support and allocation of funding to other development teams (BGD, Aave Companies) there is no need to run another Grant program in parellel.

You mention this team is compiled of “two BGD members, Aave members, and Certora”

Aave Grants already has this composition with @eboado as a reviewer, @daveytea , an early developer from Aave, and others such as @corbpage.

Many of these folks are developers at heart and are actively looking for new ways to increase the security and stability of Aave. If there is a greater need, we can add this funding and an additional reviewer.

1 Like
3

Details for the community to be discussed apart, we strongly support this renewal proposal, given how vital it is for the progress of all technical development on Aave to have a firm like Certora providing security assurances.

We can certify that during the previous 6 months of work, the professionalism and involvement of Certora in all developments (minor and major) coming from BGD and other technical contributors has been top-notch.



Regarding the main components of the new proposal:

Base price of Certora’s services
Even if the price is quite high, given that it is the same as on the previous proposal, and understanding the demand for Certora’s services, we don’t have any reason to think this is not fair. Maybe it could be helpful (if possible) to disclose some references of market rates of Certora @Shelly.

Fellowships
We think “targeted” grants programs like the previous run between Aave <> Certora should have a long-term goal, and getting part/full-time independent security professionals engaging with the Aave DAO after successfully contributing to Aave projects is the most natural and beneficial outcome.
So we support a model in which the general grants budget is reduced over time, in favor of engagement with proven individuals, becoming an acquisition channel of talent for Aave.
Given that on the previous proposal, the grant budget was $200’000 for 6 months, and now it is $400’000 for 12 months, it seems to follow that approach, on which we agree. Still, it could be important if @Shelly could clarify if there is any specific target for the split grants/fellowships out of the $400’000, as again, in our opinion fellowships should get higher allocation over time, and other grants lower.
In addition, given the highly technical knowledge/background required to evaluate the suitability of fellowship candidates, from BGD we are open to collaborating on a one-time review of the candidates and their previous work on Aave projects.

General grants
Involving 20 external security researchers to write 550 security rules on Aave projects, evaluate rules’ quality, organize workshops showcasing Aave’s technology, and the $132’500 that Certora says they provided on top of the initial budget seems enough reason to consider the program a big success.
(It could be important @Shelly to present specific examples of those collaborations with grantees).
So even if we think the size could be something open for discussion by the community, it seems like a good idea to keep some components.

On the previous @fig point, we think that probably Aave Grants DAO is not the proper entity to tackle these “grants”, given the management overhead and quite specific knowledge required to evaluate everything around. Seems preferable that Certora does the “heavy lifting”, having support from technical parties like us (part of our work scope with Aave) or other technical or security contributors (SigmaPrime?) when required.
Goes without saying that we think everything should be fully transparent for the Aave community.

4 Likes
4

Would never question Certora’s competency or contributions to date, but tend to agree with @fig here on the duplicative nature of the 400,000 USDC budget for fellowships and community grants.

Might some or all of the proposed grant reviewers (two people from Aave BGD, one person from the Aave team, and two people from Certora) be willing to contribute a bit of their time to Aave Grants DAO by acting as the final due diligence hurdle for these types of requests?

5

Thank you, @fig, @bgdlabs and @d0bby for your prompt responses.

To @fig’s first point:

This is a renewal of an existing grant and our team is still working with Aave closely. We are currently reviewing code changes and rules, hence the rush to submit now.

To @fig’s, @d0bby’s and @bgdlabs’s points about the community grant:

@bgdlabs: present specific examples of those collaborations with grantees

High security bug found by a community member on AAVE Token V3: https://www.certora.com/wp-content/uploads/2022/09/Formal-Verification-Report-of-AAVE-Token-V3.pdf
The biggest potential success of community engagements like this is bringing new talent to work closely with the DAO. Out of the 20 participants, several outstanding researchers expressed interest in contributing to security on a regular basis and with high availability. We are now picking the finalists and we will let the community know.

@d0bby: Might some or all of the proposed grant reviewers (two people from Aave BGD, one person from the Aave team, and two people from Certora) be willing to contribute a bit of their time to Aave Grants DAO by acting as the final due diligence hurdle for these types of requests?

From our experience during the last 6 months, community engagement in the rule writing process has had a net-positive effect on the overall security of the reviewed projects.
We believe that running such a process requires technical review and was handled successfully during the last 6 months. We welcome other suggestions from the community regarding the management and the structuring of the grants program.

We note that we will continue to do the heavy lifting of review while members of the committee will serve as “watchdogs” and ensure transparency, even if the grant is not run by us. Finally, we plan to give access to the platform to all the participants.

@bgdlabs: Maybe it could be helpful (if possible) to disclose some references of market rates of Certora

The current SaaS pricing for complex code bases is $2M per annum since it requires huge support from R&D personnel. The price for professional services is $80,000 per week. This includes two security engineers and one security researcher. Here we are charging $2.7M per annum and allocating up to six security engineers, a security researcher and multiple R&D persons for the whole year. We are also granting unlimited access to our platform for anyone who wants to contribute rules.

@bgdlabs: clarify if there is any specific target for the split grants/fellowships out of the $400’000, as again, in our opinion fellowships should get higher allocation over time, and other grants lower

Agreed. As mentioned before, we have contacted several excellent researchers, and we hope that we can allocate $150,000-$200,000 of the currently proposed grant programs to 2 or 3 such persons.

4 Likes
6

Hello All! :wave:

Following the community’s feedback, we decided to take the grant portion of the proposal ($400K) on us (Certora), reducing the total cost to the community down to $2.7M!
This guarantees Aave will continue to receive the same level of service and security used in the last 6 months with a reduced cost.

2 Likes
7

We’re excited to post the snapshot vote on our proposal here: Snapshot
The voting will last until November 3, 2022, 12:30pm PT.

We look forward to continuing with the governance vote and to securing the Aave protocol and ecosystem!

2 Likes
8

Voting YES as we believe the steps taken by Certora so far have proven useful to the protocol as a whole and the updated work agreement terms are reasonable and well deserved!

4 Likes
9

Sigma Prime is in favor of this proposal. Continuous formal verification is an excellent complementary tool to the ongoing and recurring security assessment services we provide to the Aave DAO. Certora have proven themselves as a leader in this field.

4 Likes
10

Certora Continuous Formal Verification Report October 2022

Hi, Aave Friends!

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

Summary

  • We’re happy to announce a renewal of our collaboration with Aave!
    The new agreement will see Certora extending and expanding its services for an additional full year. Keep reading for more details.

We are currently working on 4 projects that are still under development:

  • veToken - a new aToken primitive that allows the Aave Protocol to participate in Vote-Escrowed economies

  • GHO - a native decentralized, collateral-backed stablecoin, pegged to USD.

  • Proof Of Reserve - a system by Chainlink that allows for reliable monitoring of reserve assets, and usage of that data feed directly on-chain.

  • 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 and look for additional ones. Reports for each project will be published in the future, along with the publication and deployment of the contracts.

Collaboration Renewal

In the past month, we’ve gone through the process of raising a proposal to renew and extend our agreement with the Aave community. The proposal passed on Saturday, 12th of November 10:48 UTC with a staggering 651k supporting votes coming from 200 distinct addresses. We thank the AAVE community for their support.

In the upcoming year, we will provide more value to the Aave community by:

  1. Introducing new tools:
    1.1. A tool that will increase the quality and confidence in formal specs, and speed up the review process.
    1.2. Certora is developing a monitoring framework for checking the CVL rules on deployed contracts before every transaction.

  2. Enhancing our current services by allocating more resources:
    2.1. 6 security engineers and researchers will write formal specifications for sensitive smart contracts.
    2.2. Collaborating with the security auditing firm SigmaPrime and other 3rd party organizations to create a more holistic security suite.
    2.3. Provide Certora keys to new community members who desire to help us secure Aave by reviewing code and writing formal specifications. All previously issued keys will be automatically extended until the end of the new agreement.

  3. Making the Aave security community a more prominent part of Aave security:
    3.1. Releasing more community verification projects to existing and newly developed Aave contracts.
    3.2. Continue developing and providing educational materials on the Certora Prover and Aave eco-system, for novice and experienced members of the community alike.
    3.3. Recruiting more brilliant security-minded engineers to the community through monetary incentivization. These independent engineers will get familiar with the Aave codebase and will dive deep into specific contracts and initiatives.

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

3 Likes
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
12

Certora Continuous Formal Verification Report December 2022

Hi, Aave Friends!

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

Summary

We are happy to share our progress for some of the projects that we’ve been working on over the last couple of months:

Additionally, we are currently working on the following:

In each of these projects, we found and reported issues to the developing entity. We will share the reports

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
13

Placeholder to bypass the “no more than 3 messages in a row” limitation

14

Thanks @yuradmt :smiley:

Certora Continuous Formal Verification Report January 2023

Hi, Aave Friends!

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

Summary

  • We’ve reviewed the upcoming upgrade of the safety module - stkToken. In our verification, we’ve found three issues - one high severity, one medium severity and one low severity. The development team promptly addressed the issues, and we are currently reviewing the fixed implementation. The report will be released along with the repository

  • We’ve reviewed the first phase of ​BGD’s rescue mission of tokens locked on Aave. In our review, we suggested adding some safety checks that will prevent insolvency of the contracts due to this delicate action. You can read the specification and the official report in BGD’s github repository.

  • We continue making progress on verifying the GHO token. So far, in our verification, 48 properties have been formally written. The report will be published next month.

  • We also started verifying the staticAToken which extends the ERC4626 standard. The report and results of this verification effort will be released along with the deployment of the token.

If you are interested in our work and would like to know more, you’re welcome 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 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:30 GMT: Zoom

2 Likes
15

Certora Continuous Formal Verification Report February 2023

Hi, Aave Friends!

We’re posting a little later than usual following a very active month. a very active month. The team has been working hard behind the scenes to secure the protocol, and our findings will be published in the upcoming weeks. Take a look at what we’ve done in the past month.

Summary

  • safety module - we performed another review iteration following the modification of the code to address issues that were reported in January. In this iteration, we found and reported three additional issues, bringing the count to six - 1 high, 2 medium and 3 low severity. BGD promptly addressed the issues. The fixed version of the code passed all of the tests constructed for the Certora Prover, verifying that the reported issues were resolved.

The report will be released in March.

  • GHO - after a long review, with nearly 70 verified properties, we’re almost done with the GHO token review. A few issues were detected and reported to Aave developers.

The report will be published next month (this time for real :slightly_smiling_face:).

  • staticAToken - the lions-share of the verification was done this month. We reported three issues which were addressed promptly by the developers. We are continuing the verification effort and expect to complete it in March.

The report and results of this verification effort will be released along with the deployment of the token.

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

General Note

Do you want to write some rules and help secure contracts for Aave? We are 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:.

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

3 Likes
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
17

Certora Continuous Formal Verification Report for May and June 2023

Hi, Aave Friends!

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

Summary

  • Continuous Checks - We are continuously checking every code addition to all previously verified projects. In June, one of our tests in AAVE Token V3 caught a critical bug in CI. The bug allowed users to inflate their balance indefinitely and therefore get infinite proposition and voting power. The bug also allowed the malicious user to deflate other users’ proposition and voting power in the same action. Check out the CI run that caught it - LINK.

  • StaticAToken Community Contest - On May 17, we kicked off a formal verification security project in which we opened the static aToken V3 contract for community review. Dozens of independent security researchers participated, with a total of $40K awarded to 21 participants. 85 issues were submitted. The most significant issues were acknowledged by BGD, and fixes will be incorporated into the code base.

  • Governance V3 - We are working full force to verify the components of the new Aave governance mechanism. The governance system includes 2 repositories with 19 contracts and almost 4,000 lines of code. So far, we’ve reported multiple issues and are working closely with the developing entity, BGD, to fix them. As part of the governance project, we also recheck and review the associated voting tokens to ensure proper functionality and correct communication with the governance system.

  • GHO Stablecoin - Following the support of this TEMP CHECK by the community, we’ve reviewed the implementation of the Gho Steward.

  • Next Community Contest - On July 19, we will be starting another Aave community formal verification project. This time we will verify a live contract that is currently fully functioning in the ecosystem! Join our aave-community discord channel to stay up-to-date with the latest announcements regarding the project.

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

2 Likes
18

I was the community member / auditor that found the High severity issue on the AAVE Token v3, it was great to contribute to the security of aave v3 alongside Certora.

8 Likes
19

Hello Aave friends :wave: :grinning:

September 13th marked the end of our annual engagement with the community. Lately, we’ve been working on a few high profile contracts - Governance V3, Crosschain Infrastructure and the Gho GSM, which are all in final stages of review.

Until the reports are ready to be shared, we decided it’s a good time to list all the work that’s been done in the past 18 months as part of our continuous service to Aave.

Contracts Reviewed

A list of all the major projects we reviewed:

  1. aStETH on Aave V2 (Lido) - formal verification + manual review - Link to Spec, Link to Report - 5-26 June, 2022.
  2. Governance Crosschain Bridges to L2 - formal verification + manual review - Link to Spec, Link to Report - 5-26 June, 2022.
  3. sAVAX Listing Steward on Aave V3 Avalanche - manual review - Link to Report - 21-28 June, 2022.
  4. sUSD Listing Steward on Aave V3 Optimism - manual review - Link to Report - 21-28 June, 2022.
  5. FRAX Listing Steward on Aave V3 Avalanche, Fantom, Polygon - Link to Report - 21-28 June, 2022.
  6. MAI Listing Steward on Aave V3 Avalanche, Fantom, Polygon - Link to Report - 21-28 June, 2022.
  7. BTC.b Listing Steward on Aave V3 Avalanche - Link to Report - 21-28 June, 2022.
  8. AAVE Token V3 - formal verification + manual review - Link to Spec, Link to Report - 15 July - 10 August, 2022.
  9. Aave-Starknet Bridge (the L1 Ethereum side) - formal verification + manual review - Link to Spec, Link to Report - 15 August - 5 October, 2022.
  10. Aave Governance Level 2 Update - formal verification + manual review - Link to Spec, Link to Report - 31 August - 11 September, 2022.
  11. Reward Aware Token - formal verification + manual review - project was paused by the developing team - 15 September - 20 December, 2022
  12. Aave Proof of Reserve - formal verification + manual review - Link to Spec, Link to Report - 6 November - 22 November, 2022.
  13. Chain Link Synchronicity Price Adapter - manual review - Link to Report - 14 November - 8 December, 2022
  14. Aave Core V3.0.2 (update before deploying on mainnet) - formal verification + manual review - Link to Spec, Link to Report - 17 November - 15 December, 2022.
  15. Staked Token V1.5 - formal verification + manual review - Link to Spec, Link to Report - 7 December - 10 March, 2023.
  16. Rescue Mission Phase 1 - formal verification + manual review - Link to spec, Link to Report - 6-12 January, 2023.
  17. Static aToken V3 - formal verification + manual review - Link to Report, specs will be published soon - 18 January - 31 March, 2023.
  18. Gho Stablecoin - formal verification + manual review - Link to Spec, Link to Report - 30 January - 28 February, 2023.
  19. PR#820 for Aave V3 Core - manual review - Link to Report - 3-15 March, 2023.
  20. Staked Token V3 - an adaptation of formal specification from Staked Token V1.5 - Link to Spec - 18-26 July, 2023.
  21. aAAVE With Delegation - an adaptation of formal specification from Staked Token V1.5 - Link to Spec - 13-20 August, 2023.
  22. Governance V3 - formal verification + manual review - 16 April - present - currently in progress.
  23. a.DI - formal verification + manual review - 16 April - present - currently in progress.
  24. Gho GSM - formal verification + manual review - 27 July - present - currently in progress.

A total of 8 High severity, 6 Medium severity, and 27 Low severity issues (not including the projects currently in progress).

Community Security Reviews

We conducted several community FV reviews as an extra layer of defense after professional review. The following contracts were released for community review (the products of the community reviews are incorporated in the official reports at the above list):

  • staticATokenLM (old) - May 2022
  • aStETH - June 2022
  • AAVE Token V3 - July 2022
  • Aave-Starknet Bridge - September 2022
  • Static aToken V3 - June 2023
  • Reward Distributor - July 2023

So far, we distributed $363,500 worth of grants.

ERC20 Listings

Certora checked the following ERC20 tokens upon suggestions to enlist them in various markets:

  • sUSD on Optimistic in Aave V3
  • sAVAX on Avalanche in Aave V3
  • cbETH on Ethereum Mainnet in Aave V3
  • stMATIC on Polygon in Aave V3
  • OP on Optimism in Aave V3
  • MAI on Avalanche in Aave V3
  • MAI on Polygon in Aave V3
  • KNC on Ethereum Mainnet in Aave V2
  • GNO on Ethereum Mainnet in Aave V2
  • FRAX on Polygon in Aave V3
  • CVX on Ethereum Mainnet in Aave V2
  • BTCb on Avalanche in Aave V3

Results can be viewed here: https://github.com/Certora/aave-erc20-listing/tree/master/contracts.

Our checks extract valuable information on the behavior and capabilities of the tokens to allow the community to make more informed decisions before approving or declining a token enlistment. For example, our system alerts if any potential fees are taken by the token.

Workshops

In the past 18 months, we conducted 3 workshops to teach a community of independent security researchers more about the Aave protocol, to get them familiar with Aave code, and after supplying them access to the Certora Prover, teaching them how to use it to search for vulnerabilities. The workshops were all recorded and uploaded to Youtube:

As you can tell the last 18 months were extremely intense, however, taking the responsibility to secure the Aave protocol was as satisfying as it was demanding.

Although our engagement period is officially over, we are not disappearing anywhere! We are crafting a new proposal for another year of continuous security for Aave, including community engagement, that we will share with you soon.

3 Likes