Formal Methods for Secure Smart Contract Upgradability

Following the launch of Aave’s V2, Trail of Bits discovered a bug allowing the execution of untrusted code in Aave’s LendingPool logic contract. We studied the bug report in-depth and found that formal verification, harnessed correctly for the execution model of Ethereum, could be used to avoid this bug. The main takeaway is that even if one identifies the right safety property of the code, one still has to include the first deployment phase of the contract in the scope of formal verification.

This blog post contains some best practices for ensuring the safety of future deployments. While these results are applied to Aave’s code, they are relevant to many other DeFi projects and smart contracts in general. Our findings increase the usefulness of automatic reasoning techniques such as formal verification by shedding some light on the specific execution model of Ethereum, which may have consequences unpredictable to human reasoning.

Contract Upgradability and Initialization in a Nutshell

Aave’s architecture allows for upgradability. Logic contracts are deployed as libraries to the Ethereum blockchain and hold the code for the core business logic of the system. The deployment also includes proxy contracts that use those logic library contracts. A proxy contract features generic upgradability functionalities and maintains the system’s state. It invokes the library code using the delegatecall instruction of the EVM, which runs the code of the library in a context identical to the caller’s contract, including the caller’s storage. This way, if a bug is discovered in the code of the logic contracts, it is possible to deploy a new logic library and reroute the proxy to point to the new library.

Contracts in Aave consist of a 2-step initialization process:

1. Contract construction: The code runs as part of the constructor, before the contract’s address and code are registered on the blockchain.
2. Contract initialization: An additional, one-time initialization process usually performed immediately after construction or an upgrade. This initialization process is executed by invoking a function usually named initialize.

Since initialize is part of the contract’s public API, it can be invoked. However, initialize affects the system’s main configuration, and thus it is designed to be executed exactly once per deployment by a trusted party.

The Bug

Let us assume an upgradable contract DeFiProxy with a logic library DeFiLogic. Both DeFiProxy and DeFiLogic contain the same logic functionality:

contract DeFiLogic {   
  function initialize(address _addressProvider) {
    require(revision > lastInitializedRevision);
    lastInitializedRevision = revision;
   
    addressProvider = _addressProvider;
  }
  
  function callAddressProvider(...) {
    addressProvider.delegatecall(...);
    ...
  }
}

In addition, DeFiProxy has a constructor:

constructor(address _addressProvider) {
  initialize(_addressProvider);
}

If the initialization process was performed correctly, the eligible code owners would call initialize with the correct addressProvider. Consequently, any later calls to callAddressProvider would invoke the same addressProvider address, which is trusted. Since the interaction between users and the above smart contracts is expected to go through the proxy DeFiProxy, one may suggest analyzing DeFiProxy and DeFiLogic together as if they were a single contract.

However, such modeling overlooks the fact that the library contract DeFiLogic, which is also a contract that lives in the blockchain, should be initialized as well. If an attacker identifies that initialize was not called for DeFiLogic, they could invoke initialize and set addressProvider to a contract they control. Later, they could also invoke callAddressProvider to execute the code they control, and since the call is a delegatecall, it would run in the context of DeFiLogic.

A classic attack is to execute selfdestruct, as occurred in the Parity wallet a few years ago. After the DeFiLogic is destroyed in this manner, all calls from DeFiProxy may fail, until a new library is deployed and DeFiProxy is rerouted to point to it.

Inductive Invariants and the Safe Initialization Invariant

One of the most powerful instruments in formal reasoning is the inductive invariant. Colloquially, an inductive invariant is a property of the program that holds in both:

• Initiation: In the program’s initial state (for smart contracts: post constructor call).
• Step: After every atomically-executed transition of the program, assuming the invariant holds before that transition.

An invariant of the above toy example and also of Aave’s code is the following:

invariant safe_initialization
  must_revert(initialize);

where must_revert(f) is a predicate that is true if f certainly reverts in the current state. This invariant means that initialize, once the contract is constructed, should always revert.

A tool such as the Certora Prover can reason about properties such as safe_initialization and check if they are inductive invariants of the code. If the Prover fails to prove that the invariant is inductive in all states, it will show a concrete trace violating either the Initiation or the Step.

The safe_initialization invariant is verified for DeFiProxy but is violated for DeFiLogic. While the Step case is true for both, DeFiLogic is not properly initialized, and thus Initiation is not proved. After the construction of DeFiLogic, anyone can call initialize, including untrusted parties.

As the potential exploit shows, the fact that safe_initialization is not an invariant for DeFiLogic could adversely affect DeFiProxy. Thus there is great importance in establishing the validity of invariants to all contracts to which they apply.

Conclusion

Testing, code review, auditing, and formal verification are complementary techniques to improve code security. Unit and system testing are important to check the behavior of the system in common scenarios. Formal verification is helpful in early bug detection and guaranteeing coverage of a given correctness property, especially to identify rare corner cases where a property is violated and prove the absence of property violations. Code review and auditing are excellent ways to look for new correctness properties and promote good software practices in general.

One of the hardest problems in formal verification is writing adequate specifications. An equally important aspect is the scope of the verification. As we saw above, we could apply the safe_initialization property to both DeFiProxy and DeFiLogic contracts. To make the best use of formal verification tools, great care should be taken to apply them to all relevant code. The Certora team is collaborating with the developers on writing proper specifications, which can be used with formal verification tools and unit testing or symbolic execution.

We thank the team at Trail of Bits for locating the bug and reporting it to the community and the Aave team for reviewing this blog post. We are excited to make formal verification a useful, practical tool for enhancing the security of DeFi applications.

To learn more about how formal verification can make your contract more secure, contact Certora at info@certora.com.