Security and Agility of Aave Smart Contracts via Continuous Formal Verification

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

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

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

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?

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.

3 Likes

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

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

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

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

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

2 Likes