Detecting Corner Cases in Compound V3 with Formal Specifications

We describe an interesting correctness rule for Compound’s new protocol — Comet — and show how the Certora Prover was used during early development to eliminate bugs in the code before deployment

Introduction

In today’s market, most borrowing activity in DeFi consists of supplying volatile crypto assets and borrowing a single base token. To address this common trading pattern, Compound created their newest lending app, Comet, which aims to achieve greater capital efficiency by optimizing for that particular use case. The contract allows users to supply up to 15 pre-defined (volatile) assets as collateral while borrowing a single pre-defined coin (most frequently a stablecoin).

During the development process, the Certora team, together with Compound Labs, wrote formal specifications in Certora’s verification language (CVL) to describe the intended behavior of the system, and used the Certora Prover, our automated formal verification tool, to check if their implementation obeyed those specifications. The Compound and Certora teams specified 50 correctness rules to describe important properties the protocol should obey. Automatic formal verification helped the teams detect bugs in corner cases during development and fix them before deployment, as been be seen in the verification report.

The remainder of this post shows how the formal verification process uncovered a subtle bug in the Comet protocol during development. Since the Prover uncovered the bug before deployment, the Compound developers were able to address it before any assets were at risk. It was fixed in commit 4cbb7e6a.

Along the way, we’ll describe how to apply modularity, an important technique for handling code that causes the Prover to time out.

Collateral flags in Comet

The bug that was discovered was caused by incorrectly handling the set of flags representing the state of a user’s collateral. We begin by describing how these flags should work.

Comet holds a data structure for every user that contains the list of assets that have been supplied as collateral. This structure is stored as a bit vector, where each asset (of the 15) has a unique assetOffset from 0–14. The bit vector is called assetsIn, and each bit of assetsIn is called a flag.

struct UserBasic {
    …
    uint16 assetsIn;
    …
}
/// @notice Mapping of users to base principal and other basic data
mapping(address => UserBasic) public userBasic;
In addition, for each asset there is a mapping that stores how much collateral each user has supplied:
struct UserCollateral {
    uint128 balance;
    …
}
/// @notice Mapping of users to collateral data per collateral asset
mapping(address => mapping(address => UserCollateral)) public userCollateral;
Using the bitwise vector assetsIn allows a fast and cheap computation of which assets are used as collateral by a specific user. Two main functions are used to manipulate and access assetsIn:
/**
* @dev Whether user has a non-zero balance of an asset, given assetsIn flags
*/
function isInAsset(uint16 assetsIn, uint8 assetOffset) virtual internal view returns (bool)

/**
* @dev Update assetsIn bit vector if user has entered or exited an asset
*/
function updateAssetsIn(
    address account,
    AssetInfo memory assetInfo,
    uint128 initialUserBalance,
    uint128 finalUserBalance
) virtual internal

A fundamental property — the integrity of the assetsIn flags

We say a property is fundamental if violations of that property mean that the critical behavior of the system is incorrect. Here is an example of a fundamental property:

Property: A userCollateral for a specific asset is greater than zero if and only if the corresponding flag is set.

This property can also be written using logic notation:

userCollateral[user][asset].balance > 0 ⇔
isInAssetsIn(userBasic[user].assetsIn, getAssetOffset(asset) )

Why is this property fundamental? As indicated above, assetsIn is used for determining which assets are provided as collateral. A typical pattern in the code is as follows:

uint16 assetsIn = accountUser.assetsIn;
for (uint8 i = 0; i < numAssets; i++) {
if (isInAsset(assetsIn, i)) {
…

This pattern is used in many of the critical operations of the protocol:

• Check whether an account has enough collateral to borrow
• Calculate the amount of borrowed liquidity for an account
• Check whether an account has enough collateral to not be liquidated
• Calculate the amount of liquidation margin for an account
• Absorbing a user’s account (a process similar to liquidation)

If the above property does not hold, then several things might go wrong:

• A user may not be allowed to borrow, although they have enough collateral. This means the system is vulnerable to a denial of service attack.
• A user may be liquidatable even if they have enough collateral. This means that users may lose assets when they should not.
• The contract may not transfer a user’s collateral back to itself when absorbing an account. This results in a loss of assets to the system.

Since so many things can go so badly if this property is violated, we would like assurance that the system cannot violate the property.

Formally specifying the integrity of the assetsIn flags

Formal verification with the Certora Prover is one method for providing this assurance. To use the Prover, we must specify the desired property in Certora’s verification language (CVL). The Certora Prover can then analyze the smart contract code to determine whether it meets the specification.

Given a program and a property, the Prover returns one of three answers:

• A violation shows a concrete input that violates the specification. This input can be very rare and thus very hard to find with testing and fuzzing.
• A proof indicates that it is mathematically impossible to violate the specification.
• The Prover can also time out and fail to return an answer.

Unlike unit testing or fuzzing, Certora specifications are exhaustive: a proof of a property means that the property holds in all cases, instead of a fixed set or random sample of the possible scenarios.

In CVL, the fundamental property described above is easy to write. We have already shown a logical representation of the property:

userCollateral[user][asset].balance > 0 ⇔

isInAssetsIn(userBasic[user].assetsIn, getAssetOffset(asset) )

Writing this kind of property in CVL is straightforward. Properties that should hold at all points in time can be expressed as an invariant in CVL:

invariant integrityOfAssetsInFlags(address user, uint8 asset)
userCollateral[user][asset].balance > 0 <=> isInAssetsIn(userBasic[user].assetsIn, getAssetOffset(asset))

If the Prover can prove this property, we know it must hold on all reachable states. If the Prover finds a violation, then we know there is a critical bug and will get an example of how to exploit it. Unfortunately, because of the complexity of the Comet codebase, this rule falls into the third category: the Prover times out while trying to prove it.

The next section explains how we can resolve this timeout to find a proof or a violation.

Simplifying the verification using modularity

In a complex system such as Comet, we prove properties using a modular approach (e.g., see https://github.com/dafny-lang/dafny). We break the verification into two independent steps:

• Prove useful properties of difficult-to-reason-about low-level functions
• Simplify the low-level functions using an easy-to-reason-about abstraction that adheres to the proven properties

We now demonstrate these steps in detail.

Step 1: Simplifying assetIn() and updateAssetsIn()

The Prover currently has difficulty with bitwise operations. After some investigation, we found that the assetIn and updateAssetIn functions are called frequently in the Comet codebase and use these difficult-to-reason-about bitwise operations.

The assetIn and updateAssetIn functions query and update the bit vector containing the asset flags. In principle, these functions should be equivalent to the following implementations, which use a standard mapping instead of a bit vector:

mapping (uint16 => mapping (address => bool)) assetInState;
function isInAsset(uint16 assetsIn, uint8 assetOffset) returns (bool) {
    return assetInState[assetsIn][indexToAsset[assetOffset]];
}
function updateAssetsIn(
    address account,
    AssetInfo memory assetInfo,
    uint128 initialUserBalance,
    uint128 finalUserBalance
) override internal {
    if (initialUserBalance == 0 && finalUserBalance != 0) {
        // set bit for asset
        assetInState[assetInAfter][assetInfo.asset] = true;
    } else if (initialUserBalance != 0 && finalUserBalance == 0) {
        // clear bit for asset
        assetInState[assetInAfter][assetInfo.asset] = false;
    }
}

Although this implementation is less efficient, it is much easier for the prover to reason about.

Using CVL’s modularity, we can verify properties on the rest of the code base using these approximations in place of the actual assetIn and updateAssetIn. This simplification allows the prover to successfully prove the integrityOfAssetsInFlags invariant.

Step 2: Checking the approximation

To justify the approximation in step 1, we argued that in principle, the actual and simplified implementations should behave the same way. To check this assumption, we can verify that the implementations satisfy some basic correctness properties. For example, one property of these two functions is that the assetIn flag is updated according to calls to updateAssetIn. A typical unit-test program would check specific values:

const tokens = makeProtocol();
const user = makeUser();
const wethAddress = tokens[‘WETH’].address;
// call updateAssetsIn change from 0 value to 100
updateAssetsInExternal(user.address, wethAddress, 0, 100);
// check that isInAsset returns true for this user and token
 
assert isInAsset(getAssetinOfUser(user.address), tokens[‘WETH’].offset);

With CVL we can check the property on all possible values of user addresses, token addresses, token offsets, and balance values:

rule check_update_UserCollateral(
    address account, address asset,
    uint128 initialUserBalance, uint128 finalUserBalance)
{
    updateAssetsIn(account, asset, initialUserBalance,
                   finalUserBalance);
    bool flagUserAsset = isInAsset(getAssetinOfUser(account),
                         getAssetOffsetByAsset(asset));
    assert (initialUserBalance == 0 && finalUserBalance > 0) =>
            flagUserAsset,
           “Balance changed from 0 to non zero, yet the getter
            retrieved false”;
    assert (initialUserBalance > 0 && finalUserBalance == 0) =>
                                     !flagUserAsset,
           “Balance changed from non zero to 0, yet the getter
            retrieved true”;
}

Since our goal is gaining assurance that the actual implementations are correct, we can’t use the simplified versions of assetIn and updateAssetIn in this step. However, this rule focuses on a simple property of a single method, so the Prover can complete the verification of this rule in a timely manner, even though the code contains complex bitwise operations.

The violation found by the Certora Prover

Step 2 of the above process is essential. If the simplified version of the code doesn’t behave the same way as the original, then proofs that use the simplified version don’t apply to the real version.

In fact, the verification of the check_update_userCollateral rule in step 2 led us to discover the bug in the Comet protocol. Instead of producing a proof, the Prover produced a counterexample showing that the property doesn’t hold:

In this example, we can see that the user’s balance has changed from 0 to 1. The corresponding bitwise flag, however, is false. In the provided counterexample, the tool shows this happening for assetOffset 8.

The cause of the violation

A simple oversight caused this violation. In an earlier version of the code, the protocol only allowed 8 assets instead of 15. Some of the code still relied on the wrong assumption that there were only 8 assets. In particular, the following function is incorrect:

function isInAsset(uint16 assetsIn, uint8 assetOffset) virtual
         internal view returns (bool) {
    return (assetsIn & (uint8(1) << assetOffset) != 0);
}

This function returns false for any assetOffset greater than or equal to 8, which is not the correct behavior.

Once the bug was discovered, it was easy to address; it was fixed in commit 4cbb7e6a. The Prover was able to verify that the patched implementation did satisfy the intended property.

Conclusion

Formal verification using the Certora Prover is a powerful tool for finding subtle but important bugs in smart contracts. One of the fundamental limitations of formal verification is that there will always be cases where the Prover times out. However, we have shown that the technique of simplifying a complex function and then checking the simplification sometimes allows you to find bugs, even when the Prover initially times out.