Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Governance
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