Runtime Verification audits Morpho’s AAVE V3

Runtime Verification is pleased to announce the completion of the Morpho AAVE V3 audit. Morpho is a lending protocol built on top of AAVE which matches borrowers to lenders peer-to-peer.

Audit Scope

In the Morpho protocol, borrowers and lenders are paired up to exchange assets. In the event that no compatible pairing is found, the protocol will fall back on the AAVE. One advantage of a peer-to-peer transaction is that users will benefit from better interest rates than trades that rely on the AAVE network. 

This audit focused on a group of contracts in the protocol which are responsible for handling several key functions including -

• Transfers of reserves(ERC20) tokens 
• Internal accounting of collateral 
• Borrowing and lending positions
• Liquidations
• Configuration of lending markets and risk parameters

These contracts aim to maximize peer-to-peer credit lines, as this optimizes interest rates and borrowing rates for the users. 

The audit scope is limited to the Solidity source code of a number of contracts in the protocol. Datastructure libraries used by the matching engine and off-chain code are outside the scope. A detailed list of all the contracts, libraries and interfaces audited can be found in the report.

Methodology

Runtime Verification conducted a manual code review for a period of 10 weeks and delivered a detailed report. on May 2nd, 2023. 

The first step in the audit process consisted of a thorough reasoning of the business logic of the protocol. During this process, any security critical properties were identified and validated to ensure the absence of loopholes in the logic and inconsistencies between the logic and implementation. To increase our confidence, we extended Morpho’s test suite with a set of safety properties

Next, the code was checked against a list of known security vulnerabilities and attack vectors. 

During the audit process, several code quality assurance tools were used to aid in the testing, ranging from static analysis tools, e.g. Slither, over dynamic testing tools, e.g. Foundry, to symbolic execution with KEVM. Finally, we met with the Morpho team to provide feedback and suggested development practices.

Results

The audit identified and highlighted some issues along with a number of informative findings. Runtime Verification worked together with the Morpho team to review code fixes. 

Users interested in a more detailed and technical explanation about the findings can go over the full report in our GitHub repository.

About Morpho

Morpho is a lending protocol, the third biggest on Ethereum after Aave and Compound, with +$700m currently deposited. Built on top of Aave and Compound, Optimizers improve rates while maintaining the same liquidity and risk parameters.

The user experience of a Morpho Optimizer is almost identical to that of Aave and Compound. Users can supply and borrow assets just as they would from lending pools but with Morpho’s seamless peer-to-peer matching system, they experience better rates.

About Runtime Verification

Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.