Continuous Formal Verification

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

@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

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

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

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.

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.

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

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

This proposal is now live for voting.

Please participate here: Aave - Open Source Liquidity Protocol

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

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

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

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

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

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 (worth stating the net value?).

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