[ARFC] Continuous Security Proposal Aave <> Certora

Governance
1

Title: [ARFC] Continuous Security Proposal Aave <> Certora

« post updated »

Author: @Shelly - Certora

Date: 2023-12-07

Summary

We offer to extend the existing formal verification and manual review services and provide additional security services:

  1. Governance proposal reviews - Review every governance proposal in the on-chain stage as suggested by BGDLabs.
  2. We will assist Aave and BGD in reviewing Immunify bug bounties per request.

This proposal asks for a 1-year duration with a budget of $1.5m, starting from the 14th of September 2023.

Motivation

During the 18 months of services, we have reviewed 169 smart contacts consisting of over 51,289 Solidity lines. We have prevented 28 significant bugs. Full breakdown of our work can be found in this spreadsheet.

Continuous Formal Verification (Auditing and Formal Verification integrated into CI)

Following the success of the collaboration in the last 18 months, we offer to continue this service in the same format - new code is formally verified and manually reviewed. Our open-source CVL specification rules are checked using the Certora Prover and become publicly available when the code is released. The formal tests are also integrated into Aave’s CI system to continuously check changes introduced into the code. Reports are delivered upon demand at the end of each project. We have recently released a free version of the Certora Prover and the community can use this to validate the outputs.

The Aave and BGD teams will play a key role in rule writing going forward. These teams are highly technical and have insights into high-level properties of the protocol. Our team will review these rules and ensure the Certora Prover can formally prove these rules or find a bug. Our team will add more rules and manually review the code.

Governance Proposal Review

Following BGD’s suggestion to add a third party to the governance proposals verification process, we will allocate a dedicated team to review each proposal on the on-chain stage within 3.5 days.

Each proposal’s payload will be reviewed by the dedicated team, and we will verify that it does what it’s supposed to do according to its description/AIP. We will also check that there are no unwanted effects on the codebase, which is supposed to stay unchanged.

Our job will be done after a review by BGD at an earlier stage. BGD will also assist with onboarding to guarantee the highest quality of service.

Incident Investigation Support Services

Triaging and validating all the incoming bug reports for a massive protocol, such as Aave, can be highly time-consuming and distracting for the developing entities. Many of the reported issues turn out to be benign. However, at the time of the report, the severity and feasibility of bugs are still unknown. Therefore, it is crucial to investigate them with full seriousness and urgency. We offer to establish an incident investigation support team available 24/7 to support emergency cases. In every incident, we will write a rule that confirms or rejects the existence of a bug and later use it to test the validity of the fix. After every incident, we will update the specifications and incorporate the new tests in the CI.

In past commitments, we have played a crucial role in two critical incident responses. In one case, we concluded that there was no bug in the system. In another case, we identified a missing rule, wrote it, and used it to catch a tricky bug in the suggested fix before the code was deployed.

Specification

The annual price for the project is $1.5M: $1M is paid in GHO vested linearly over one year, and $500,000 is paid in Aave tokens vested linearly over one year. A 30-day termination is possible after a vote. We reduced the price of $2.7M from last year to reflect the bear market and inlined with the reduced project review capacity.

The Aave and the BGD team will also assist by writing their CVL rules.

Next Steps

  1. Gather community feedback on this ARFC.
  2. If consensus is reached, escalate this proposal to ARFC snapshot stage.
  3. If ARFC snapshot outcome is YAE, escalate to AIP stage.

Disclaimer

Certora is presenting this ARFC independently and is not compensated by any third party for creating this ARFC.

Copyright

Copyright and related rights waived via CC0.

12 Likes
2

Certora is a great service provider for the AAVE DAO. In general, I am in favor of this proposal.

Re: Price
The payment for ALL service providers should be done in GHO and avoid using more AAVE tokens from the treasury.

Question for a community expert, is there a general rule for using AAVE tokens for SPs?

3 Likes
3

Super glad to see the Certora team submit a renewal proposal and we commend them for decreasing quite drastically given market conditions. A few comments we had were would the team be open to accepting a portion of their salary vested in GHO? Seems like some better alignment there possibly.

Also, could you elaborate a bit more in how BGD and Certora will work together in this proposal?

4

Part of our scope of engagement with the Aave DAO is to evaluate, coordinate with, and be the point of contact for security partners like Certora.

Given the history and performance of Certora on Aave and having worked with the team for the past years, we would like to say to the community that we firmly believe a renewal with Certora is a really good choice as a security partner.

The rationale of it is the following:

  • First of all, Certora has one of the best teams of security researchers in the space, not only in regards to their specialization (formal methods and verification techniques) but also holistically in the security of smart contracts and DeFi systems.
  • The technical contributors to the Aave DAO (us included) require quite frequent flexibility in terms of availability, and Certora has always fulfilled their obligations on the previous engagements.
  • Certora has always shown extra involvement with Aave, for example by always improving sets of properties, even when the project was considered as finished by the development team.
  • As we commented on our active Phase 2 scope, we believe Certora can be a good candidate to have a different party reviewing on-chain proposals. This is highly specialized BGD’s expertise at the moment, but we think that helping onboard a different party will give even more resilience to Aave.

To answer questions raised by the community, our collaboration with Certora will be similar to their previous engagement, with the following changes:

  • We will make an effort from our side to onboard them on on-chain governance proposal reviews.
  • We will act as coordinators of all Aave security needs of which we have visibility, trying to define a clear pipeline to optimize review time and consequently, delivery.
  • We have noticed that to have the best results, development teams contributing to Aave should be more involved in the formal verification procedures, by progressively integrating them into the development flow itself. This is something we started doing on BGD from Phase I, but we will keep improving.
8 Likes
5

Hey @PGov, @ApuMallku, thanks for your questions :slightly_smiling_face:
Let us refer to each question:

As a long-time contributor to the ecosystem, Certora is a big believer in the Aave project. In the past 2 engagements, we included a portion of the compensation (~30%) in AAVE tokens to put the money where our mouth is. We think that getting a portion in AAVE best aligns Certora with the protocol’s success. We want to stress out that we kept all our AAVE tokens since our first engagement.

With that said, if the community is not keen on spending more AAVE treasury tokens for service providers, we’re willing to accept GHO instead of AAVE tokens.

To answer your question directly - with BGD being a central entity that builds and maintains a considerable portion of the ecosystem, our collaboration with them will clearly be substantial.

  1. BGD took on itself to make a series of improvements for Aave v3 as a service provider in the upcoming months. We will consult and review all of these crucial and delicate changes to the core logic of the protocol with security in mind.
  2. Any new components developed by BGD, like the killswitch and potentially others, will be thoroughly reviewed by us upon request.
  3. We will take the responsibility of reviewing every on-chain governance proposal raised on the protocol. In the process of passing the baton, BGD will onboard us and later support us upon request to ensure a top-quality review.
  4. BGD also acts as a first responder for reports of live bugs via immunify and other channels. During the engagement, we will be available 24/7 to examine, consult and review any bug report and suggested patch as per BGD’s demand.

We would like to stress, however, that we’re offering our services to the DAO. This means that we are looking to consult and perform security reviews for every provider developing for the benefit of the DAO. This includes Aave company and additional smaller developing entities. We encourage any provider and developer that got community approval for their project to contact BGD as a security resource coordinator and inquire regarding our availability to perform a security review.

2 Likes
6

Hi @Shelly,

It appears that this proposal does not comply with the ARFC proposal format and should be reworked to reflect the correct template. The details regarding the correct format can be found here. The most recent ACI or Chaos Labs proposal can be used as a guide.

Requesting AAVE as payment is a hard “No” for us. Please do amend the proposal to remove AAVE and replace it with GHO as payment. Ideally, all or at least >50% of the funding should be nominated in GHO. Outside of this, requesting USDC should state which Aave deployment this will be drawn from, v2 (aUSDC) or v3 (aEthUSDC), otherwise, it is hard to budget without such details.

This is applicable to all Service Providers, with Chaos Labs, Gauntlet, ACI, Karpatkey, and TokenLogic not receiving payment for services rendered in AAVE, it is a moot point. Certora should not receive AAVE.

5 Likes
7

The ACI is supportive of this proposal from Certora, who have been an important service provider for the past years.

We also do not have an issue with Certora being paid in AAVE.

We suggest using the following edits for the proposal and will be happy to support this proposal with Skyward.

Title: [ARFC] Continuous Security Proposal Aave <> Certora

Author: @Shelly - Certora

Date: 2023-12-01

Summary

We offer to extend the existing formal verification and manual review services and provide additional security services:

  1. Governance proposal reviews - Review every governance proposal in the on-chain stage as suggested by BGDLabs.
  2. We will assist Aave and BGD in reviewing Immunify bug bounties per request.

This proposal asks for a 1-year duration with a budget of $1.5m.

Motivation

During the 18 months of services, we have reviewed 169 smart contacts consisting of over 51,289 Solidity lines. We have prevented 28 significant bugs. Full breakdown of our work can be found in this spreadsheet.

Continuous Formal Verification (Auditing and Formal Verification integrated into CI)

Following the success of the collaboration in the last 18 months, we offer to continue this service in the same format - new code is formally verified and manually reviewed. Our open-source CVL specification rules are checked using the Certora Prover and become publicly available when the code is released. The formal tests are also integrated into Aave’s CI system to continuously check changes introduced into the code. Reports are delivered upon demand at the end of each project. We have recently released a free version of the Certora Prover and the community can use this to validate the outputs.

The Aave and BGD teams will play a key role in rule writing going forward. These teams are highly technical and have insights into high-level properties of the protocol. Our team will review these rules and ensure the Certora Prover can formally prove these rules or find a bug. Our team will add more rules and manually review the code.

Governance Proposal Review

Following BGD’s suggestion to add a third party to the governance proposals verification process, we will allocate a dedicated team to review each proposal on the on-chain stage within 3.5 days.

Each proposal’s payload will be reviewed by the dedicated team, and we will verify that it does what it’s supposed to do according to its description/AIP. We will also check that there are no unwanted effects on the codebase, which is supposed to stay unchanged.

Our job will be done after a review by BGD at an earlier stage. BGD will also assist with onboarding to guarantee the highest quality of service.

Incident Investigation Support Services

Triaging and validating all the incoming bug reports for a massive protocol, such as Aave, can be highly time-consuming and distracting for the developing entities. Many of the reported issues turn out to be benign. However, at the time of the report, the severity and feasibility of bugs are still unknown. Therefore, it is crucial to investigate them with full seriousness and urgency. We offer to establish an incident investigation support team available 24/7 to support emergency cases. In every incident, we will write a rule that confirms or rejects the existence of a bug and later use it to test the validity of the fix. After every incident, we will update the specifications and incorporate the new tests in the CI.

In past commitments, we have played a crucial role in two critical incident responses. In one case, we concluded that there was no bug in the system. In another case, we identified a missing rule, wrote it, and used it to catch a tricky bug in the suggested fix before the code was deployed.

Specification

The annual price for the project is $1.5M: $1M is paid in USDC vested linearly over one year, and $500,000 is paid in Aave tokens vested linearly over one year. A 30-day termination is possible after a vote. We reduced the price of $2.7M from last year to reflect the bear market and inlined with the reduced project review capacity.

The Aave and the BGD team will also assist by writing their CVL rules.

Next Steps

  1. Gather community feedback on this ARFC.
  2. If consensus is reached, escalate this proposal to ARFC snapshot stage.
  3. If ARFC snapshot outcome is YAE, escalate to AIP stage.

Disclaimer

Certora is presenting this ARFC independently and is not compensated by any third party for creating this ARFC.

Copyright

Copyright and related rights waived via CC0.

2 Likes
8

Certora has been critical for security over the past months. Security is important when handling billions of dollar. So i am supportive, but i would also like to ask Certora to at least reduce the amount of Aave and take GHO instead. If we are about to reduce Aave rewards for staker to reduce sell pressure and use this scarce asset for other important things then we should also do this with SP.

Others have already showed their committment why make an exception here.

3 Likes
9

There should be a general rule to not pay SPs with AAVE tokens to avoid favoritism

1 Like
10

We support Certora’s renewal and value the role they play within the Aave ecosystem. Having a dedicated security team to review every on-chain payload is a great value add to Aave and its stakeholders.

1 Like
11

We are also in support of renewing the partnership with Certora. The community has notably appreciated their role as a security partner for Aave DAO. Their contributions have been particularly vital in key areas such as the v3 deployment, the GHO token, the safety module, and their proactive response to live security incidents. This track record underlines the importance of continuing AAVE DAO’s collaboration with Certora.

1 Like
12

In my opinion, the current argument of not allocating AAVE for long-term service providers is becoming pretty unreasonable, for the following aspects:

  • AAVE is governance power in the Aave ecosystem, distributed via different channels. The diversity of these channels should grow in the future, not be reduced, because the goal is to have people meaningfully involved in the protocol having voting and proposition power.
    With service providers collaborating with the Aave ecosystem for a long time, I see little to no case to argue against them having power that could be used or delegated.
  • The budgets become de facto reduced because it is pretty rare (I don’t know if it happened before) for a service provider to sell all the AAVE systematically as it is received/streamed. That is the reason why the AAVE allocation should be in the AAVE denomination, no matter if the reference for the proposer is fiat currency value.
  • Personally, I think the payment to service providers in GHO at the current stage is not reasonable, not for the interests of the service provider, but GHO’s: it creates sure sell pressure of GHO while is in the process of peg built-up, as the stablecoin component needs to be used for operations, and currently is far from trivial to use GHO as medium of exchange.
    However the community seems to have some kind of strong stance on this, which I respect.

Disclosure. I’m part of BGD Labs, a service provider that received AAVE in the past, but my comment is as an AAVE holder and community member

2 Likes
13

The argument doesn’t make any sense. If SPs are not going to sell AAVE tokens, why would they sell GHO? I agree that the scenario is not ideal having not the peg not been restored yet. But if we want SPs with skin in the game, the best option is to pay them with GHO. If they want to have a voice on the governance, they can buy AAVE on the open market as every holder did.

2 Likes
14

Regarding your first point, the reason is that if the objective is receiving and selling AAVE, there is no point in requesting AAVE to start with. Apart from being weirdly exposed to a 1-year stream price-wise.

About the argument of “skin in the game”, not sure why giving GHO makes any difference. Having skin in the game is creating a payment stream that can be canceled, reputation alignment, and if analyzing it price-wise (which I don’t think is so legit), as I mentioned the fact of having a stream of AAVE over a year.

Not sure why there is even a discussion of service providers buying AAVE to participate in governance: contributing professionally to Aave has no relation with any kind of investment strategy.

Then if you have some argument saying that people who buy AAVE from the market have more governance legitimacy than contributors giving direct value, I respect it, but I don’t agree, as I think there should be no comparison like that.

15

I hear you, but ultimately there are better ways of using AAVE with a proper treasury management strategy @karpatkey_TokenLogic and build a robust and diversify treasury than using AAVE for paying service providers; we have enough hard cash (stablecoins) for paying providers that we don’t need to use our token for it like other DAOs does.

2 Likes
16

Thanks @bgdlabs, @TokenLogic, @ACI, @EzR3aL and @WintermuteGovernance for your support, questions and help with the template.

Regarding the Gho Vs. AAVE payment, we see that there’s quite a big disagreement regarding the payment tokens, and we understand your concern. Note that we offer a vesting mechanism with a cliff of 1 year. We are willing to extend this clif period to 18 months to prove our intentions. We would like to emphasize again that we haven’t sold any AAVE we received since the 13 of March 2022, and we have no intention to do so either.

We have no preference so we leave this for the DAO to decide. As a treasury management SP, we trust you, @TokenLogic, to choose the aUSDC pool/asset that makes the most sense to allocate money from.

We would also like to stress that this proposal is a continuation of our previous engagement with the DAO, meaning that the start date will be Sept 14th, 2023, a day after the previous engagement ends. We’ve been working with Aave company since September on a regular basis and therefore this proposal includes retroactive compensation.
We added the exact engagement dates to the original post.

2 Likes
17

We support this proposal as Certora is a valuable partner with a pristine tracking record with Aave DAO. Their willingness to accept GHO as payment shows their commitment to Aave Ecosystem.

Would you mind clarifying whether the expectation is to get a proportional one-time compensation for the services provided since September 14th with a stream for the remaining of the service period, or a pro-rata streaming ending on Sep 13th 2024?

1 Like
19

Thanks for the question @Karpatkey.

The retroactive compensation will be charged as part of the stream, meaning that we will stream the entire sum between the execution date of proposal and the end date - 13th of September 2024. So basically the payment for the work since September will be stretched across the entire engagement period.

3 Likes
20

Following the discussions in the past week and the overall support for our proposal, we decided to escalate this ARFC to the snapshot stage.

In order to be fully transparent - we decided to change the original payment plan and propose compensation in GHO instead of USDC in a ⅓-⅔ proportion, both linearly vested over a period of one year.

Snapshot is now live. Voting will start in ~18 hours.

2 Likes
21

Snapshot is now officially over, supporting our full proposition.
We are already preparing the on-chain proposal, which we expect to go live in the next couple of days.
Please stay tuned, we’ll update once we submit an official proposal on-chain.
Thanks everyone for your immense support!

2 Likes