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.
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.
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.
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:
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:
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;
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.
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.
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.
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.
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:
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:
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;
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.
Subscribe to Morpho
Subscribe to Morpho
MorphoUnderstanding Morpho Vaults: Intro & Simplifying Isolated Markets
Morpho Vaults combines the best of isolated markets and multi-asset lending pools to create a better way to lend. In time, we believe Morpho Vaults will become the default lending solution. Today, we are introducing a four-part series explaining why, starting with Part One: Intro to the Morpho Approach & Simplifying Isolated Markets.The Morpho ApproachThere are two main approaches to structuring lending markets in decentralized finance: lending pools and isolated markets. The former excels in...
MorphoAligning Around MORPHO — The Only Asset For Morpho
TL;DRMorpho will have only one asset—the MORPHO token. This single-asset approach ensures complete alignment between the network of contributing entities and the Morpho DAO (MORPHO token holders). To clarify this alignment, Morpho Labs is becoming a wholly-owned subsidiary of the Morpho Association to eliminate any perceived conflicts with equity value and ensure that token holders and these contributing entities share the same incentive. As the Morpho DAO explores introducing protocol fees t...
MorphoUnderstanding Morpho Vaults: Enabling Diverse Risk Profile
Morpho Vaults (formerly known as MetaMorpho Vaults) combines the best of isolated markets and multi-asset lending pools to create a better way to lend. In time, we believe Morpho Vaults will become the default lending solution. Last week, we introduced the Understanding Morpho Vaults article series with Part One: Intro to the Morpho Approach & Simplifying Isolated Markets. Today, we share Part Two: Enabling Diverse Risk Profiles to explain how, unlike the traditional one-size-fits-all approac...
MorphoUnderstanding Morpho Vaults: Intro & Simplifying Isolated Markets
Morpho Vaults combines the best of isolated markets and multi-asset lending pools to create a better way to lend. In time, we believe Morpho Vaults will become the default lending solution. Today, we are introducing a four-part series explaining why, starting with Part One: Intro to the Morpho Approach & Simplifying Isolated Markets.The Morpho ApproachThere are two main approaches to structuring lending markets in decentralized finance: lending pools and isolated markets. The former excels in...
MorphoAligning Around MORPHO — The Only Asset For Morpho
TL;DRMorpho will have only one asset—the MORPHO token. This single-asset approach ensures complete alignment between the network of contributing entities and the Morpho DAO (MORPHO token holders). To clarify this alignment, Morpho Labs is becoming a wholly-owned subsidiary of the Morpho Association to eliminate any perceived conflicts with equity value and ensure that token holders and these contributing entities share the same incentive. As the Morpho DAO explores introducing protocol fees t...
MorphoUnderstanding Morpho Vaults: Enabling Diverse Risk Profile
Morpho Vaults (formerly known as MetaMorpho Vaults) combines the best of isolated markets and multi-asset lending pools to create a better way to lend. In time, we believe Morpho Vaults will become the default lending solution. Last week, we introduced the Understanding Morpho Vaults article series with Part One: Intro to the Morpho Approach & Simplifying Isolated Markets. Today, we share Part Two: Enabling Diverse Risk Profiles to explain how, unlike the traditional one-size-fits-all approac...
>200 subscribers
>200 subscribers
Share Dialog
Share Dialog
No comments yet