Silo Finance - 问题回顾

执行摘要

• 5月10日，Silo 团队通知我们一个关键漏洞，该漏洞是由一位外部研究人员报告的，并且在几天前已被修复。
• 我们对该问题、修复和其他代码基础进行了彻底调查和手动审查。
• 我们添加了特殊的正确性规则，以防止未来类似错误，并使用 Certora Prover 对 Silo 代码的漏洞和修复版本进行了测试。
• 我们可以确认 Silo 的修复成功缓解了该漏洞。
• Certora 将通过 Code4rena 分配 $100,000，用于在下一个 Silo 代码版本中撰写额外规则，以增强协议的安全性。
• 我们将利用我们的新开放源代码突变测试技术和 Gambit ，检查规则覆盖率。

详细报告

背景

Silo 是一个无权限和风险隔离的借贷协议，旨在为所有代币资产提供安全和高效的货币市场。

Silo Finance 的正式验证项目在 2022 年 5 月 7 日到 7 月 15 日之间进行，使用 Certora Prover 工具。在验证过程中，我们与 Silo Finance 密切合作。在了解协议的设计和代码库后，我们：

1. 指导 Silo 团队进行规则编写过程。

2. 在 Silo Finance 的帮助下进行了属性和规则的构建。

3. 审查了规范文件。

在验证过程中，大约编写了两百个正确规则。这些规则揭示了五个问题（其中两个为高风险，三个为中等风险）。Silo 团队解决了所有问题。在此过程中，Silo 团队掌握了 Certora Prover 的使用。其余规则证明了代码是正确和健全的。为 InterestRateModel 合约编写了 29 条规则。

完整报告可在此找到：

Formal Verification of Silo V1, July 2022

5月10日，Silo 团队通知我们一项关键漏洞，该漏洞是由一位外部研究人员报告的。Silo Finance 提供了该问题的详细说明，以及他们的缓解计划和代码修复。

采取的行动

Certora 将此问题视为最高优先级。我们的产品安全总监 Amit Levy，拥有 18 年的代码安全经验，组建了由两名安全研究人员和两名安全工程师组成的任务团队。研究人员的工作是审查脆弱和修复后的代码，而安全工程师则检查已验证的规则。研发团队协助解决 Certora Prover 的性能问题。

我们在三个不同的层面上采取了行动：

1. 理解漏洞

Silo 提供了潜在攻击的清晰和深入的解释。

有漏洞的代码存在于 Interest Rate Model contract 中。

利率模型负责为每项资产（基础资产和桥接资产）在任何给定时间计算动态利率。

在利率模型中，利用率是通过 totalBorrowedAmount 与 totalDeposits 的比率计算得出的。从 Silo 合约借入“捐赠的”流动性可能导致利用率超过 100%。因此，当利用率超过 100% 时，InterestRateModel 模型会将利用率视为临界，导致利率迅速飙升至天文数字，使抵押品价值数倍增加。尚未偿还的利息也会在抵押品计算中考虑。

上述条件允许抵押品操控。

攻击 POC：

1. 攻击者向 Silo 捐赠代币，增加代币的 totalBalance（但不增加 totalDeposits）。
2. 攻击者从 Silo 借入一定数量的这些代币，使得 amount <= totalBalance AND amount > totalDeposits。
3. utilizationRate 将超过 100%（borrow > totalDeposits）。
4. InterestRateModel 将计算出巨额利息。
5. 抵押代币价格将相应上涨，允许攻击者借入更多其他代币并消耗 Silo。

导致此漏洞的两个不同失败：

1. 借入金额不应超过总存款金额（utilizationRate > 100%）。
2. 利息不应在 utilizationRate > 100% 的情况下计算。

我们确认该漏洞存在于我们的工作库中。我们审查了规范文件，发现没有任何规则能够捕获这些失败。

为了减少计算时间，CVL 规则包含一个明确假设，即利用率不能超过 100%。因此，Certora Prover 并未识别出攻击。Certora 和 Silo 团队都意识到这一假设，并未将这些场景视为可行。

2. 检查修复

在我们理解漏洞和攻击场景后，我们审查了 Silo 的代码修复。Silo 选择通过在利息计算函数中添加限制和边界，以限制 utilizationRate 百分比并降低利息曲线，从而缓解漏洞。

我们通过问自己两个问题来调查修复：

1. 修复确实关闭了这一攻击场景的可能性吗？
2. 是否还有其他方式可以利用和滥用利用率超过 100% 的事实？

我们认为，这一修复确实阻止了攻击场景。提出的修复保持了安全的利率，不允许其以不理想的方式上升。我们未能找到其他会对协议造成伤害的高利用率方式。

3. 编写规则

在我们的手动检查和调查过程中，我们添加了规则，以保证修复纠正了问题。

我们编写了 以下规则：

1. cantExceedMaxUtilization — 确保利用率不能超过 100% 的不变量。这意味着没有人可以借入超过存款金额的金额。

我们已设置以下不变量：

getAssetTotalDeposits(asset) >= getAssetTotalBorrowAmount(asset)

我们已在修复后的版本上运行这一不变量，结果如预期获得了几项违规。如前所述，我们无法找到其他方法来利用这些不变量违规。

2. interestNotMoreThenMax — 用于测试修复并证明没有其他路径可以使利息超过其最大限制的规则。计划是对脆弱版本进行测试（预期看到违规）并在修复版本上进行验证（预期获证）。

我们编写的规则背后的逻辑是用参数测量最大的利息率，这将提供 100% utilization (10¹⁸)，然后在不要求任何利用率的情况下再次测量利率（这意味着没有利用率边界）。

然后我们放置以下逻辑表达式：

assert unbounded_interest <= max_interest;

通过这样做，我们证明在任何路径中，任何利息值不会超过从最大利用率计算出的最高利息金额。

然而，InterestRateModel 具有各种复杂的计算，难以进行正式验证。

不明确地，下面的函数在利息计算期间调用，包含了一种复杂的指数计算：

/// @notice Calculates the binary exponent of x using the binary

function exp2(uint256 x) internal pure returns (uint256 result) {..}

该函数导致规则的验证超时。

经过一些内部调查，我们最终提出了一个解决方案，并得到了 Silo 团队的批准：

1. 我们从源代码中删除了溢出检测。该函数包括对 exp2() 函数的调用。在溢出发生的情况下，利率将为 0，属性仍然成立。
2. 我们限制验证器只能利用 Silo 中已部署资产的配置及所有 fallback configurations，因为它们只能由其所有者更改。

在我们克服了超时后，我们在脆弱版本上运行规则，并得到预期违规，在修复版本上，我们确实得到了修复证明。

3. 修复一些规则以支持新版本的代码（由于接口变化）

教训

1. 规范需要不断完善
2. 不要放弃超时的规则

Certora Prover 使用了一种独特的正式验证技术。它将源代码和规范文件（包含规则）转换为 SMT 公式，然后可以通过多个 SMT 求解器进行求解。最终公式代表了代码中所有可能的运行路径，考虑了所有参数的任何值。这等同于对所有可能状态进行测试。

由于计算复杂性，并非所有生成的公式都可以被求解。如果工具能解决一个公式，我们将得到证明或反例。然而，如果无法求解公式，验证器将超时。

例如，复杂的代码和复杂的数学可能会导致此类超时。在 Silo 的利息计算中，我们面对复杂的数学和非线性操作。

当规则超时时，最佳解决方案是简化代码或规则。

简化迫使工具减少要检查的路径数量，使证明工作变得更容易和更快。有几种技术可以实现这一目标，其中一些涉及为验证过程创建假设。这些假设必须经过仔细检查。

3. 所有假设都必须经过证明和确认。

在原始项目中，我们假设利用率始终在 0–100 之间，以避免超时。因此，验证器忽略了任何其他场景。对于脆弱代码而言，这是一种不安全的假设。假设可以通过其他规则或仔细的手动审查予以证明。在我们的分析中，与 Silo 团队一起，我们批准了特定配置并初始化状态，修剪了一些不可行的路径，最终解决了利息模块规则的超时问题。

4. 无界利用率作为通用属性

借入超过总存款资产可能非常危险，我们在报告的漏洞中看到了这一点。

通过非存款函数捐赠或转移资产在借贷协议中很常见。正如我们在之前的攻击中看到的，捐赠可能导致不希望的代码行为。

Certora Prover 可以模拟这种情况，并在适当的规则下找到其任何后果。

我们针对利用率和利息模型所进行的规则可以被视为其他借贷协议的通用属性。

虽然每个协议可能有独特的特征和复杂性，但大多数借贷协议共享基础原则，这些原则应保持一致。这些原则可以用逻辑表达，并转换为 CVL 规则。

结论

Certora 很高兴能够帮助出色的 Silo 团队确保他们的代码安全。我们计划通过以下方式提供帮助：

1. 手动审查新代码。
2. 我们正在与 Code4rena 社区合作编写新正确性规则。我们将分配最多 $100,000 来寻找缺失规则并提出新建议。
3. 利用 Certora Prover 进行代码中漏洞的早期检测和规则的正式验证。
4. 利用 Gambit 查找规则是否覆盖了足够的场景。

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