Continuous Formal Verification

Governance
21

Certora Continuous Formal Verification Report September 2022

Hi, Aave Friends!

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

Summary

  • We have released the results of the Aave-Starknet Bridge community verification project! A total of 11 participants contributed over 150 rules and uncovered 1 issue.
    More stats and details below.
    The Certora team also contributed to the bridge’s security by verifying properties and catching an additional two issues.
    The issues were acknowledged by BGD and fixed where appropriate.
    The verification report can be found here.

  • We have reviewed BGDLabs’ practical plan to adjust the requirements of Level 2 governance proposals. The carefully reasoned and detailed plan was raised as RFC in the Aave forum, and the repository containing the actual contracts can be found here.
    Certora found four low severity issues that were addressed and fixed by BGD in later commits. The report can be found here.

  • We are working in collaboration with the Aave development team to review and verify a new set of contracts that constitutes a new feature for the Aave platform. We’re excited to share more with you as the collaboration progresses.

  • In the following month we will raise a proposal to continue our collaboration with Aave for a period of a full year. Our proposal includes access to and usage of new tools, continuing the Aave community grants program we have been managing, and 6 R&D personnel all dedicated to securing Aave.
    Watch this space for updates or check out our discussion page to take part in the conversation.

Aave-Starknet Bridge

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

  • We had 15 community members reviewing the code, asking questions, and discussing functionalities.

  • 11 out of the 15 participants submitted formal specifications with a total of 165 properties.

  • Out of the 165 correctness rules, 104 rules passed our professional review, earning grants for their authors. This is an incredible effort by the community!

  • The top community correctness rules joined Certora’s properties in the final specification, increasing overall coverage.

  • The participants who submitted specs won a combined sum of $57.5k, with the top 2 contributors winning $8k each. Congratulations!

Governance-V2 Update

Between the 31st of August to the 11th of September we conducted a verification project to secure the following contracts of the plan to update the requirements of Level 2 governance proposals:

The contracts implement concrete modifications to the governance Level 2 requirements through payloads and a new long executor contract. They also enable a boost of the Level 2 proposal by voting on a Level 1 proposal to use the treasury reserve in favor of that Level 2 proposal.

Following our review, we suggested that BGDLabs add several simple validity checks to the executor, which prevents proposal requirements having undesired values.

General Note

In the upcoming month we will raise a new proposal on the Aave governance system to renew and continue the Aave <> Certora collaboration for a period of an additional year.

You can follow the new proposal and discussion around it on the following link: Security and Agility of Aave Smart Contracts via Continuous Formal Verification.

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