🗒️ Summary

Asymptotic has conducted a comprehensive security audit and verification of the kai-leverage project, examining commit d6cdbbe of the codebase. Due to limitations in the Move Prover for post-Move 2024 code, we performed the verification of the code right before it was adapted for Move 2024. Finally, we make the verification artifacts available for CI integration down the line.

<aside> 🔗 Github repository: https://github.com/kunalabs-io/sui-smart-contracts Inspected commit: d6cdbbedc408b9a18abfdc038b13211cf6cb586c (not available in open-sourced repo) We audited an early pre kai-leverage-v1 version Verification commit: https://github.com/kklas/kai-leverage-audit/commit/b3de08596deb15f08c5910901d47c5512064374a Verification artifacts: https://github.com/asymptotic-code/kai-leverage-audit/commit/c4fd0012ebef59a40413a81cceaff4284bd1aada (private repo)

</aside>

Key Findings

• Critical Vulnerabilities: We identified three critical vulnerabilities (C-1, C-2, and C-3), with C-1 being a true vulnerability and C-2 and C-3 intentionally planted to verify audit quality.
  • C-1: A flash loan exploit allows liquidity providers to drain the pool. Remediated, and flash loan functionality was also subsequently removed from the contract before publishing.
  • C-2: Incorrect computation of max_liquidity_factor. Remediated.
  • C-3: Missing assertion in liquidation functions. Remediated.
• Medium and Low Severity Issues: Three low (L-1, L-2, L-3) severity issues were discovered, primarily related to incorrect checks and minor logic errors.
• Refactoring Suggestions: We proposed one refactoring suggestion (R-1) to improve code structure and type safety.

Verification Results

Formal verification was performed on key components of supply_pool.move and position_model.move. This process helped identify several vulnerabilities and confirmed critical properties of the system, including:

• Correct rounding behavior in EquityTreasury and DebtTreasury.
• Bookkeeping property in SupplyPool.
• Non-aborting behavior of critical functions in position_model.move.

Manual Audit Findings

The manual audit focused on access control, error handling, and code quality. While many aspects were implemented correctly, we identified areas requiring further clarification or improvement, particularly in access management and error handling.

Remediation Summary

The kai-leverage project team has addressed most of the identified issues. The critical flash loan vulnerability (C-1) was fixed by correctly calculating the interest added to the pool's value; furthermore, the flash loan functionality was fully removed from the smart contract before it was published. The intentionally planted vulnerabilities (C-2 and C-3) were also remediated. Of the low-severity issues, L-1 and L-2 were resolved by correcting the loop increment and borrowing condition respectively.L-3, regarding the incorrect treasury empty check, was not addressed, but the code is still safe due to other layers. The refactoring suggestion (R-1) to split the debt_bag into separate components was not implemented.