Runtime Verification audits Algofi Lending v2

Runtime Verification is pleased to announce the completion of the Algofi Lending v2 smart contracts audit. Algofi is a decentralized application on Algorand, allowing users to lend, borrow, and trade Algorand and Algorand Standard Assets.

Past Algofi audits

Algofi engaged Runtime Verification back in October 2021, before the Mainnet launch, to conduct an initial audit on the protocol. The first audit lasted 7 weeks and covered a series of contracts implementing its decentralized lending market, including core contracts such as the "Manager Application", "Market Application" and a small helper library. After the Mainnet launch on December 17th, 2021, a second audit was carried out in January 2022 for 7 weeks covering two types of Automated Market Makers (AMM): a constant-product AMM (CPMM) and a stableswap AMM (Nanoswap). Algofi CPMM allows swapping between different assets, while Nanoswap focuses on efficient swaps between stablecoins. During the audit, the first 5 weeks were dedicated to the CPMM and the following 2 to the Nanoswap. Due to the AMM sharing code and architecture, during the Nanoswap audit, the focus resided on the implementation of the stableswap mathematical invariant.

This blog post is dedicated to the third audit conducted on Algofi lending v2 protocol.

Audit scope

The audit scope is limited to the PyTeal source code of the core smart contracts comprising the lending platform.

Audited contracts handle the bulk of the protocol functionality, and include -

• Manager smart contract - This is the central link of the protocol, managing all users and market functionalities.
• Market smart contract - Provides lending and borrowing functionality for ALGO and ASAs (Algorand Standard Assets)
• STBL2 Market smart contract - Provides borrowing of the Algofi stablecoin, STBL2, and controls its supply
• Vault Market smart contract - Allows users to deposit algos and participate in Algorand Governance, while still being able to use their assets as collateral in the lending protocol.

The audit only covered PyTeal source code of the contracts and it excluded any deployment and upgrade scripts, off-chain code and client-side portions of the codebase.

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 6 weeks, and delivered a detailed report on July 13th, 2022.

The first step in the audit process consisted of a thorough review of protocol and documentation to identify the components of the smart contract system and the interactions between them.

Next, a thorough manual review of the contracts PyTeal source code took place to identify a series of invariants that the system must maintain. A violation of one or more of these invariants may leave the system open for exploitation.

The contracts were then tested in a simulated environment using Runtime Verification’s in-house tooling (pyteal_eval and tstmodel). Leveraging this simulation environment has allowed us to systematically generate and check a large number of potentially malicious behaviors and look for violations of the system invariants discovered in the previous stage of the audit process.

Finally, an additional manual review of the codebase was conducted to ensure that any issues or potentially dangerous corner cases were identified.

Results

The audit identified and highlighted some issues along with a number of informative findings. The Algofi team addressed all the issues and concerns raised during the audit and incorporated all the necessary changes in the smart contracts. Code changes were not part of the scope and only a limited number of very small fixes went through a lightweight best-effort review.

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

About Algofi

Algofi is the leading decentralized finance application on the Algorand network. On Algofi, users can seamlessly lend, trade, farm, and participate in governance. Algofi was founded by a team of former traditional finance and technology professionals who believe DeFi will fundamentally change the financial system. They have chosen to build on the Algorand network due to its technological advantage across scalability, security, and decentralization.

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.