Security and Agility of Compound Smart Contracts via Continuous Formal Verification

Proposals
1

About the Compound System

Compound’s contracts implement an algorithmic, autonomous money market protocol that has been innovating in the lending space since its inception. The smart contract Solidity codebase is written in a clean and sophisticated way. From our experience, the Compound team invests a massive effort in proper system design before the code is even written, using a security-first approach. The R&D team includes some of the best engineers in the space

About Compound Security

The Compound team deploys several complementary techniques to improve code security:

  1. Various techniques for scenario-based testing and fuzzing have been implemented.
  2. The protocol engages with top auditing firms to review each code change.
  3. Starting in 2018, the Compound team has been working with Certora on formally verifying the code before it is deployed. Formal verification techniques have been used to secure hardware and safety-critical systems across various industries. The Certora Prover plugs into your normal development pipeline, and the formal verification process itself is useful for bug finding before and after manual auditing. In the process, Compound and the Certora teams wrote formal specifications of the code and used the Certora Prover to prove the rules mathematically. When the property does not hold, the Certora Prover generates a test case indicating a scenario in which the property is violated. This test case indicates a bug in the code or the property.

The theme of this proposal is making the tool available to the whole Compound community, including limited access to the source code. We want to allow everybody to have the same access to Prover as the Compound internal team and the Aave community.

By their very nature, complex systems are susceptible to bugs, and this remains true even of carefully planned and executed protocols like those authored by Compound. Bugs in Compound code and governance proposals have been a source of vulnerability for the protocol. For example, a bug in proposal 62 resulted in the distribution of extra COMP awards, and a bug in proposal 117 introduced a buggy oracle, causing the ETH markets to be paused.

Certora has developed a unique domain-specific language, the Certora Verification Language (CVL), for expressing high-level DeFi properties. Certora has also developed a unique product, the Certora Prover, which statically proves that smart contracts obey properties written in CVL. The Prover is integrated into CI/CD pipelines and allows a developer to ensure that changes to the code do not violate the specified properties. Notably, the Prover can perform these checks with every change to the code, both before and after manual audits. A whitepaper of the technology is available here.

We have been working with the Compound team almost since its inception. Originally, we formally verified the first Price Oracle implementation. Using the Certora Prover tool, we found a subtle bug after a third party audited the contract. The part that we did not verify, the MoneyMarket contract, was later found to contain a serious vulnerability in the liquidation function, potentially breaking the protocol’s solvency, allowing an attacker to steal money from the contract. Compound then asked us to help formally verify a sophisticated bugfix, which aimed to block potential exploits. We have written rules for that purpose, showing that no code paths can trigger the exploit.

Ten engineers wrote a total of 80 CVL rules for Compound Code. The rules are available in the following repos: CompoundV2, CompoundV2 Open Oracle and CompoundV3.

Since 2018, the tool has revealed critical issues in Compound Finance, allowing them to be addressed and preventing potential discovery and exploitation in the wild. These bugs are really hard to detect by humans. The Full reports of our past verification projects and findings are available for CompoundV3 and CompoundV2.

We propose to improve the security and agility of the Compound protocol in three ways:

(1) By granting access to the Certora Prover to anybody checking the Compound code. This includes accessing the Certora Prover’s source code under NDA.

(2) By allocating a team of 3 Certora security engineers for 12 weeks per annum to review code changes and propose new correctness rules.

(3) By creating a community of security researchers to review code changes and propose new correctness rules.

Every code change and governance proposal will be reviewed by both internal and external teams using the Certora prover to prevent bugs when the code is upgraded.

A similar service is currently active with Aave: twenty external researchers have contributed 380 rules defining security properties for Aave smart contracts. We prevented six critical bugs and wrote over 500 correctness rules.

Read more about the Aave verification community in the Secureum articles - Aave-Certora-Secureum: A DeFi Security Collaboration part 1 and part 2.

About Certora

Our technical team of over 90 employees comprises formal verification and static analysis experts, security engineers, and security researchers. Many have PhDs in their fields, decades of security experience, and a strong history of significantly increasing the security of the most significant protocols in DeFi, such as Aave, Balancer, Bancor, Compound, Euler, MakerDAO, OpenZeppelin, TrueFi, and others.

Services Provided by Certora

If this proposal is accepted, Certora will provide the following services:

  • We will create a two-week online course on writing rules for the Compound Protocol. The course will be recorded and available to all developers.
  • We will hold weekly office hours via Zoom for users working on Compound verification.
  • We will release a tool for converting CVL rules to Foundry tests. This will allow using the CVL rules for unit testing and fuzzing with Foundry. The first version will support CVL invariants.
  • We will engage with ChainSecurity, Code4rena, Sherlock, Macro, OpenZeppelin, Secureum, SigmaPrime and Spearbit to create a community of security researchers who will review changes to the Compound code and propose new rules. Certora will pay for the engagement with the community a total of $200,000 from the Certora budget.
  • The Certora team will create a mirror git repository for the source code for the Certora Prover. Anybody in the Compound Community can get limited and revocable access to the repository, provided they sign the appropriate NDA. This addresses Compound’s concern about the availability of the Certora Prover code.
  • We will allocate as many keys as needed to security researchers working on Compound. Certora will cover cloud computation time.
  • We will allocate a team of three Certora security engineers to write rules for up to 12 weeks. Compound’s community will determine weeks. This team will review the code and community rules and suggest new rules.
  • One of the challenges in formal verification is coming up with a good formal specification; therefore, we released an open-source tool called Gambit for mutation testing in Solidity code. This tool will be used to review specifications written by the community. We will apply this tool to check the coverage of the rules developed by the community and the Certora team.

Pricing

The proposed price for the project is $1.5M per annum. A termination of the agreement will be available through governance voting given a 30 days notice.

Payment method:

$1.0M USD/USDC vested linearly over one year, and $0.5M worth of COMP vested linearly over one year, with a 1-year cliff to show our long-term alignment with the community.

Price Breakdown:

Regular price for SaaS customers of the Certora Prover is $2M per year; The weekly price for professional services is $80K per week; therefore, the total price for such engagement would normally be $2.960M. We are giving a discount of $1.46M on this proposal. In addition, Certora will allocate $200K to incentivise independent security researchers to review contracts and write specifications. The incentive model for this program can be found here.

8 Likes
2

It seems that you don’t need to re-initiate discussions for this proposal. :slightly_smiling_face:

https://www.comp.xyz/t/continuous-formal-verification
https://www.comp.xyz/t/certora-formal-verification-proposal/

2 Likes
3

Mr. Clairvoyant’s comment in those previous post makes sense.

Most DeFi protocols are running under loss, annual revenue for AAVE is 16MM while expenditure is 26MM (or 17MM deducting the development cost of $GHO). Currently, Compound’s revenue is about 2MM, while there’s a fixed cost of at least 4MM from Gauntlet and OZ.

I suppose it’s a wise choice to think longer about the sustainability of the protocol.

1 Like
4

Hi @ClairvoyantLabs and @RapidsCapital thanks for your comments; we understand and appreciate your concerns!

Formal verification is complementary to audits, risk management, and bug bounties. It adds an extra layer of security on top of these other layers and can be used before and after auditing. In the Aave project, we prevented six critical bugs while working in parallel with several top auditing firms. We’re also enabling agility by checking the code, and preventing critical bugs while enabling rapid development. The Certora Prover is integrated into the normal development pipeline and analyses the code after every change through CI/CD.

We believe that for a protocol holding approximately $2bn in TVL, the cost of a potential hack or failure could be far worse than the costs of extra security.

We are also committing ourselves to the well-being of the project by accepting 1/3 of the price in COMP, locking it for one year.

Additionally, we are developing complementary open-source technology that integrates with other tools and gives value independent of Certora’s proprietary tools, namely Gambit and CVL to foundry integration; so even if the agreement is not renewed the CVL rules can still be used together with fuzzers and other external tools.

2 Likes
5

This is very expensive, and I’m curious as to whether it’s sustainable to be paying this much. Is there any way that the cost can be brought down?

2 Likes
6

Thanks for your question @VonNeumann2022!

In addition to unlimited access to the market-leading verification platform, Compound will have a team of Certora senior security engineers and researchers actively reviewing code changes and providing formal security rules before manual audits. These rules are also used for unit testing, e.g., with tools like Foundry and Echidna. This is currently working well for Aave. Our team works before audits to prevent critical bugs while enabling rapid code development. To help offset the total cost, Certora is giving back to the Compound community $200,000 to increase the security posture through open-source rule writing competitions.

7

Generally speaking, we are a huge fan of this proposal and believe the service is both appropriate and needed. When looking at the budget concerns brought up, we have a slightly different opinion and take. We’ve worked together with Certora in the past, and believe that in today’s environment, with the passing of other service providers of similar skill and depth across many of the defi blue chip players, this specific scope of work is priced pretty competitively. The ideal bull market scenario of $3m for this type of service would be quite hefty in this market, but taking this down to $1.8m to the core team makes this seem very appropriately priced.

One thing we would like to learn more about is the $200k chunk that is for the Compound community. How is the team looking to proportion this amount and how does the community at large get involved here?

3 Likes
8

Citing Mr. Clairvoyant’s comments posted here:

Certora provides services first, and Certora finds problems after OpenZeppelin, and it is more appropriate for the community to pay Certora fees each time. This is a better way to cooperate.

Trail of Bits and ChainSecurity may also be able to provide more multiple security services, and they may also find other security issues after the OpenZeppelin and Certora audits.

To maximize security, Compound should buy all security services and audits regardless of expense.

If certora really wants to proceed the proposal, it’s wise to consider other alternative payment programs.

9

Dear @pennblockchain,

Thanks for your supportive comments, given your deep involvement in governance proposals and understanding of security.

The $200K in community grants incentivize security researchers to review suggested changes and submit CVL rules. Certora will provide free Prover access to any Compound community members that want to learn CVL and write rules for the Compound protocol. Throughout the year, Certora will host rule writing competitions through Secureum, Code4rena, and via the Certora discord channel. The payouts for those competitions will be funded from the $200K budget in this proposal.

1 Like
10

Dear @RapidsCapital

Thanks for your feedback on this proposal.

In addition to the Services components of the proposal, at its core, Certora Prover is a development tool designed to be integrated into Compound’s CI/CD pipeline before manual audits. This proposal enables Compound developers to continue the hard work they are doing to take a shift-left approach to write secure code by checking every change, similar to the way compilers are used. Every time the code is changed the Certora Prover is invoked via a command line interface in order to find which rules hold.

As stated in a previous discussion [here]

“This all being said, we do think that having robust FV rules would enhance the security of governance proposals and would be a good way to prepare for an audit by catching bugs during development. We already recommend that our audit clients build a robust test suite, which can include FV, as part of their Audit Readiness.”

Including FV enhances the auditing process and enables a better outcome for Compound’s security. Certora is fully committed to protecting Compounds community of users.

1 Like
11

We’ve used Certora on OUSD, and it’s been a good thing. It’s a layer of security that takes a different angle than audits, and it can find things that audits typically don’t. Formal verification also has a particular strength in working with math heavy contracts such as Compound/AAVE.

I do think that continuing to work with Certora would be advantageous for Compound.

This proposal would be a considerable increase in the scope of work that Certora would be doing with Compound. So the question would be if the extra gains beyond periodic formal verification audits as have been done in the past would be worth the price difference.

2 Likes
12

Adjustments to the original proposal

After collecting feedback from the community and in order to address the concerns expressed, we understand the best way to proceed is to submit the same proposal, but for half a year. This period will allow Certora to prove the value that formal verification can add to the protocol’s security before committing to a longer period.

We did something similar with AAVE, and the proposal passed just with sufficient votes. After proving our value, we raised an annual renewal proposal and got 651.7k votes, 331.7k more than the 320k necessary votes.

To summarize, we are proposing the following changes:

Offering

The agreement period will be 6 months. Certora will allocate a team of three security engineers to write rules for up to 6 weeks.

Pricing

The proposed price for the project is $750k for 6 months. Termination of the agreement will be available through governance voting given a 30 days notice.

$750k worth of COMP vested linearly over six months.

Certora will allocate $100K to incentivize independent security researchers to review contracts and write specifications.
We have been thrilled with community researchers’ results using our Prover platform - our recent contest with Code4rena for Blockswap uncovered 6 bugs of medium severity, and all injected high-severity bugs were found.

3 Likes
13

We don’t doubt your professionalism, but Aave’s support for your decision is not related to Compound. Based on practical considerations, I still can’t agree to this increase in expenditure.

2 Likes
14

"The bug survived 9 rounds of auditing by top security companies and even formal verification. It was not found until being exploited. "

15

Hi @ClairvoyantLabs. Thanks for your involvement and for sharing that.

Nobody can guarantee 100% lack of bugs. The interesting question is whether formal verification finds additional high-severity bugs that are hard to be caught by manual auditing (and therefore weren’t reported). Formal verification doesn’t claim to find all of the bugs in a system, but it allows one to approach security from a different angle that often finds a different class of issues.

1 Like
16

Formal Verification Report for Euler

But Euler Finance has been hacked for 177M USD. :slightly_smiling_face:

1 Like
17

That Certora report was from October 31, 2021. The bug was added after that, on July 5th, 2022.

6 Likes
18

Thank you, @dvf. The Euler team acknowledged that the newly added functionality was not reviewed by the Certora team or checked with the Certora Prover.

Dear @ClairvoyantLabs, the idea in this proposal is to run formal verification every time the code is changed to avoid situations like Euler.

3 Likes
19

Hi @sofiviss,

Would love to introduce you to Omniscia. We do audits, pen tests, tokenomics analysis and due diligence. We could probably help Compound in some ways for your upcoming audits.

We have audited close to 250 projects like L’Oreal, Republic, Morpho, Tokemak, AvaLabs, Matic, LimitBreak, OlympusDAO since 2021.

  • Our reports are web-based and include aggressive gas-saving recommendations
  • We have a clean track record (not on the rekt leaderboard)
  • Static analysis represent < 10% of the work we will conduct on your contracts. The bulk of the audit consists of having extremely senior security engineers manually review your contracts

Happy to connect by email at clement@omniscia.io or TG at @ClementBarbier

What are the most important criteria when picking an audit firm to you?

Best

1 Like
20

There are a few reasons why I plan to vote against this proposal:

  1. The Compound III (comet) codebase is already formally verified, and there shouldn’t be material changes to the codebase going forward; a key differentiator between comet and v2, is that comet uses a factory model to deploy new instances (generally a single smart contract), reducing the need to add new code or properties. In many ways, it’s “complete” already.
  2. This proposal doesn’t demonstrate a clear path for how community developers will use Certora–making the tools available is great, but it’s likely to have little “up-take” without significant investment from developers.
  3. Any changes to the security surface of the Compound ecosystem, at this point, should be planned holistically based on a needs-based strategy.
  4. In general, I am opposed to funding requests outside of the grants program. There is even a security section of the grants program, which could accomodate specific security-based endeavors.

Making Certora available to a distributed ecosystem of developers would make a lot of sense if/when a gen-4 protocol is being written from the ground up.

4 Likes