Led by Quentin Garchery, the formal verification of Morpho Blue involved collaboration with other companies and individuals. Morpho Labs would like to thank members of Certora, specifically Jochen Hoenicke, and Daejun Park from a16z for their contributions.
Designed as a base layer for decentralized lending, software correctness and security are paramount for Morpho Blue.
Ensuring this involves a multi-faceted process across several phases, from pre-build to post-deployment. However, when proving the correctness of a smart contract, it is hard to find a method more rigorous and comprehensive than formal verification.
Used effectively, formal verification can help develop higher quality and, most importantly, more secure code. That is why Morpho Labs, with help from members of Certora and a16z, have invested significant time and resources into formally verifying Morpho Blue.
This article introduces formal verification, explains why it is suited to Morpho Blue, and demonstrates how it has been used to secure the protocol.
The full scope of Morpho Blue’s formal verification is available here.
An introduction to formal verification
Formal verification is the process of using mathematical methods to prove the correctness of a smart contract by verifying that it satisfies certain properties. These properties are expressed using formal language supported by the verification tool used to prove them.
In Morpho Blue’s case, specific information was written using CVL (Certora's Verification Language) and was verified by the Certora prover.
Formal verification is a powerful way to evaluate code correctness because it is exhaustive. Other methods, such as unit testing, are not. With tests, one can only check for correctness for specific scenarios (some inputs), while formal verification allows one to check for every scenario (all inputs).
Of course, everything has its pros and cons. Formal verification is comprehensive, but it is also resource-intensive. Its effectiveness depends heavily on the quality of the specifications. For developers, performing formal verification can be time-consuming, and it is often difficult to grasp the concepts that make it work on top of the tools and quirks that may exist.
Formally verifying Morpho Blue
Many code bases are too complex for formal verification, but Morpho Blue is well suited to it. As mentioned, the process can be time-consuming and only exaggerated by the complexity of a code base. The larger the code base, the more challenging it is to verify. Additionally, past specifications must also be updated if part of the code is upgraded.
Morpho Blue, however, is neither complex nor upgradeable. Its minimalist, immutable code base, consisting of only 600 lines of code, makes it a good fit for formal verification.
With that clarification out of the way, let us run through demonstrations of verification performed on Morpho Blue.
Example 1: Morpho Blue Markets
The Morpho Blue contract is a singleton contract that defines different markets. Markets on Morpho Blue depend on a pair of assets, the loan token that is supplied and borrowed, and the collateral token.
Taking out a loan requires to deposit of some collateral, which stays idle in the contract. Additionally, every loan token that is not borrowed also stays idle in the contract.
This can be verified by the following property:
Where idleAmount is the sum over all the markets of the collateral amounts plus the supplied amounts minus the borrowed amounts.
In effect, this proves:
-
Funds can only leave the contract through borrows and withdrawals
-
On a given market the borrowed amounts cannot exceed the supplied amounts
This property, along with the previous one, ensures markets are independent: tokens from a given market cannot be impacted by operations done in another market.
In the end, the verification of those invariants is done automatically by the Certora prover in a few minutes:
Example 2: Protection against common attack vectors
Reentrancy and immutability
Reentrancy is a common attack vector that happens when a call to a contract allows, when in a temporary state, to call the same contract again.
The state of the contract usually refers to the storage variables, which can typically hold values that are meant to be used only after the full execution of the current function.
The Morpho Blue contract is verified not to be vulnerable to this kind of reentrancy attack, using the rule reentrancySafe. Here is a simplified version of this rule:
rule reentrancySafe(method f, env e, calldataarg data) {
f(e, data);
assert !hasReentrancyUnsafeCall;
}
The variable hasReentrancyUnsafeCall is defined in the specification before this rule. This variable is set to true when a call is accessing storage, then making an external call, and accessing storage again. Setting the variable is done through hooks, which are given below for storage accesses.
Notice that storage access corresponds to either a storage read or to a storage write.
The variable hasCallAfterAccessingStorage is another specification variable (also known as a ghost variable) that requires to be set. This is done through a hook on CALL that is not shown here.
Similar techniques can be used to show that there are no delegate calls to other contracts, ensuring notably that the contract is truly immutable. With all of those defined, the verification is successful:
Extraction of value
The Morpho Blue protocol uses a conservative approach to handle arithmetic operations. Rounding is done such that potential (small) errors are in favor of the protocol, which ensures that it is not possible to extract value from other users.
The rule supplyWithdraw handles the simple scenario of a supply followed by a withdraw and has the following check.
assert withdrawnAssets <= suppliedAssets;
The rule withdrawAssetsAccounting is more general and defines ownedAssets as the assets that the user owns, rounding in favor of the protocol. This rule has the following check to ensure that no more than the owned assets can be withdrawn.
assert withdrawnAssets <= ownedAssets;
Understanding the limitations
Despite the thoroughness of formal verification, it cannot guarantee absolute perfection or eliminate all potential risks associated with Morpho Blue.
Formal verification is effective within the defined scope of specifications and assumptions. Human input and interpretation, incomplete specifications, and bugs in the tools used can also impact the accuracy of results.
For more on Morpho Blue’s formal verification, visit the GitHub.