Certora 对 Sui 链上的借贷协议 Suilend 进行了形式化验证，重点分析了系统级不变量。验证涵盖了偿付能力、账户健康度以及清算盈利性三个维度，识别并修复了包括双重舍入漏洞、算术舍入漂移以及特定 LTV 条件下清算导致资产状况恶化等技术问题，确保了协议的整体安全性。
借贷协议看起来很简单：存款、借款、偿还、清算。但保持借贷协议偿付能力的属性并不存在于任何单一函数中。它们源于操作的组合方式。在某些条件下，存款本身是安全的，但当它与清算交互时可能会导致资不抵债。重要的漏洞在于这些交互中，而发现它们需要证明整个系统的属性。
Certora 团队通过编写并证明系统级不变性（system-level invariants），对 Sui 上的 Suilend 进行了形式化验证。这些属性必须在每一个操作、每一个可达状态以及每一个可能的调用序列中保持成立。我们将验证围绕三个类别进行：偿付能力、账户健康度和清算。
虽然在 Suilend 中发现的漏洞都不是关键性的，也没有让资金处于立即的风险之中，但它们的微妙性和复杂性说明了形式化验证的深度，也是对 Suilend 现有安全性的证明。
证明偿付能力
cToken 比率必须保持 >= 1。如果不是这样，存款人就无法完全赎回。我们证明了这一点是成立的，没有任何用户行为可以降低它，并且储备金的内部记账从未声称拥有比链上实际存在的更多的流动性。
cToken 比率的研究中发现了一个双重舍入漏洞 (M-01)。铸造功能有两个堆叠的截断（truncations），导致存款人获得的份额略多于其存款的价值。虽然每笔交易的影响很小，但它会累积。每一次存款都在悄悄稀释现有的持有者。
账户健康度
只要价格和利息没有变动，一个健康的头寸在任何用户操作后都应该保持健康。我们证明了这一点，以及预期的 LTV 单调性（随债务增加，随抵押品减少），以及借款需要抵押品支持。
这里有两个发现。L-01：协议使用舍入算术增量更新健康度聚合数据，增量更新可能会偏离完整的重新计算，足以让一个头寸在借款后通过健康检查，然后在下一次刷新时失败。L-02：借款金额小到其美元价值截断为零，从而完全绕过了抵押检查。
清算与盈利能力
大多数关于借贷协议的形式化验证工作都证明了清算会将正确的 Token 转移到正确的地方，这虽然是必要的，但并没有解决实际风险。清算可以正确地转移资金，但仍使头寸比以前更糟。
我们更进一步，证明了清算总能改善头寸的 LTV，并且对清算人来说总是有利可图的（即使奖金为零）。盈利属性很重要，因为如果清算人赚不到钱，他们就不会出现，坏账就会积累，无人清理。
M-02 是最有趣的发现。当头寸清算前的 LTV 超过 1/(1+bonus) 时，清算实际上恶化了 LTV。每一步都使其更高。重复的清算可能会使头寸陷入资不抵债。修复方案是对源自当前 LTV 的奖金设置动态上限，这样操作只能将头寸引向正确的方向。
验证重要属性的挑战
在生产代码上证明这些都不简单。你需要对协议有足够的了解，以识别哪些属性真正保护了用户，然后弄清楚如何以适合形式化验证的方式表达它们。我们正在证明“这个协议是否具有偿付能力？”而不是“这个函数是否返回了正确的数字？”，这两者是完全不同难度的级别。
选择证明什么是大部分工作。偿付能力、账户健康度和清算的正确性，需要对整个系统中存储字段之间的关系进行推理，而不是孤立地验证单个函数。这也是我们发现漏洞的地方，这可能不是巧合。
查看完整报告了解详情：https://www.certora.com/reports/suilend
