DeepHigh
  • Welcome
  • Architecture
    • Compound
    • Venus
  • Threat Modeling
    • Identification of Function
    • Risk Library
    • Threat Enumeration
      • Enumeration
    • Risk Tree
  • Lending Invariant
    • Invariant
      • Aave V3
      • Venus
      • Euler V2
      • BIFI
      • Inverse Finance
      • Omni
      • BendDAO
      • Airpuff
      • Goldfinch
      • Wildcat
    • General Precautions
  • Edge Function
    • Flash Loan
    • BadDept
      • Auction
    • Mode
      • E-Mode
    • Leverage
    • Custom Pool
Powered by GitBook
On this page
  • Collateral Deposit
  • Collateral Withdraw
  • Borrow
  • Repay
  • Liquidation
  • Interest and Reward
  • Oracle
  1. Lending Invariant
  2. Invariant

Aave V3

Aave is a decentralized non-custodial liquidity protocol where users can participate as suppliers or borrowers in a common pool. Suppliers provide liquidity to earn a passive income, while borrowers are able to borrow in an overcollateralized (perpetually) or undercollateralized (one-block liquidity) fashion.

Collateral Deposit

Invariants
O/X
Description

The block state of the market where collateral is deposited must be updated to the latest status.

O

-

Collateral deposits must not be allowed when the protocol is in a paused state.

O

There are separate pause and freeze functions.

Collateral Withdraw

Invariants
O/X
Description

Users can withdraw collateral only within the limits that do not exceed the set Loan-to-Value (LTV) ratio.

O

-

The block state of the market where collateral is withdrawn must be updated to the latest status.

O

-

Borrow

Invariants
O/X
Description

Collateral deposits must not be allowed when the protocol is in a paused state.

O

There are separate pause and freeze functions.

The borrower must be registered in the relevant market.

O

-

After executing the loan, the market's total borrow amount must not exceed the set borrow cap.

O

-

Borrowers cannot exceed the Loan-to-Value (LTV) ratio relative to their collateral.

O

-

Before executing a loan, the target market's block state must be updated to the latest status.

O

-

Repay

Invariants
O/X
Description

The block state of the repayment market must be updated to the latest status.

O

-

Repaying more than the borrowed amount is not allowed.

O

If the input amount for repayment exceeds the limit, it attempts to repay the user's total debt.

Liquidation

Invariants
O/X
Description

The liquidator can only liquidate borrowers whose Loan-to-Value (LTV) ratio exceeds the limit, resulting in a liquidity shortfall.

O

-

The liquidator's repayment amount must not exceed the close factor relative to the borrower's total borrow amount.

O

-

Both the market for the borrowed asset and the collateral asset must be updated with the latest block information.

O

-

The amount of collateral the liquidator receives cannot exceed the total collateral balance of the borrower.

O

-

The liquidator and the borrower cannot be the same account.

X

This feature is not checked.

The collateral and borrowed assets involved in the liquidation must be under the same administrative entity.

O

-

Interest and Reward

Invariants
O/X
Description

The borrow interest rate must not exceed the set maximum value.

O

-

During interest calculation, related state variables like total reserves, total borrows, and market indices must be updated to their latest statuses.

O

-

For fixed-point arithmetic, steps should be taken to prevent rounding issues in low decimal places, such as using correct operation order or a fixed-point library.

O

-

Oracle

Invariants
O/X
Description

The price of the underlying asset retrieved from the oracle must not be zero; if the price is zero, the transaction should be halted.

O

-

It verifies that the oracle value is up-to-date.

X

It uses the latestAnswer function, which is not recommended by third parties, and does not check if the data is up-to-date.


PreviousInvariantNextVenus

Last updated 7 months ago