使用 Certora Prover 形式化验证确保 infiniFi 中公平的赎回

infiniFi 是一个 DeFi 平台，通过管理在 Pendle、AAVE 和 Ethena 等热门协议上的存款来优化收益。用户存入 USDC 并收到 iUSD，这是一种收据代币，可以被质押或锁定以换取收益。锁定期限与特定 epoch 相关联，更长时间的承诺会因更高的乘数而获得奖励。该协议的模块化农场设置使其可以轻松地与各种 DeFi 策略集成，从而确保最佳回报和透明度。

与传统银行不同，infiniFi 让用户准确地选择他们愿意锁定多少流动性以及锁定的时间。

在赎回时，如果流动性不足以完成请求，则该请求将提交到先进先出 (FIFO) 队列，并按照流动性可用的顺序进行处理。这确保了公平性，特别是考虑到排队等待的用户可能会受到处罚（通过削减）。

然而，使用 Certora Prover（我们旨在检测智能合约问题的工具）进行的形式化验证检查发现了一个重要的故障：一个新的赎回请求将在现有的赎回请求仍然开放的情况下得到满足。这个问题被归类为高危漏洞，目前已得到解决。

infiniFi 中 iUSD 赎回背后的机制

当用户将 USDC 存入 infiniFi 时，他们会收到 iUSD 代币。然后，用户可以选择：

• 将 iUSD 转换为 siUSD 以获得即时流动性（可随时赎回）。
• 将 iUSD 转换为 liUSD-xw，锁定它以获得治理权和更高的收益乘数。

在内部，存款分配在流动性和非流动性收益来源之间。当用户赎回他们的 iUSD 时，系统首先尝试从流动性来源满足请求。如果没有足够的流动性可用，请求将进入队列，稍后将被注资。队列中的用户有资格获得削减，直到他们的赎回完成，这使得公平性至关重要。

绕过赎回队列

每当用户想要赎回资金时，他们会调用 redeem，触发 beforeRedeem hook 从流动性收益来源提取流动性以满足请求。如果流动性不足，赎回请求将添加到赎回队列中。

队列注资通过管理员触发的操作执行，这些操作为用户完成赎回提供必要的流动性。

然而，infiniFi 系统中可用的流动性是高度动态的，可能在瞬间增加或减少。新增加的流动性没有被用于现有的赎回请求，但可以在不首先考虑队列的情况下用于满足新的赎回请求。

示例场景：

• 区块 N：Alice 调用赎回 100。由于没有可用的流动性，因此将赎回请求添加到赎回队列中。
• 区块 N+1：由于收集的收益，系统中的流动性增加了 100。
• 区块 N+1：Bob 调用赎回 100。由于有 100 的流动性可用，他立即收到他的资金。Alice 的赎回请求仍然在队列中。

这违反了 FIFO 排序，并且使 Alice 不公平地受到削减。

使用 Certora Prover 形式化验证公平性

为了捕获和执行 FIFO 行为，我们的安全研究人员和形式化验证工程师使用 Certora Prover 编写了一个精确的规则：

规则：no_immediate_redemption_from_non_empty_queue

此规则断言，如果赎回队列是非空的，则新的赎回应不导致用户收到全部资产金额。它确保系统尊重待处理请求的优先级。

在原始代码上执行时，该规则失败，表明系统在某些情况下允许队列绕过。针对原始代码进行的测试显示失败，暴露了系统错误地允许新请求绕过现有赎回队列的实例。

修复队列以确保公平

解决方案涉及调整 RedeemController 中的赎回逻辑，以便无论流动性如何，只要队列不为空，新的赎回请求都会自动进入队列，从而确保 FIFO 排序。

修复版本中的关键部分：

这通过消除任何流动性比较的需要来简化流程。所有用户都得到公平对待，简化了流程并确保了对早期和后期赎回者的一致处理。

值得注意的是，通过此更改，不再需要将新的赎回金额与现有流动性进行比较。那些早期赎回和那些稍后赎回的人都得到公平的处理。避免部分注资使跟踪交易的过程更加简单。此处描述的更新后的逻辑在 infiniFi 平台中已上线并处于活动状态。

验证结果

应用修复程序后，使用 Certora Prover 重新测试了相同的规则 no_immediate_redemption_from_non_empty_queue。这一次，它成功通过，确认：

• 当队列不为空时，不能发生即时赎回。
• 队列中的用户优先于新请求。
• FIFO 排序始终如一地执行。

这提供了正式保证，即该错误已得到完全缓解，并且赎回行为现在与协议的公平性目标保持一致。

为什么这很重要？

公平性不仅仅关乎安全性；它还关乎金融系统中的信任和可预测性。正如这里所展示的，形式化验证有助于主动检测和解决关键问题。

形式化验证确保了关键经济和治理原则的完整性，从而维护了用户对 DeFi 协议的信任。

• 赎回队列必须优先，以确保公平的 FIFO 排序得到尊重，并且用户不会不公平地遭受削减。
• 正式规范有助于编码公平性属性，使其具有强制性而非期望性。
• Certora Prover 可以在部署前检测业务逻辑违规，这使得它在具有复杂状态转换或流动性约束的协议中尤其有价值。
• 修复后的重新验证至关重要，以确认预期的行为已恢复。

结论

我们的工程师通过严格的形式化验证，识别并纠正了 infiniFi 赎回逻辑中的一个微妙但重要的问题，从而确保了公平性和可信赖性。这突出了形式化方法在保护智能合约和维护 DeFi 生态系统中的基本经济公平性方面的重要作用。

通过将预期的 FIFO 行为编码为精确的规则并针对协议的实现进行验证，该团队确保了用户在所有条件下都得到一致和可预测的对待。

详细的调查结果和漏洞可在完整报告中找到：https://www.certora.com/reports/infinifi-protocol-formal-verification-report

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