Summary
A proposal for significantly and continuously improving the security of the Compound platform and the dApps built on top of it, by offering our formal verification and path coverage tooling service to the Compound Platform contributors and the Compound Protocol dApp developers.
Background
Compound Protocol Security
The Compound 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 not streamlined well 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 30 experts in smart contract security, formal verification methods, and compilation techniques. 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 Finance, 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. We are particularly proud of finding the most issues in all the projects that we worked with both before and after manual auditing. We are also the only team that was able to formally verify interesting security properties including preservation of funds.
Certora and Compound Relationship
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 were able to find a subtle bug after the contract completed auditing by Trail of Bits. 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 in formally verifying a sophisticated bugfix, whose goal was to block potential exploits. We have written rules for that purpose, successfully showing that no code paths can trigger the exploit.
In addition, we formally verified the V2 version of the protocol, including the MoneyMarket contract. There, we were able to find more bugs in pre-deployment and post-audit. For example, a rule for ETH borrows written by Jared Flatow (VP Engineering) from the Compound team found a mismatch in the computation of accrued interest, leading to never being able to fully repay the loan. We have found many more costly bugs in the platform, preventing immense losses and protecting its users, including in the OpenOracle protocol.
Proposal
As described previously, we have been working closely with the Compound core team. However, we are not working with the Compound Platform contributors (not directly employed by Compound) and the Compound dApps developers (developing dApps on top of the Compound Protocol). Recent exploits (such as the claimComp bug discovered in Proposal 62) show that this approach is insufficient; these exploits have caused hundreds of millions of dollars of losses.
Case Study: Applying Certora Prover to check Proposal 62
Proposal 62 pertains to parts of the code that were not verified by Certora, but applying simple rules could have identified the bug. For example, the bug would be detected by the following rule:
Rule: maxCompReward
Description: The max COMP reward of a user has an upper limit, based on the current supplyState, borrowState and compAccured.
Claimed COMP should also satisfy other simple properties, and checking these properties could detect and prevent additional bugs. For example:
Rule: noFrontRunningGainOrLose
Description: The amount of COMP received at a specific state is the same whether or not another user (possible admin) has performed an operation just before.
Rule: zeroGainOnZeroBlocks
Description: A user with zero borrows can not gain COMP in a single block (for example by using a flash loan).
An executable formalization of the rules detects the bug introduced in Proposal 62, in particular, the rule called maxCompReward triggers a violation.
Hence, we propose two approaches to significantly increase the confidence in the platform itself and in the smart contracts built on top of it. The first is the Certora Prover, and the second is a new symbolic execution tool (path coverage). Both of these methods leverage the high-level rules to guarantee that all paths of the code satisfy the rule.
The two approaches are complementary: The Certora Prover will prove that specific critical parts of the code are sound and find hard to detect bugs, while the symbolic execution tool will be 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.
Formally Specifying High-Level Rules of dApps in Open-Source CVL
We will carefully review every code change and write high-level correctness rules in English and in CVL, Certora’s domain-specific specification language, for DeFi smart contracts built on top of Compound, as well as for the Compound platform itself via its contributors. These rules will be used later for the Certora Prover and the new path coverage tool.
In the process of writing the rules, we will perform a code audit and identify bugs manually. We will allocate a full-time software engineer for updating the rules capturing the essential security properties of the Compound Protocol and its derivatives, and a security researcher to review ALL code changes. These engineers are readily available and familiar with the logics of the Compound Protocol. Our current backlog for customers is several months.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 dApp developers, as different developers could use rules fitting their purposes which were written by others. We will compensate non-Certora rule writers with COMP tokens according to their contributions.
Formal Verification of Smart Contracts during CI/CD
The above rules will be used by the Certora Prover, which will be available to all Compound platform developers. The CVL will be integrated as part of a 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 Compound 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. The code developed in this project will be open source to allow contributions from the community.
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.
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 and report every CVL rule holds.
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 cases that are not covered by the specification are currently not 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 measures: (1) the number of paths covered by the path coverage 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 one security engineer and one security researcher for writing rules for the Compound platform contributors and for Compound dApps as needed. These engineers will be constantly available to Compound on a year-round basis.
- We will offer all Compound platform contributors (registered by Compound) access to the Certora Prover SaaS platform to check new and existing rules, as well as provide support for run result analysis and new rules creation.
- We will create a cloud-based path coverage product that will analyze the Compound 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 path coverage product, including rule violations and covered paths, visible to all Compound users. Rule violations will be reported automatically to the Compound 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 path coverage tool.