Formal Methods for Secure Smart Contract Upgradability

Thomas Bernardi, Nurit Dor, Anastasia Fedotov, Shelly Grossman, Uri Kirstein, Alexander Nutz, Lior Oppenheim, Or Pistiner, Mooly Sagiv, John Toman, James Wilcox

December 21, 2020

Background

A bug allowing the execution of untrusted code in Aave's LendingPool logic contract was discovered by Trail of Bits following the launch of Aave's V2. 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 that 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 that is usually performed immediately after construction or an upgrade. This initialization process is executed by invoking a function usually named initialize().

Since the initialize() function 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. As a consequence, 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:

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 Initiation or 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 have an adverse effect on DeFiProxy. Thus there is great importance to establish 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 is 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 absence of property violations. Code review and auditing is an excellent way 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, the safe_initialization property could be applied to both DeFiProxy and DeFiLogic contracts. To make the best use of formal verification tools, great care should be taken to apply it to all relevant code. The Certora team is collaborating with the developers on writing useful specifications, which can be used with formal verification tools as well as in 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.