Continuous Formal Verification

Governance
1

Summary

A proposal for significantly and continuously improving the security of the Aave platform and the dApps built on top of it, by offering our formal verification and path coverage tooling service to the Aave Platform contributors and the Aave Protocol dApp developers. The initial proposal is for 6 months starting January 2022. A discount price is given for an annual contract.

Background

Aave Security

The Aave Protocol is a fully decentralized system that provides sophisticated tools for accessing liquidity. The protocol’s ongoing management is controlled by a governance protocol that allows external contributions and voting by stakeholders. Such a system opens up the possibility of creating powerful new DeFi protocols built on top of it, without giving up on decentralization.

One of the major risks in managing a complex system of smart contracts is that it is harder to ensure that changes introduced via governance are safe, and that they do not break the behavior of the protocol. While those problems are common to every piece of evolving software, decentralization introduces additional risks.

These risks were highlighted by a recent incident in which a bug was introduced in a Compound governance proposal, leading to huge nonrecoverable financial losses. Of course, such bugs are not exclusive to Compound— they have been affecting many DeFi protocols.

Detecting vulnerabilities before they are deployed is difficult because of the lack of good security tools for smart contract development. Smart contract developers often rely on manual auditing to prevent bugs, but audits are difficult to employ in the setting of ongoing, time-controlled governance proposals. Moreover, even the best auditor can miss critical bugs due to the complexity of the code.

About Certora

Our team consists of 31 experts in smart contract security, formal verification methods, and compilation techniques. 9 of our team members have PhD in formal verification. We have built a world-class and unique developer tool that seamlessly integrates into CI/CD, allowing continuous verification of contract correctness.

We enable companies to “move fast and break nothing”, taking months off of the time to market, by decreasing code audit time. Our product, the Certora Prover, allows both pre- and post-deployment code verification: it statically analyzes the code before it is deployed but also runs on the EVM bytecode of the deployed contracts. The product verifies code by checking that it obeys high-level semantic rules. For example, a rule could assert that the sum of token balances remains unchanged by all operations that do not mint new tokens. A free demo of the Certora Prover can be found here.

Our product is used by the industry’s leading companies (Aave, Balancer, Benqi, Compound, MakerDAO, OpenZeppelin, Sushi and more) and has prevented more than 100 safety-critical bugs, including 20 “solvency” bugs (a bug in which a user can steal money from the contract). Each bug can lead to tens or even hundreds of millions of dollars in losses. The Certora technology has also uncovered critical security bugs in the Solidity compiler itself and in deployed contracts of major DeFi organizations.

Certora and Aave relationship

We have been working with the Aave team since before V2 protocol. We’ve formally verified the various iterations of the AAVE token, and significant parts of the V2 protocol. We found and prevented 6 high severity issues in V2 before deployment, including a solvency bug. We will soon be working on the next major upgrade to the protocol. Our security rules for Aave are publicly available and serve as a useful tool for contract upgrades and integrations. Protocols that integrate into Aave could use these rules and run their code against them to make sure the integration process is smooth. Making this service more accessible is part of this proposal.

Proposal

We propose two approaches to significantly increase the confidence in the platform itself and in the smart contracts built on top of it.

First, we propose to change the project-based relationship of Aave and Certora, to an ongoing relationship, where we will provide ongoing support and rule-writing for Certora Prover on Aave’s code. This service will be provided to all who contribute to Aave’s ecosystem: Aave’s in-house developers, community contributors and dApp developers. This will ensure that the constantly-evolving code of Aave’s platform remains secure, protecting its users’ assets.

Second, we will develop a new symbolic execution tool (path coverage) which will significantly increase the coverage of code areas where we look for bugs, complementing the more focused nature of the Certora Prover. This tool’s results will be visible to all via a unique dashboard we will build. In addition, it will be open-source, so the community could contribute to its development.

The two approaches are complementary: Our continuous rule-writing for the Certora Prover will mathematically prove that critical code areas are secure, while the symbolic execution tool will be more comprehensive, running 24/7 to continuously increase the coverage for specifications that are too complex to prove using the Certora Prover.

In the following sections, we will specify the deliverables of our proposal.

Continuous High-Level CVL rules specification for the Aave Ecosystem Contributors

We will write high-level correctness rules in English and in CVL, Certora’s domain-specific specification language, for DeFi smart contracts built on top of Aave, as well as for the Aave platform itself via its contributors. These rules will be used later for the Certora Prover and the new symbolic execution tool.

In the process of writing the rules, we will perform a code review and identify bugs manually. We will allocate an expert software engineer for the entire period of the contract, dedicated to Aave. Normally, customers wait several months for our services, while here Aave will receive ongoing support. This engineer will update the rules to capture the essential security properties of the Aave Protocol and its derivatives. Also, we will update the rules when bugs are found.

Fitting the DeFi community spirit, we will make the CVL rules open-source, allowing decentralized rule writing and rule auditing. This will allow knowledge-sharing in rule writing between contributors and dApps developers, as different developers could use rules fitting their purposes which were written by others.

Formal Verification of Smart Contracts during CI/CD

The above rules will be used by the Certora Prover, which will be available to all Aave platform developers. Rules can be developed using a new VSCode extension, with tooling to integrate CVL specs to the Solidity code project. The extension will also be able to invoke the Certora Prover, and present an ongoing status of the rules: whether they are proven or violated. When a rule is violated, the extension will return a concrete call-trace showing the input for which the rule is violated, in a view similar to a debugger.

Code Coverage for Smart Contracts

This project is inspired by the Sage Direct Fuzzing Project which prevented million-dollar bugs for Microsoft.

We will develop a new symbolic execution product for increasing code coverage of the Aave smart contracts. For each smart contract, the product will automatically generate inputs, enumerating over time more and more control flow execution paths using SMT solvers, in pre and post-deployment. This complements formal verification when the code is too complex for it or when using it is too labor-intensive.

This is similar to Dynamic Monitoring provided by Forta, however, our tool is different in two aspects: it uses high-level security rules and leverages SMT solvers for triggering rarely executed scenarios. The code developed in this project will be open source to allow contributions from the community. This means that every developer can get access to a security tool for her/his smart contract.

In addition to creating the product, we will create a dashboard that will report the inputs and the paths covered by the different inputs, as well as rule violations that may occur. Also, for each input, we check that every CVL rule holds, which will also be reported.

Measures of Success

Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of Certora Prover are scoped to the provided specification, and any cases not covered by the specification are not currently checked by Certora Prover.

In general, we note that there is no silver bullet in smart contract security and in formal verification specifically. Still, we plan to measure success according to the following KPI: (1) the number of paths covered by the symbolic execution tool, (2) the number of rules formally proved, (3) the number of bugs identified by the Certora Prover before deployment, (4) the number of bugs identified by the path coverage tool, and (5) the number of missed bugs in code analyzed by Certora found by auditors and other means. The numbers will be available on a daily basis.

Certora Services Summary

We offer the following services by the company:

  • We will allocate a dedicated expert software engineer for writing rules for the Aave platform contributors and for Aave dApps as needed for the whole period. We will also allocate a full-time security researcher to review all proposed code changes.
  • We will offer all Aave platform contributors (registered by Aave) access to the Certora Prover SaaS platform to check new and existing rules, as well as provide support for run analysis and creation of new rules.
  • We will develop an open source directed fuzzing engine on top of modern SMT solvers.
  • We will create a cloud-based symbolic execution product that will analyze the Aave platform code and the dApps built on top of it in pre and post-deployment.
  • We will create a dashboard displaying the results of the symbolic execution product, including rule violations and covered paths, visible to all Aave users. Rule violations will be reported automatically to the Aave security team, but not visible to all users to avoid revealing potential exploits.
  • We will create an open-source database of CVL rules and the code they refer to, to decentralize rule writing and promote decentralized contributions to rules.
  • We will create a two-week online course on writing rules. The course will be recorded for availability for all developers.
  • We will hold 2 weekly support Zoom calls for users of the Certora Prover and the new symbolic execution tool.

Pricing

  • The project price is $1,700,000 for 6 months or $3,400,000 for 1 year. For a 6 months period, $1,000,000 is paid in USD and USDC. $700,000 is paid in Aave tokens vested linearly over a year period. A 20% discount is given for an annual contract bringing the total to $2,720,000 for a year.
  • An additional sum of $200,000 will be paid to Certora and purposed for paying decentralized community rule writers. This sum will not be used for any other purpose.
  • The normal price for our services is $70,000 per week for rule writing subject to availability. We are booked 6 months in advance. The SaaS fees are $2000 per month for each user. Here we allow 52 weeks and an unbounded number of users.
8 Likes
2

@Shelly thanks for bringing this forward and thinking about Certora’s and Aave’s relationship in a new way.

Your audits have been a great resource for security in the industry.

Few questions about rules and reporting -

This quote seems to make sense however fails to consider the pace and values of crypto:

  1. What happens if there is high turnover on the Aave team and this information is carried to an external community?
  2. This solution seems very centralized. Is there a way to release these violations to the larger community and incentivize compliance without revealing the exploit? How about a public leaderboard of developer ID’s and noting violations but the actual exploit redacted.

For rules in general - how do you achieve security without becoming too rigid and deterring innovation?

Look forward to your answers!

2 Likes
3

Thank you @fig for the very useful feedback!

It is true that from rule violations one could derive a concrete exploit, and thus withholding information to a select group of users can be problematic.

However, we need to make a distinction between bugs found pre-deployment, and bugs found after the deployment.

There is no problem to show all of the details of the violation if it was found pre-deployment (given that it is fixed in time, of course!).

As for post-deployment, we plan to work with the community to find a disclosure mechanism that ensures a prompt fix to the issue without giving up on decentralization.

1 Like
4

Thanks for sharing @Shelly .
I support this proposal by Certora, for the following reasons:

  • I have firsthand experience working with the Certora team and with others in the ecosystem, and can certify that their are one of the most talented teams out there, specially for their exceptional combination applying formal verification methods and more “traditional” Solidity code reviews.
  • The Certora team is really familiar with all the versions of the Aave protocol, which makes them a perfect fit for the task.

Some questions concerning the proposal @Shelly :

  • The personnel allocation from your side are the software engineer to write rules with contributors and security researcher?
  • The scope is for anything developed on the Aave community during the engagement period?
  • Certora will take care and report to the Aave DAO about the allocation (e.g. developers and projects receiving) of the $200,000?
1 Like
5

Thanks @eboado!

  1. Yes, personnel includes 2 people - a software engineer for writing rules and a security researcher.
  2. Yes. Ideally, the community can decide on prioritization.
  3. Of course - we’ll be happy to work with the Aave DAO on a concrete mechanism for deciding on the teams that will receive grants out of the $200,000 fund.
6

Thanks for bringing this idea @Shelly.

A continuous audit process is a essential security measure for a leading protocol as Aave is. Since nowadays there is no plan for security revisions in a decentralized manner, I believe this proposal is a pretty good starting point of how the community can work altogether to ensure a safe and healthy behavior of the protocol in an ongoing basis and prevent potential vulnerabilities. In addition, I see Certora as the perfect candidate for this purpose given the background and experience on the field.

Just a little thought on my side as a community member regarding the pricing. I am not sure if the service you would provide could be compared to a normal service. Imho reviewing and auditing a popular, battle-tested and familiar project in a day to day basis is not the same as auditing new random projects from scratch. The Aave protocol is well-known for its security and robustness and given that was already audited multiple times in the past I think it could take less effort to assess and review. On the other side, I am aware auditing is a sophisticated and highly complicated thing and there are a bunch of things you can do/give a hand with.

I am not pretty familiar with this kind of services and pricing and don’t want to be misunderstood. I just want to leave this thought and would like to know your opinion about this topic and how do you foresee the work you are willing to do.

7

Thanks @miguelmtz for the feedback!

Our pricing captures 4 value propositions of the proposal for the protocol’s benefit:

  1. For the whole period of 6 months (and 6 months more if decided to prolong), allocate a full time software engineer to write rules with expertise in formal methods and DeFi and a security researcher to review each proposed change.
  2. A comprehensive set of rules for the entire Aave Protocol that would permit continuous guaranteed security and robustness of the protocol even in the presence of changes coming from governance proposals. The idea is that those rules will be checked automatically on changes pushed to the code repository, even for external contributions. Such a set of rules can greatly ease the task of auditing and give greater confidence in the system, especially as complex as Aave’s.
  3. An open source path coverage tool that continuously scans code paths for more complex rules. This is a new offering.
  4. Teaching the community how to write security rules for Aave and rewarding contributors of new rules. The participating people will have full access to the tool.
1 Like
8

Thanks for the reply. I hope the community supports this initiative. Eager to see how your work enhances protocol’s security, fosters adoption and empower users with advanced knowledge.

1 Like
9

This proposal is now live for voting.

Please participate here: Aave - Open Source Liquidity Protocol

10

Following approval of the governance proposal, we are excited to be part of the Aave family. We have closely worked with the Aave dev team since V2, and we are glad to work with the community and the BGD initiative.

Personnel
The following are more concrete details about our joint work going forward:

Itay Grandenwits @itayGradenwits is a security researcher who worked on Aave V3. He is available to help you in reviewing the code changes introduced in new proposals.

Yura Sherman @yuradmt, a security engineer, is available to verify additional properties about the protocol.

Together with Nurit Dor, Itay and Yura, we will review proposed changes to the Solidity code.

In addition, our team will hold office hours every Wednesday at 3:30 pm European time via a zoom link.

Continued Verification
The verification report for Aave V3 is available at https://www.certora.com/wp-content/uploads/2022/02/AaveV3Jan2022-1.pdf. Going forward, we plan to verify more rules. If you would like to suggest more rules this will be greatly appreciated.

Certora Prover Education
We plan to deep dive into Aave V3 core implementation and teach formal verification.

A beginner workshop is scheduled to start on the week of April 25, 2022, on Monday, Tuesday, Wednesday, and Thursday 3 pm-4:30 pm European time. This workshop will provide instructions on the general use of our tool and explanations of Aave V3 implementation and properties. A second workshop, planned for May, will cover advanced topics and additional rules which were verified in V3. A third workshop, planned for summer, will cover new rules written by the community which will be reviewed by both the Aave community and the Certora team, and appropriately rewarded in Aave tokens.

Grants
As part of the proposal, a sum of up to $200K will be distributed to allow contributions from the Aave community for formal verification using the Certora Prover. Grant proposals can be submitted by posting in the forum where the Aave and Certora teams will review them and allocate following it.

Access to Certora Prover and Workshops
If you would like to have keys to access the tool and/or participant in the workshop please email lori@certora.com.

New Products and Early Availability
We are developing a new dashboard for code security. We will share the dashboard proposal in an upcoming office hours meeting

Our new path coverage tool for rules is scheduled to be available during Q2, 2022. We will start by running the fuzzer on the hardest rules from the Aave Protocol V3 verification project and present the findings to the community, following which we will allow the community to utilize the path coverage tool as part of their workflows and build systems freely.

4 Likes
11

Workshop Details

Hi Aave Community,

Now is your chance to learn how to formally verify Aave v3 and beyond! Join the Certora Prover Workshop!

  • New Workshop Dates: 4/27 (Wed) - 4/29 (Fri), 3p-4:30p CET via a zoom link. 4.5 hours total, over 3 days
  • What you will learn:
    • Day 1: CVL Language - writing basic rules and understanding verification results.
    • Day 2: Thinking through properties - thinking about high-level properties while working on a generic liquidity pool.
    • Day 3: Finding real bugs - practice your newly acquired skills on examples based on bugs found in the real-world.
  • Register here and get a key to the Certora Prover before the workshop.
  • Weekly Office Hours: Wednesday, 4:30-5:30p CET
  • Be sure to add the calendar. We will publish more special events here.
    https://bit.ly/38DDqu0

We are excited to work with you!

2 Likes
12

Dates: 4/27, Wednesday -4/29, Friday 3-4:30 pm CET
Preliminary Talks
Understanding the Certora Prover (20 mins) Understanding the Workflow of the Certora Prover - YouTube
CVL: Formalizing DeFi SafetyStart at 7:23:30 Secureum TrustX — Mainnet Room, 21 April - YouTube

Installing the Certora Prover
Grab your key from the email you used to register
This key should not be shared. Follow the installation guide here:
https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html
Run an example to verify a proper set up. Follow our guide here: Running the Certora Prover — Certora Prover Documentation 0.0 documentation

Learning Resources
Certora Tutorials: GitHub - Certora/Tutorials: Practical tutorials of Certora Prover
Certora Documentation: Certora Prover Documentation — Certora Prover Documentation 0.0 documentation
Certora Forum: https://forum.certora.com/

Recordings/Agenda
Day 1: CVL Language - writing basic rules and understanding verification results. recording: Workshop: Aave Community Day 1 4/27/22 - YouTube
Day 2: Thinking through properties - thinking about high-level properties while working on a generic liquidity pool. Workshop: Aave Community Day 2 4/28/22 - YouTube
Day 3: Finding real bugs - practice your newly acquired skills on examples based on bugs found in the real-world. Workshop: Aave Community Day 3 4/29/22 - YouTube
All slides and lessons: GitHub - Certora/Tutorials: Practical tutorials of Certora Prover

1 Like
14

Certora Continuous Formal Verification Report April 2022

We are working on our grant proposal, stay tuned for more in the next couple of weeks.

Summary

We can’t believe it’s already been a month. In the last few weeks, we have created a beginner workshop that was held 4/27-29 with 100 registered Aave community members. We also did a verification of BGD labs streaming treasury contract.

Verification Updates

BGD labs Ecosystem Reserve v2
Described at Aave <> Bored Ghosts Developing (BGD) - #31 by EzR3aL

We have conducted a formal verification and manual audit of the ecosystem reserve contracts. It’s a modified version of Sablier money streaming protocol. The modifications allow Aave treasury to stream funds to recipients without locking them upfront, so that yield can be earned on unvested funds.

The formal verification spec includes 18 rules and invariants. These rules verify conditions like treasury solvency, correctness of withdrawal and so on.

Detailed properties description is on Github.

Certora Prover Education Updates

Certora & Aave held a beginner 3-day workshop that took place 4/27-4/29 with 100 registered Aave community members. The schedule and links to resources and recordings are below

Day 1: CVL Language - writing basic rules and understanding verification results. recording: Workshop: Aave Community Day 1 4/27/22 - YouTube

Day 2: Thinking through properties - thinking about high-level properties while working on a generic liquidity pool. Workshop: Aave Community Day 2 4/28/22 - YouTube

Day 3: Finding real bugs - practice your newly acquired skills on examples based on bugs found in the real-world.

All slides and lessons: GitHub - Certora/Tutorials: Practical tutorials of Certora Prover

Register here and get a key to the Certora Prover.

If you missed the workshop, you can still register to get a key and watch the recordings. We have Office Hours for any questions or ideas you have.

Weekly Office Hours: Wednesday, 4:30-5:30p CET

Be sure to add the calendar. We will publish more special events here.
https://bit.ly/38DDqu0 6

As we wrap up the first month of our proposal, we want to hear from you……Review our work - is there anything the community can review

  1. Please give us feedback on the beginner training here (link to survey)

  2. Feedback

  3. Further suggestions

  4. Thank the community

Thank you to this wonderful community. A special thanks to Stani and Ernesto for always answering our questions.

Email: lori@certora.com

Discord:lorib#1242

Telegram:@lblonn

3 Likes
15

Certora Continuous Formal Verification Grant Plan

Hi everyone, we’re glad to announce our grant plan to the community

Time Frame

Up to 1st of October 2022

Evaluation

Grants will be given to participants who meet the following criteria:

  1. Each participant that contributes at least 3 good rules will receive 2k$. Rules will be counted only if they are verified or uncover an issue in the code.

  2. For every additional rule/invariant or issue found in the process, an additional 0.5k will be rewarded.

  3. Each participant will be limited to a max reward of 10k per project.

How To Participate

If you’re not registered yet, you can fill your details in the following form:

2 Likes
16

Certora Continuous Formal Verification Report May 2022

Hi Aave Friends! Here’s is a peek at what we have been up to in May 2022

Summary

Aave ERC20 Listing Checker

To assist with the token listing process on Aave platform, we designed a specification that helps inspect the suggested ERC20 for certain behaviors. When a token implementation runs against the specification using the Certora Prover, it supplies valuable information on the expected behavior of the asset in a relatively short time.

The specs contain rules to detect supply changes, pause on transfers and transfer tax, among other things. Since these can be potential token features and not bugs, the counterexamples that the Certora prover finds when running this spec should be seen, first and foremost ,as information about the tested token, not as a standard violation or a bug. The idea is that testing the token code against the spec provides knowledge and richer details to the community, so that it can make a more informed decision about the asset.

The repo with the specifications, the inspected contracts and a thorough explanation on the spec and the motive of each rule can be found here.

In our first release we’re happy to share the results obtained by the Prover on the following tokens:

The results for the runs along with their analysis can be found here.

Coming Soon: We will inspect several additional tokens, suggested by BGD, and display the results on a dedicated section in the dashboard. Stay tuned! :slight_smile:.

Grant Plan

During May we’ve announced our grant plan for the community which allows community members to win rewards for their best effort of securing Aave and Aave related contracts. Tweet

First Community Driven Verification Project

Between the 15th-29th of May we launched our first verification project. The goal was verifying the StaticATokenLM.sol contract which is related to the starknet bridge.
Thank you to all the participants and congratulations on your winnings.

Aave Verification Dashboard

We’ve released a dashboard that gathers all the verification efforts done so far on Aave platform.
It features all the specifications written for different contracts and their results, including the Certora generated verification reports for each project.

For the duration of our work with Aave we will maintain the dashboard with the latest specifications and their results.

Certora Keys Distributed

During the past month we’ve handed 25 additional licenses to the community upon requests.

General Note

We are still open for license applications. If you’re interested in helping us securing Aave you can apply in this form for a key.
We encourage every community member to join us on our mission to formally verify Aave contracts and earn some money on the way :upside_down_face:.

You can follow us on twitter to hear about our latest announcements on the grant plan: Twitter
Join us in our discord channel dedicated to the AAVE Verification Project: Discord
And come talk to us every Wednesday on 14:30GMT: Zoom

3 Likes
17

Certora Continuous Formal Verification Report June 2022

Hi Aave Friends! Here’s is a peek at what we have been up to in June 2022

Summary

  • A full verification project was conducted by Certora on 3 governance crosschain bridges - Polygon, Optimism and Arbitrum bridge executors on L2.
    The security report can be found here.

  • A verification and manual review was conducted on the sAVAX oracle adapter for AAVE and the Aave V3 sAVAX listing steward. Our audit found 1 issue in the latter contract, which was fast attended and fixed by BGD.
    The security report can be found here.

  • We concluded the second community driven project. The verification of AStETH on AAVE V2 has finished with 5 participants contributing to the security of the contract, writing a total of 25 quality rules and winning a combined 19.5k$ in grants.
    Certora has also contributed to the security of the AStETH by writing rules and verifying properties. Some of the best rules will be combined with our rules into one complete formal specification. The verification report will be published in the near future.

  • We’ve inspected and released the result of additional ERC20 tokens that were proposed to be listed on the Aave platform using our Aave ERC20 Listing Checker.
    You can read the results on Github or on our dedicated dashboard.

  • More licenses were distributed to the community to reach a total of over 140 keys since the beginning of the Certora-AAVE collaboration!

Governance Crosschain Bridges

Between the 5st-26th of June we conducted a verification project with the goal to secure the following contracts of the governance crosschain bridges:

The contracts are executors for the Aave governance system on the L2 chains.

In this project we’ve verified 24 rules and invariants and found 3 issues.

The spec can be found here, and the security report can be found here.

Our findings include an unexpected revert reason for queued actions, the impossibility to queue 2 identical actions, and a misleading emitting of events in case of a low-level call to a wrong contract.

All these findings have been discussed with the Aave dev team and accepted as low severity issues since they either have workarounds or are edge cases which are unlikely to occur.

Aave V3 sAVAX Listing Stewards

We’ve conducted a manual audit on 2 contracts:

During our audit, we’ve found that wAVAX was forgotten to be configured and set into the same eMode category on the platform. This missing piece was later added to the code before deployment.

You can read about the security audit, our findings and what we’ve checked on our report on the following link.

AStETH on AAVE V2

Between the 12th-29th of June we launched our second verification project. The goal was to verify the AStETH.sol contract, which is the AToken of StETH on the AAVE platform. 5 People helped us secure the contract by writing specifications and verifying them using the Certora Prover. In total 25 quality rules and invariants were generated by the community, resulting in a total of 19.5k$ in rewards given to the participants.

Thank you to all the participants and congratulations on your winnings.

In parallel to the community-driven project, Certora has audited and formally verified a set of rules and invariants. The best rules written by the community will be combined with ours into one complete specification. The report shall be released next month.

Aave ERC20 Listing Checker

In our second release we’re happy to share the results obtained by the Prover on the following tokens:

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

We are still open to licensing applications. If you’re interested in helping us secure Aave you can apply in this form for a key.

We encourage every community member to join us on our mission to formally verify Aave contracts and earn some money on the way :upside_down_face:.

You can follow us on Twitter to hear about our latest announcements on the grant plan: Twitter

Join us in our discord channel dedicated to the Aave Verification Project: Discord

And come talk to us every Wednesday on 14:30GMT: Zoom

3 Likes
18

Thanks for being consistent with the updates @MCERFSR - getting a reply in so you can share the next one :slight_smile:

19

Thanks @0xbilll :smiley:

Certora Continuous Formal Verification Report July 2022

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

Summary

  • Another community driven project was launched and finished this month! The verification of AAVE Token V3 is over, with 25 participants contributing to the security of the contract and 19 participants submitting their specifications, writing a total of 275 security rules.
    Certora has also contributed to the security of the AAVE Token V3 by writing nearly 40 rules and verifying properties. One of our properties uncovered an issue that resulted in a precision loss of delegated balance. The problem was acknowledged by BGD and handled promptly.
    Currently the rules submitted by the community are being processed in order to determine the deserved grants for each participant. In addition, the best rules written by the community will be combined with our rules into one complete formal specification. The verification report will be published in the near future.

  • A verification and manual review of 7 token listings were performed on 3 different tokens on 4 distinct markets: sUSD listing on Optimism, MAI listing on Avalanche, Fantom and Polygon, and FRAX listing on Avalanche, Fantom and Polygon. Our security checks found 2 issues in the MAI listings, which were fast attended and fixed by BGD.

  • As part of EthCC week we’ve held an in-person workshop whose goal was to assist people in writing specifications for the new AAVE Token contract (AAVE Token V3), and engage in future projects for the benefit of Aave security.
    The workshop was live streamed and recorded. You can watch the entire workshop or chosen lessons at the following link: Formal Verification for Fun and Profit

  • During this month, we started a collaboration with Secureum. The goal of the collaboration is to engage more smart contract security community members in the security of the Aave ecosystem. So far, over ten people contributed to the verification of AAVE Token V3. The Secureum participants will continue to work with Certora to ensure the safety of the community projects.

  • During August, we will be launching a new Aave community formal verification grant. The new contract to be verified is the Aave-Starknet bridge on the Ethereum side. Stay tuned to our channels if you’re interested in engaging in the security of this contract.

AAVE Token V3

Between the 1st-23rd of July we conducted a verification project to secure the following contracts of the AAVE Token V3:

The contracts implement an ERC20 that is destined to be used as a governance token for the Aave governance system on Ethereum.

In this project we’ve verified 37 rules and invariants and found 1 issue.

The spec can be found here.

Our finding catches an unintentional precision loss of delegated balance upon token transfer.

This finding was discussed with Aave’s technical contributor BGDLabs and the issue was fixed by fine-tuning the relevant properties and correcting the code.

Aave V3 Listing Stewards and Payloads

During the month of July we’ve reviewed the listing of 3 tokens on several different markets:

In our security checks, we found that the specified underlying asset for MAI in the Avalanche listing steward referred to a relay MAI, a “synthetic” token minted by the relay bridge which was in common use before MAI officially deployed on Avalanche. BGD were quick to confirm and fix the issue. In addition, we’ve noticed that the configuration values for the assets were in disagreement with the snapshot decision, which led us to a discussion about the parameters values of each token on each market with BGD. Raising this concern resulted in the realization that MAI should also be listed as a collateral asset in Polygon due to sufficient liquidity on this market.

EthCC Workshop

Between the 21st-23rd of July we conducted a workshop on formal verification called ”Formal Verification for Fun and Profit”. The workshop was targeted at both beginners and advanced smart contract security professionals with a main objective of assisting people to write formal specifications and engage with the Aave ecosystem’s security.

In the first couple of days we taught the fundamentals of formal verification - approach security by thinking about properties, capabilities and syntax of the Certora prover, correct formulation of rules and invariants, and ways to evaluate the quality of one’s work. On the third day we put things into practice by getting to know the AAVE Token V3 code base, discussing the properties of the system, and assisting with rule writing.

The workshop drew and assisted over 10 community members in writing specifications for the new AAVE token contract.

A recording of the workshop can be found on our youtube channel.

General Note

We are still open to licensing applications. If you’re interested in helping us secure Aave you can apply in this form for a key.

We encourage every community member to join us on our mission to formally verify Aave contracts and earn some money on the way :upside_down_face:.

You can follow us on Twitter to hear about our latest announcements on the grant plan: Twitter

Join us in our discord channel dedicated to the Aave Verification Project: Discord

And come talk to us every Wednesday on 14:30GMT: Zoom

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