使用 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 的赎回逻辑中识别并纠正了一个微妙但重要的Issue，确保了公平性和可信赖性。这突出了形式化方法在保护智能合约和维护 DeFi 生态系统中基本经济公平方面的关键作用。

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

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

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