Scallop借贷 — 全面形式化验证

概述

全面形式化验证（CFV）意味着证明能够实际保护资金的属性。这是我们针对 Scallop 借贷协议的报告。Scallop 是 Sui 区块链上的一个 DeFi 借贷协议，允许用户提供资产以赚取利息、以抵押品借款以及获取闪电贷。所有安全关键功能（资产负债表操作、清算、抵押品估值、访问控制和参数更新）都具有语义规范。整体 API 覆盖率达 100%。

报告范围

我们涵盖 Scallop 借贷协议的核心功能：管理功能、算术运算、锁定/解锁/时间锁机制以及资产负债表操作（铸币/赎回、借入/偿还、抵押品存入/取出、闪电贷）。我们还涵盖债务义务管理和清算评估。

我们证明：特权操作所需的 admin caps、安全的定点算术（经过溢出检查）、有界参数（例如用于清算/抵押品风险和利息计算）、精确的清算汇率数学，以及市场币铸造/赎回汇率的正确性。

验证亮点

治理保障（面向管理员）

参数更改需要链上时间锁，确保在更改生效前具有可见性。治理延迟只能延长，不能缩短。收入提款受累积金额限制，因此管理员不能提取超过所赚取的金额。风险参数（抵押因子、清算罚金等）有上限，以防止不安全的杠杆。所有特权操作都需要 AdminCap。请参阅“管理功能安全”和“风险参数界限”。

头寸保护（面向用户）

清算因子被证明大于抵押因子，确保头寸在资不抵债前变得可清算（参见“风险参数界限”）。用户义务受访问控制保护：我们证明只有匹配的 key 才能解锁义务，lock keys 必须在使用前注册，并且通过 key 匹配要求防止跨协议解锁攻击。不健康的头寸可以被强制解锁以进行清算，但健康的锁定头寸仍然受到保护。请参阅“义务访问控制”。

资产负债表完整性

所有资产负债表操作都被证明是精确的。供应操作（铸币/赎回）保留了汇率数学。债务操作（借入/偿还）保持了精确的现金/债务会计，我们证明现金减少了借入金额，债务相应增加。抵押品存入/取出在义务和市场层面都保持了精确的抵押品会计，其中存入被证明完全不改变资产负债表。闪电贷强制收取费用。请参阅“资产负债表操作”。

头寸安全

评估器函数强制执行安全限制。借款能力等于抵押品盈余价值；最大提款量从不超过存入的抵押品。清算金额有上限：最大清算量不能超过总抵押品，健康的头寸产生零清算。清算汇率被证明是精确的： $$ \texttt{liq_exchange_rate} = \frac{\texttt{scale_ratio} \times \texttt{price_ratio}}{1 - \texttt{liq_discount}} $$

请参阅“头寸安全评估器”。

算术安全

所有定点运算都具有溢出安全性和精度验证。请参阅“算术运算”。

方法论

证明结构

每个规范都与其目标函数的签名相呼应。规范主体建立前置条件（asserts——由证明器验证，requires——假设，通常用于结构上保证但重新推导成本较高的溢出界限），调用目标，然后陈述证明器必须完成的后置条件（ensures）。

中止建模

在可行的情况下，规范使用 asserts 前置条件来完整地建模中止条件，证明函数在前置条件满足时成功，否则中止。储备操作断言算术安全、足够的流动性和资源存在。义务操作断言所有权、锁定状态和 key 注册。算术规范断言非零除数和结果界限。

中止处理

对于那些穷尽中止建模不切实际的复合用户操作，规范使用 ignore_abort，仅验证成功执行的属性。中止条件仍然由实现层面的 assert! 语句强制执行，这些语句会回滚事务。例如，borrow 在现金不足时中止，force_unlock_unhealthy 在头寸健康时中止（参见“义务访问控制”）。规范证明成功时的正确状态更新；健康检查是一个实现保证，而不是一个已证明的后置条件。

访问控制

特权操作将 AdminCap 作为参数。在 Move 中，函数签名在字节码级别强制执行：调用者不能在不拥有 capability 对象的情况下调用此类函数。这是一个语言层面的保证，而不是证明器需要重新推导的属性。

已知限制

某些规范在结构上是完整的，但在推理 Sui 动态字段或某些算术辅助函数时遇到证明器限制，阻碍了完整的语义后置条件。这些规范仍然正确地建模了中止行为。如果某个单独的规范存在已知问题，则会在验证数据中进行跟踪。

验证详情

管理功能安全

时间锁强制执行

所有参数更改（利率模型、风险模型、流出限制器）都需要链上延迟期。我们证明更改不能在延迟期满之前应用，从而防止即时操纵。我们还证明时间锁值一旦创建就不可变，并且过期的时间锁可以销毁以清除过时的待处理更改。

延迟延长

治理延迟是非递减的。在规范中，这通过精确的字段进行检查，例如 interest_model_change_delay_after == current_interest_model_change_delay + delay（风险/限制器延迟也类似），因此管理员不能缩短延迟以匆忙推行更改。

AdminCap 要求

所有特权操作都需要 AdminCap。我们验证了每个此类操作的正确行为。

收入收集

管理员不能提取超过所赚取的金额。我们证明提款后： $$ \texttt{new_revenue} = \texttt{revenue} - \texttt{take_amount}, $$ $$ \texttt{new_cash} = \texttt{cash} - \texttt{take_amount}, $$ 并且金库余额精确地减少了提款金额。借款费用提款也同样受已收取费用的限制。

风险参数界限

抵押品与清算

我们证明了所有风险模型的硬上限和排序约束都得到强制执行。这些属性在借款限额和清算阈值之间创建了一个安全缓冲区，同时通过罚金/折扣排序保留了清算人的激励。

参数满足： $$ \begin{aligned} \texttt{collateral_factor} &\leq \texttt{MaxCollateralFactor}\ (95\%) \ \texttt{liquidation_factor} &\leq \texttt{MaxLiquidationFactor}\ (95\%) \ \texttt{liquidation_penalty} &\leq \texttt{MaxLiquidationPenalty}\ (20\%) \ \texttt{liquidation_discount} &\leq \texttt{MaxLiquidationDiscount}\ (15\%) \end{aligned} $$ 以及排序约束 $$ \begin{aligned} \texttt{liquidation_factor} &> \texttt{collateral_factor} \ \texttt{liquidation_penalty} &> \texttt{liquidation_discount} \end{aligned} $$

利率模型

Scallop 使用一种双拐点模型，其中利用率超过阈值“拐点”时利率增长更快。我们证明了实现中使用的利率参数排序是单调的： $$ \texttt{base_borrow_rate} \leq \texttt{borrow_rate_on_mid_kink} \leq \texttt{borrow_rate_on_high_kink} \leq \texttt{max_borrow_rate} $$

我们还验证了每个利用率区段的精确分段线性插值公式。这确保了正确的参数排序和精确的费率计算。

资产负债表操作

所有用户操作都与四部分资产负债表交互：现金、债务、收入和市场币供应。我们证明了以下每种操作类型的不变式；影响资产负债表的管理员提款在“管理功能安全”中涵盖。

本节中使用的定义：

利息累积

在任何资产负债表操作执行之前，协议会累积未结利息。我们证明了独立的累积不变式限制其副作用。对于所有资产类型同时（通过市场上每个 TypeName 的普遍量词证明），累积保留现金和市场币供应，而债务和收入非递减。这种单调性属性意味着利息累积不能被利用来减少借款人的债务。当累积与义务同时运行时，我们额外证明了义务的抵押品和所有五个锁定标志都得到保留。

供应操作（铸币/赎回）

汇率

在储备层面，我们证明了 reserve::mint_market_coin 和 reserve::redeem_underlying_coin 中精确的汇率数学： $$ \begin{aligned} \texttt{result.value()} &= \frac{\texttt{old_underlying_balance_value} \times \texttt{mcs}}{V} \ \texttt{result.value()} &= \frac{\texttt{market_coin_amount} \times V}{\texttt{mcs}} \end{aligned} $$ 当 $\texttt{mcs} = 0$ 时，铸币直接返回 old_underlying_balance_value。

资产负债表不变式

铸币后：现金因存款而增加，市场币供应量因铸造量而增加，债务和收入不变。赎回后：现金因提款而减少，供应量因销毁量而减少，$\texttt{cash_after} \geq \texttt{revenue_after}$（流动性得到保留）。

利息累积

铸币和赎回在内部在交易前累积利息。我们证明现金和供应量的变化是精确的： $$ \texttt{cash_after} = \texttt{cash} + \texttt{deposit} \qquad \texttt{mcs_after} = \texttt{mcs} + \texttt{minted} $$ 而债务和收入可能因累积利息而增加： $$ \texttt{debt_after} \geq \texttt{debt} \qquad \texttt{revenue_after} \geq \texttt{revenue} $$

债务操作（借入/偿还）

借入一致性

当用户借款时，我们证明协议保持精确的会计：现金减少借款金额，债务至少增加借款金额（考虑到累积利息），市场币供应量保持不变。至关重要的是，我们证明在任何借款执行之前 $\texttt{cash} \geq \texttt{borrow_amount}$，因此协议不能出借超过其持有的现金。 $$ \texttt{cash_after} = \texttt{cash} - \texttt{borrow_amount} \qquad \texttt{debt_after} \geq \texttt{debt} + \texttt{borrow_amount} $$

偿还安全

当用户偿还时，我们证明现金增加量受偿还金额限制，并且收入永不减少： $$ \texttt{cash_after} \geq \texttt{cash} \qquad (\texttt{cash_after} - \texttt{cash}) \leq \texttt{coin_value} $$ 市场币供应量保持不变，防止通过偿还路径进行铸币/销毁攻击。

抵押品操作（存入/取出）

存入抵押品

当用户存入抵押品时，我们证明了义务和市场层面的精确会计，每个相关的抵押品数量都增加了 amount。我们还证明资产负债表完全不变：存入抵押品不触及任何资产类型的现金、债务、收入或市场币供应量。 $$ \begin{aligned} \texttt{total_collateral_after} &= \texttt{total_collateral_before} + \texttt{amount} \ \texttt{collaterals_stats_amount_after} &= \texttt{colaterals_stats_amount_before} + \texttt{amount} \end{aligned} $$

取出抵押品

我们证明了义务和市场层面的精确会计，与存入对称。如果义务保留了抵押品类型，则用户级别和市场级别的抵押品都精确减少了提款金额，并且返回的币带有该价值： $$ \texttt{result.value()} = \texttt{withdraw_amount} $$ 资产负债表得到保留：现金和市场币供应量不变，而债务和收入非递减（因提款前的利息累积）。 $$ \begin{aligned} \texttt{total_collateral_after} &= \texttt{total_collateral_before} - \texttt{withdraw_amount} \ \texttt{collaterals_stats_amount_after} &= \texttt{colaterals_stats_amount_before} - \texttt{withdraw_amount} \end{aligned} $$

闪电贷

我们证明闪电贷借款不修改资产负债表（现金、债务、收入、供应量不变）。偿还需要 $\texttt{coin_value} \geq \texttt{loan_amount} + \texttt{fee}$，并且收取的费用会同时添加到现金和收入中。

义务访问控制

义务初始化

我们证明新创建的义务以干净状态启动：零奖励，lock key 设置为 none，所有五个操作锁（borrow、repay、deposit_collateral、withdraw_collateral、liquidate）初始化为 false。债务和抵押品表得到正确初始化和访问。这是以下访问控制不变式的基本情况；没有它，通过在受损的初始状态下创建义务，锁定/解锁保证可能会被绕过。

Lock Key 注册

Lock keys 必须在使用前在 ObligationAccessStore 中注册。我们证明 lock 要求 key 类型存在于存储的已注册 keys 中，从而防止未经授权的协议锁定用户义务。

Key 匹配

只有匹配的 key 才能解锁义务。我们证明 unlock 要求提供的 key 类型与义务当前的 lock key 完全匹配。防止跨协议解锁攻击。

强制解锁不健康头寸

当一个义务被锁定时，不能对其执行任何操作（借入、偿还、取出、存入、清算）。然而，如果一个头寸变得不健康，清算人必须能够解锁它。我们证明 force_unlock_unhealthy 完全清除所有锁：lock key 设置为 none，所有操作锁（借入、偿还、取出抵押品、存入抵押品、清算）都设置为 false。当头寸健康时，函数中止，这由一个实现层面的 assert! 强制执行，当 weighted_debts_value 不超过 collaterals_value（经折算的清算上下文抵押品价值）时回滚。规范证明成功时的锁清除；健康检查是一个实现保证，而不是一个已证明的后置条件： $$ \texttt{weighted_debts_value} > \texttt{collaterals_value} $$ 这确保了锁定的健康头寸受到保护，而不健康的头寸始终可以被解锁以进行清算。

头寸安全评估器

评估器函数根据抵押品和债务价值计算用户操作的安全限制。我们证明这些评估器正确地强制执行头寸健康约束。此处证明的评估器数学被“资产负债表操作”中的资产负债表操作所使用：借款和提款使用借款/提款限制，清算使用清算评估器输出。

抵押品和债务估值

每个评估器限制都取决于将原始代币头寸转换为美元价值。在这一层面上，一个小数缩放错误、一个缺失的风险因子或一个循环聚合错误，无论参数被如何严格地限制，都将使所有下游安全检查失效。我们证明了完整的估值流程：从预言机价格检索到每资产转换，再到投资组合级别的聚合。

每资产美元转换

我们证明了所有估值路径使用的基本公式。预言机价格被证明是新的（与当前区块时间戳匹配）、有效的 Q32 且非零。小数缩放被证明不会溢出： $$ \texttt{usd_value} = \frac{\texttt{price} \times \texttt{amount}}{10^{\texttt{decimals}}} $$

抵押品聚合

总抵押品价值被证明等于义务中每种抵押品类型的每资产美元价值的总和，每种类型都乘以其风险模型因子：collateral_factor 用于借款决策，liq_factor 用于清算阈值。这直接与“风险参数界限”中证明的排序约束（$\texttt{liq_factor} > \texttt{collateral_factor}$）相关联，确保清算使用比借款更宽松的估值。该证明使用一个循环不变式，断言在处理前 i 种类型后，当前总计等于其加权美元价值的部分总和：

#[spec_only(loop_inv(target = collaterals_value_usd_for_borrow))]

##[spec_only(loop_inv(target = collaterals_value_usd_for_borrow))]
fun collaterals_value_usd_for_borrow_loop_inv(
    obligation: &Obligation, market: &Market,
    coin_decimals_registry: &CoinDecimalsRegistry,
    x_oracle: &XOracle, clock: &Clock,
    i: u64, n: u64,
    total_value_usd: FixedPoint32,
    collateral_types: &vector<TypeName>,
): bool {
    // ...
}

债务聚合

总债务价值遵循相同的结构，具有类似的循环不变式。未加权变体汇总所有债务类型的原始美元价值；加权变体将每个项乘以来自利率模型的 borrow_weight，确保高风险债务类型对借款限额的贡献按比例增加。

结论与持续保证

• 原文链接： scallop.asymptotic.tech/...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～