Continuous Formal Verification

Governance
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