Formal Verification of Aave v3: A Review

Introduction

In this case study we look at how the Certora formal verification Prover can be used for discovering high-severity vulnerabilities in the Aave lending protocol. Certora uses symbolic execution to evaluate all possible inputs to functions being tested, allowing us to uncover vulnerabilities that typical unit tests covering only specific cases can't. This was the case for Aave when it underwent this assessment by Certora, their test suite consisted of multiple hardhat tests with specific values for assessing specific system behavior. Expected behavior however can often bias test creation and leave out potential edge cases that may lead to unexpected functionality and consequently security vulnerabilities as we will see with the vulnerability discussed below.

The Contracts

For the review conducted by Certora 6 contracts were included in scope, but we'll only be focusing on the Pool contract since this is where the vulnerability we'll be looking at exists:

Pool - the main entry point into the Aave Protocol, most user interactions (borrowing, lending, etc.) with the Aave Protocol occur via the Pool contract

Discovered Vulnerabilities

Certora tested a total of 46 rules written in CVL during their campaign, with an accompanying manual review of the code included as well, the resulting vulnerabilities identified from these efforts are shown here:

1 Critical
2 High
2 Medium
1 Low
1 Recommendation

For this post we'll focus on one of the High severity vulnerabilities detected using a rule during the Certora review, you can review the other vulnerabilities in the report.

Note

The spec files used in the report have been updated in the current Aave repo and the vulnerability has been resolved by this PR. For our study, we have created this repo forked from commit d66a5fd (the last commit made before the PR that resolved the issue), so that the tests could be run to show the vulnerability. To run the test for yourself follow the instructions in this README.

H2 - Loss of assets

From the report, we see Certora's description of the issue as: "Confusion of Asset and EMode price feed for liquidations" meaning that the wrong price feed is used for liquidations. In Aave, a user's collateralized debt position (CDP) can be liquidated by anyone using liquidationCall whenever the health factor (a measure of the debt-to-collateral ratio of their position) is less than 1, we can see that this issue must come from calls to this liquidation function.

Looking at the liquidationCall function in the Pool contract:

  function liquidationCall(
    address collateralAsset,
    address debtAsset,
    address user,
    uint256 debtToCover,
    bool receiveAToken
  ) external override {
    LiquidationLogic.executeLiquidationCall(
      _reserves,
      _usersConfig,
      _reservesList,
      _eModeCategories,
      DataTypes.ExecuteLiquidationCallParams({
        reservesCount: _reservesCount,
        debtToCover: debtToCover,
        collateralAsset: collateralAsset,
        debtAsset: debtAsset,
        user: user,
        receiveAToken: receiveAToken,
        priceOracle: ADDRESSES_PROVIDER.getPriceOracle(),
        userEModeCategory: _usersEModeCategory[user],
        priceOracleSentinel: ADDRESSES_PROVIDER.getPriceOracleSentinel()
      })
    );
  }

we can see that the price oracle passed into ExecuteLiquidationCallParams is returned by the getPriceOracle function in PoolAddressProvider contract:

 function getPriceOracle() external view override returns (address) {
    return getAddress(PRICE_ORACLE);
  }

This is the default asset price oracle, meaning that if the user is in eMode ("efficiency mode" which is supposed to maximize capital efficiency and allows using a specific price oracle for each eMode category) an oracle other than the default asset oracle that might've been specified will be ignored.

Given that the user can be using any number of a possible 255 eMode categories, each with a possible price oracle, the priceOracle parameter passed into the ExecuteLiquidationCallParams should check if the category being used has a different oracle associated with it and only fallback to the default oracle if none has been specified.

The property outlined by Certora to catch this vulnerability was "Emode source price usage" which is located in the original pool.spec file under the rule named priceOracelCounter, for this article we have rewritten this rule in the priceOracelCounter.spec file for clarity and to resolve some issues with the Certora Prover due to the specification used in the review being written in an older version of CVL. The slightly modified rule is defined as:

using SymbolicPriceOracle as priceOracle;

ghost mapping(address => mathint) usageOfPriceOracle {
    init_state axiom forall address asset. usageOfPriceOracle[asset] == 0;
    axiom forall address asset. usageOfPriceOracle[asset] >= 0;
}

hook Sload uint256 p priceOracle.price[KEY address asset] STORAGE {
	usageOfPriceOracle[asset] = usageOfPriceOracle[asset] + 1;
}

rule priceOracelCounter(address asset, method f) {
	env e;
	calldataarg args;
	mathint before = usageOfPriceOracle[asset];
	f(e, args);
	assert usageOfPriceOracle[asset] == before;
}

where we use the usageOfPrice ghost variable to indicate whether the priceOracle variable has been accessed via a hook into load operations for this variable in the SymbolicPriceOracle contract which we are using as a mock price oracle. We can see from the below result of running the Prover that it has been violated in the liquidationCall function in the Pool contract:

This proves that the property outlined in the report is violated, meaning that instead of accessing the eMode price oracle associated with the category, the default asset price oracle was used instead. This could potentially cause the liquidation price to be worse than expected and is inconsistent with borrow/repay operations that may use the eMode price oracle.

Conclusion

We've seen how defining a system's properties via property testing with Certora can uncover novel vulnerabilities that might not have been identified otherwise. Defining these properties as code rather than just having them in writing allows them to become an integral part of the development lifecycle and ensures they are never violated. Once these tests are added to a project's test suite, they can be used in a CI/CD pipeline and run against new changes to ensure that the additions don't cause any breaking of the properties and potential vulnerabilities associated with them.