Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Governance
19

Hello Aave friends :wave: :grinning:

September 13th marked the end of our annual engagement with the community. Lately, we’ve been working on a few high profile contracts - Governance V3, Crosschain Infrastructure and the Gho GSM, which are all in final stages of review.

Until the reports are ready to be shared, we decided it’s a good time to list all the work that’s been done in the past 18 months as part of our continuous service to Aave.

Contracts Reviewed

A list of all the major projects we reviewed:

  1. aStETH on Aave V2 (Lido) - formal verification + manual review - Link to Spec, Link to Report - 5-26 June, 2022.
  2. Governance Crosschain Bridges to L2 - formal verification + manual review - Link to Spec, Link to Report - 5-26 June, 2022.
  3. sAVAX Listing Steward on Aave V3 Avalanche - manual review - Link to Report - 21-28 June, 2022.
  4. sUSD Listing Steward on Aave V3 Optimism - manual review - Link to Report - 21-28 June, 2022.
  5. FRAX Listing Steward on Aave V3 Avalanche, Fantom, Polygon - Link to Report - 21-28 June, 2022.
  6. MAI Listing Steward on Aave V3 Avalanche, Fantom, Polygon - Link to Report - 21-28 June, 2022.
  7. BTC.b Listing Steward on Aave V3 Avalanche - Link to Report - 21-28 June, 2022.
  8. AAVE Token V3 - formal verification + manual review - Link to Spec, Link to Report - 15 July - 10 August, 2022.
  9. Aave-Starknet Bridge (the L1 Ethereum side) - formal verification + manual review - Link to Spec, Link to Report - 15 August - 5 October, 2022.
  10. Aave Governance Level 2 Update - formal verification + manual review - Link to Spec, Link to Report - 31 August - 11 September, 2022.
  11. Reward Aware Token - formal verification + manual review - project was paused by the developing team - 15 September - 20 December, 2022
  12. Aave Proof of Reserve - formal verification + manual review - Link to Spec, Link to Report - 6 November - 22 November, 2022.
  13. Chain Link Synchronicity Price Adapter - manual review - Link to Report - 14 November - 8 December, 2022
  14. Aave Core V3.0.2 (update before deploying on mainnet) - formal verification + manual review - Link to Spec, Link to Report - 17 November - 15 December, 2022.
  15. Staked Token V1.5 - formal verification + manual review - Link to Spec, Link to Report - 7 December - 10 March, 2023.
  16. Rescue Mission Phase 1 - formal verification + manual review - Link to spec, Link to Report - 6-12 January, 2023.
  17. Static aToken V3 - formal verification + manual review - Link to Report, specs will be published soon - 18 January - 31 March, 2023.
  18. Gho Stablecoin - formal verification + manual review - Link to Spec, Link to Report - 30 January - 28 February, 2023.
  19. PR#820 for Aave V3 Core - manual review - Link to Report - 3-15 March, 2023.
  20. Staked Token V3 - an adaptation of formal specification from Staked Token V1.5 - Link to Spec - 18-26 July, 2023.
  21. aAAVE With Delegation - an adaptation of formal specification from Staked Token V1.5 - Link to Spec - 13-20 August, 2023.
  22. Governance V3 - formal verification + manual review - 16 April - present - currently in progress.
  23. a.DI - formal verification + manual review - 16 April - present - currently in progress.
  24. Gho GSM - formal verification + manual review - 27 July - present - currently in progress.

A total of 8 High severity, 6 Medium severity, and 27 Low severity issues (not including the projects currently in progress).

Community Security Reviews

We conducted several community FV reviews as an extra layer of defense after professional review. The following contracts were released for community review (the products of the community reviews are incorporated in the official reports at the above list):

  • staticATokenLM (old) - May 2022
  • aStETH - June 2022
  • AAVE Token V3 - July 2022
  • Aave-Starknet Bridge - September 2022
  • Static aToken V3 - June 2023
  • Reward Distributor - July 2023

So far, we distributed $363,500 worth of grants.

ERC20 Listings

Certora checked the following ERC20 tokens upon suggestions to enlist them in various markets:

  • sUSD on Optimistic in Aave V3
  • sAVAX on Avalanche in Aave V3
  • cbETH on Ethereum Mainnet in Aave V3
  • stMATIC on Polygon in Aave V3
  • OP on Optimism in Aave V3
  • MAI on Avalanche in Aave V3
  • MAI on Polygon in Aave V3
  • KNC on Ethereum Mainnet in Aave V2
  • GNO on Ethereum Mainnet in Aave V2
  • FRAX on Polygon in Aave V3
  • CVX on Ethereum Mainnet in Aave V2
  • BTCb on Avalanche in Aave V3

Results can be viewed here: https://github.com/Certora/aave-erc20-listing/tree/master/contracts.

Our checks extract valuable information on the behavior and capabilities of the tokens to allow the community to make more informed decisions before approving or declining a token enlistment. For example, our system alerts if any potential fees are taken by the token.

Workshops

In the past 18 months, we conducted 3 workshops to teach a community of independent security researchers more about the Aave protocol, to get them familiar with Aave code, and after supplying them access to the Certora Prover, teaching them how to use it to search for vulnerabilities. The workshops were all recorded and uploaded to Youtube:

As you can tell the last 18 months were extremely intense, however, taking the responsibility to secure the Aave protocol was as satisfying as it was demanding.

Although our engagement period is officially over, we are not disappearing anywhere! We are crafting a new proposal for another year of continuous security for Aave, including community engagement, that we will share with you soon.

3 Likes