Runtime Verification audits Atlendis Protocol

Runtime Verification is thrilled to announce Atlendis Protocol's audit completion. Atlendis is a capital-efficient DeFi lending protocol that enables uncollateralized crypto loans for institutional borrowers.

Audit scope

The audit scope focused on the Solidity source code of the three main protocol contracts and a series of libraries and interfaces. The audited contracts account for the totality of the project by the time the audit was conducted and covered a series of functions such as:

• Pools are borrower specific on Atlendis. Once whitelisted, borrowers can borrow as they please from their own isolated liquidity pool in order to satisfy any recurrent liquidity needs. However, borrowers can only take one loan at a time and it needs to be repaid first in order to take the next one.

• Any user can be a lender and choose the pool they want to participate in, and select their preferred lending rate within a range.

• The borrowing rate is discovered by the market based on the offered lending rate thanks to a dedicated order book. At borrowing time, the protocol will automatically match the borrower with the most favorable lending rates.

• Once whitelisted, the Atlendis governance account can freely create ERC20 pools for the borrower, but the contracts only allow one token for each pool.

• Lenders making a deposit will get an NFT in exchange to reflect their positions.

• Unused capital such as funds not actively loaned are automatically forwarded to AAVE to generate yield. Borrowers can also choose to distribute additional liquidity rewards to their lenders for unused capital to incentivize liquidity in their pool and increase lenders’ base line APY.

A detailed list of all the contracts, libraries and interfaces audited can be found in the report.

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

Methodology

Runtime Verification conducted a manual audit review on Atlendis smart contracts for a period of six weeks and published a detailed report on February 18th, 2021.

The first step consisted of analyzing the documentation and whitepaper provided by the Atlendis team to understand the protocol's business model and identify the different ways each actor interacted with the protocol, such as their responsibilities and capabilities.

The next step focused on how the theory translated into implementation through the source code of the contracts in scope. A series of features were mapped out in specific locations in the source code and vice versa with the aim to, first, find where the features from the whitepaper were located in the code, followed by analyzing if the code behaved the same way as it was mentioned in the documentation. This step aimed to link each feature mentioned in the report to a part of the code and inform about any potential missing links to Atlendis to discuss it with them. Then, the mental model was materialized into mathematical formulas.

Finally, a series of hypothetical scenarios were developed to test whether certain interactions with the Atlendis protocol resulted in the expected outcome. In the cases where the outcome differed from the expected one, the team investigated what went wrong and why. An incorrect outcome could lead to a potential vulnerability and exploit of the protocol. The contracts in scope were also analyzed against well-known security vulnerabilities and mathematical details of the calculations performed by the contract were studied closely to dismiss possible rounding errors that could lead to an unexpected behavior.

Results

The audit identified and highlighted some issues along with a number of informative findings. The Atlendis Labs 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; however, the team conducted a lightweight best-effort review of a limited number of changes.

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

About Atlendis

Atlendis is a capital-efficient DeFi lending protocol that enables uncollateralized crypto loans. Institutional borrowers can obtain flexible and competitive loan terms. Uncollateralized loans function as a revolving line of credit, giving borrowers flexibility for recurrent and short term liquidity needs. Lenders earn high returns on actively loaned out capital and have granular control over their investment portfolios. Unused capital is placed on a trusted third-party liquidity protocol, while simultaneously earning additional returns from Atlendis. There is no idle capital on Atlendis. Atlendis enables trusted borrowing and lending, opening a wide range of use cases for borrowers.

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.