Lending protocols are the backbone of DeFi. This post breaks down the core mechanics of a Compound V2-style lending protocol on Sui, where the real bugs hide, and what I learned from formal verification with Certora.
Lending protocols hold the largest share of Total Value Locked (TVL) across all of DeFi. Aave, Compound, and their forks collectively hold tens of billions of dollars. When they break, the damage is measured in hundreds of millions. They're also deceptively complex — the basic concept of "deposit collateral, borrow assets" hides layers of interest accrual, oracle integration, liquidation mechanics, and risk parameter management that interact in subtle ways.
I recently spent weeks auditing Current Finance (also known as Pebble Lending) — a Compound V2-style lending protocol built in Move on Sui, as part of a Sherlock contest. The protocol had already undergone two prior audits (Asymptotic and MoveBit). This post distills what I learned — the mechanics, the bugs, and the formal verification experiments.
Every lending protocol follows the same fundamental loop: users deposit assets to earn interest, and other users borrow those assets by putting up collateral. If a borrower's collateral value drops too low relative to their debt, they get liquidated — a third party repays part of their debt and seizes their collateral at a discount.
Let's break down each one and learn where bugs hide.
When you deposit ETH into a lending protocol, you receive cTokens (or similar receipt tokens). These cTokens represent your share of the pool. As borrowers pay interest, the exchange rate between cTokens and the underlying asset increases — your cTokens become worth more ETH over time.
The exchange rate is the accounting anchor of the entire protocol. Every deposit, withdrawal, borrow, and repayment flows through it. A bug in the exchange rate calculation corrupts every operation downstream.
Audit target — First depositor inflation: In EVM lending protocols, a classic attack involves the first depositor inflating the exchange rate by donating tokens directly to the reserve contract. On Sui, this attack is structurally prevented — the object model doesn't allow direct token transfers to a reserve object without going through the protocol's entry points. This is one of the security benefits of Sui's object-centric architecture.
Sui-specific: Sui's object model means every asset is an object with explicit ownership. You can't "accidentally" send tokens to a contract address like in EVM. This eliminates an entire class of donation/inflation attacks that plague Solidity lending protocols. That said, it introduces its own patterns — like the Coin<CToken<MarketType, CoinType>> generic nesting that defines each unique cToken type.
Interest doesn't accrue continuously for every borrower on every block. That would be too expensive. Instead, lending protocols use a borrow index — a single cumulative multiplier that starts at 1.0 and grows every time someone interacts with the protocol.
This "lazy evaluation" pattern means the protocol only updates state when someone actually interacts with a reserve. But this creates a dangerous timing dependency: interest must be accrued BEFORE any state-dependent reads.
Bug found — Retroactive interest model application: When an admin updates the interest model (say, from 2.3% APR to 300% APR), the protocol should first accrue all pending interest at the old rate, then switch to the new one. In the audited protocol, this pre-accrual step was missing. The new rate was retroactively applied to the entire period since the last accrual. If nobody touched the reserve for 7 days and the admin updated the model, those 7 days got charged at the new 300% rate instead of the old 2.3%.
The fix: Call accrue_interest() before updating the model. This settles all pending interest at the old rate, ensuring the new rate only applies going forward. This is a universal pattern — any parameter that affects interest calculation must be preceded by an accrual.
The audited protocol uses Pyth oracles with a dual-price system: an EMA (Exponential Moving Average) price for safety checks, and a spot price for liquidation seizure calculations. This dual approach is supposed to provide stability (EMA smooths short-term volatility) while ensuring liquidators are incentivized with real-time pricing.
Each asset has an independent check: if EMA and spot diverge by more than 10%, the operation is blocked. Sounds safe, right? Here's where it breaks.
Bug found — EMA/Spot deviations compose across assets: The per-asset divergence check works fine in isolation. But when a borrower has one asset as collateral and another as debt, the deviations multiply. If the collateral's EMA is biased 10% high and the debt's EMA is biased 10% low — both within tolerance — the combined mismatch is ~21%. The borrower opens a position that's already insolvent at spot prices but appears healthy in EMA. Then, because liquidation eligibility also uses EMA, the position cannot be liquidated. It's a phantom-healthy zombie position.
E-Mode (Efficiency Mode) groups are a concept popularized by Aave V3. They allow the protocol to offer higher collateral factors for correlated assets (e.g., ETH/stETH, USDC/USDT). Each obligation is locked to a single eMode group at creation, and the group defines per-asset risk parameters: collateral_factor, liquidation_factor, liquidation_incentive, and borrow_weight.
Critical invariant: An obligation's eMode group must never change after creation. If it could, an attacker could create an obligation in one eMode group, borrow assets allowed there, then switch to a different group with more favorable parameters — bypassing the risk restrictions that were supposed to apply. We formally verified this invariant with Certora — more on that later.
E-Mode groups also track aggregate borrows per asset within the group. This aggregate is used to enforce borrow caps. But here's the catch — the aggregate uses delta-based accounting:
Bug found — Stale borrow cap aggregate: When a borrower interacts with the protocol, update_asset_borrow() captures the old_value of that specific obligation's debt and computes the delta. But the "old value" is only the debt as of the last time that specific obligation was touched. Interest accrued on all other idle obligations is permanently invisible to the group aggregate. Over time, real group debt silently exceeds the configured max_borrow_amount.
The lesson: Delta-based accounting is a common optimization in DeFi — only updating state based on the difference from last known value. It works fine for individual positions but breaks when used for aggregate tracking, because the "last known value" of each position freezes the moment it was last touched, making passive interest invisible to the aggregate.
Liquidation is the protocol's last line of defense against bad debt. When a borrower's health factor drops below 1.0 (debt exceeds collateral * liquidation_factor), anyone can repay a portion of their debt and seize their collateral at a bonus — the liquidation incentive.
Three distinct bugs affect the liquidation engine in this protocol:
liquidate_ctokens function immediately redeems seized cTokens into underlying tokens in the same transaction. But when the reserve has high utilization, borrowers have drained the idle cash. The liquidator tries to withdraw, say, 69.3 ETH from a reserve that only has 0.1 ETH of idle cash — the transaction reverts. Unhealthy positions can't be liquidated, and bad debt accumulates. The standard fix is to give the liquidator cTokens instead of underlying, and let them redeem later when liquidity returns.liquidate calls in a single PTB, each independently passing the 50% check against the full original debt. Result: near-full position drain in one atomic transaction, far exceeding the intended 50% cap.reserve.debt() (total debt across ALL eMode groups) instead of emode_group.borrow_amount() (group-specific debt). When one eMode group's debt is healthy but another group's debt inflates the reserve total past the ADL threshold, healthy positions in the first group get force-liquidated.Rate limiters enforce rolling-window outflow caps per eMode group per asset — preventing large, rapid drains. They use a sliding window divided into time segments, tracking accumulated outflow in each segment.
Bug found — eMode update resets rate limiters: The update() function in emode.move is monolithic — it takes all eMode parameters as input and rebuilds the entire structure. This includes unconditionally rebuilding rate limiters via new_from_struct(). When an admin adjusts an unrelated parameter like collateral_factor, the accumulated outflow history is wiped. Users can immediately consume the full limit again in the same window. In testing, this allowed 9M in borrows against a 5M limit — 1.8x the intended cap.
The lesson: Monolithic setter functions that rebuild entire structs are a recurring bug pattern. When struct A contains both config parameters and runtime state (like accumulated history), an update to the config also resets the state. The fix: separate the update paths, or only rebuild the limiter when the limiter-specific parameters actually change.
This bug is subtle enough that I used formal verification to prove it exists. The deposit limit check in reserve.move is supposed to ensure total deposits don't exceed a configured maximum. Here's the formula:
The total_deposit_plus_interest() function already subtracts cash_reserve via the exchange rate calculation. Then deposit_limit_breached() subtracts it again in the comparison. The effect: the deposit cap is under-enforced by exactly cash_reserve. As protocol fees accumulate, the gap widens.
One of the most valuable parts of this audit was writing Certora CVL specifications for the protocol's core invariants. Certora's prover can mathematically prove that an invariant holds across all possible inputs and states — not just the ones you thought to test.
emode_group field never changes after creation, across all obligation-mutating functions (accrue_interest, deposit_ctoken, withdraw_ctokens, try_borrow_asset, repay_debt). This prevents an attacker from switching risk profiles mid-position.u256 value must never decrease, across all reserve-mutating functions. A 3-level chained field access (Reserve → BorrowIndex → Decimal → u256) was needed to express this. If the index could decrease, outstanding debts would shrink, causing protocol insolvency.try_borrow_asset) can add new debt types to an obligation. This is a compositional proof: try_borrow_asset is only called from market::handle_borrow, which enforces the eMode asset restriction via borrow_mut_emode().cash_reserve > 0. This is formal verification being used offensively — to prove a bug exists, not that code is correct.Key insight: Formal verification isn't just for proving code is correct. It's equally powerful for proving bugs exist. Write the property you want to hold, run the prover, and if it finds a violation, you've got a mathematically proven bug with a concrete counterexample. This is stronger evidence than any PoC test.
These are the patterns that actually found bugs in this audit:
For every admin action, every parameter update, every model change — check if interest is accrued first. The retroactive interest model bug is a direct consequence of missing this check. This applies to interest rates, reserve factors, collateral factors — anything that changes how interest is calculated or how balances are interpreted.
Whenever you see aggregate tracking (total borrows, total deposits, group-level caps), ask: does the aggregate stay in sync with the sum of individual values? Delta-based tracking is an optimization that creates drift. The eMode borrow cap drift is a textbook example — individual obligations accrue interest invisibly to the group aggregate.
When a function operates at one scope (eMode group) but checks a constraint at a different scope (reserve-level), that's a scope mismatch. The ADL bug checks reserve-level debt for a group-level operation. Always verify that the check's scope matches the action's scope.
Functions that rebuild entire structs from scratch are dangerous when those structs contain runtime state alongside configuration. The eMode rate limiter reset is caused by a monolithic update() that doesn't distinguish between "config I want to change" and "state I need to preserve." Look for structs that mix config and state, then check if update functions accidentally reset state.
When a value is computed by composing multiple functions, trace the full computation chain. The deposit limit double-subtraction only becomes visible when you expand total_deposit_plus_interest() and see that cash_reserve is already subtracted inside, then subtracted again outside. Inline every helper mentally — or write a formal spec.
Does the liquidation function assume it can withdraw underlying tokens? At high utilization, it can't. Does the liquidation function assume it can execute in a single call? With close factor enforcement per-call and Sui's PTB, it can be called multiple times atomically. Every assumption the liquidation engine makes about its execution context is a potential bug.
When a system validates prices per-asset but uses those prices in cross-asset calculations (like collateral value / debt value), individual tolerances compound. A 10% tolerance per asset becomes a 21% tolerance when assets deviate in opposite directions. Check if per-asset validation is sufficient for multi-asset accounting.
Having audited both Sui and Aptos Move protocols, here are the key differences that matter for security researchers:
move_to, borrow_global). On Sui, you pass objects explicitly as function arguments — which makes data flow more visible but also means you need to understand dynamic_field patterns, where state is attached to objects dynamically and can be harder to discover during audits.public(package) is the same concept, different ergonomics. Both Sui and Aptos Move use public(package) (formerly public(friend) on Aptos) for module-level access control. On Sui, entry functions are the external attack surface. On Aptos, public fun is the danger — any module can call it. Both require the same audit pattern: grep for visibility outliers.drop ability that must be consumed in the same transaction). This is a powerful guarantee — the flash loan struct forces repayment. On Aptos, flash loans typically use a callback pattern. The hot potato is structurally safer.coin::transfer to any address. On Sui, objects are explicitly owned — you can't send a Coin object into a Reserve object without calling a function that accepts it.dynamic_field and dynamic_object_field to attach state to objects. During an audit, the struct definition won't show you all the state — you need to grep for dynamic_field::add and dynamic_field::borrow to discover the full state surface. This is a common blind spot.Auditing a lending protocol is an exercise in understanding accounting. Every bug I found came from a mismatch between what the code computes and what it should compute — a delta that misses passive interest, a formula that subtracts a term twice, a scope that's too broad, a setter that doesn't know what to preserve.
The formal verification work was the highlight of this audit. Using Certora not just to prove invariants but to prove bugs exist feels like a genuine advancement in audit methodology. When you can show a prover that two formulas should be equivalent and it hands you a counterexample — that's a level of certainty no PoC test can match.
If you're just starting in lending protocol audits, start with the exchange rate formula. Understand how every function in the protocol affects the four variables (debt, cash, cash_reserve, total_supply). Once you internalize that, the rest is tracing interactions and questioning assumptions.
The most dangerous bugs in lending protocols aren't in the complex math — they're in the simple accounting that everyone assumed was already correct.
📝 Sui Move evolves fast — if any tip here is outdated, incorrect, or no longer applies, please reach out on X so I can update this article accordingly.