Certora对SPL Stake Pool的形式化验证

SPL Stake Pool 程序 已上线近五年，目前帮助管理 Solana 最大型质押池中价值约 84.5 亿美元的质押 SOL。其复杂性和链上交互性使其成为形式上最难推理的 Solana 程序之一。2025 年 6 月，Certora 对 Solana 质押池程序进行了手动审计和形式化验证。

将手动审查与形式化方法相结合 使团队能够比传统审计更深入，发现了一些此前未被识别的缺陷。 形式化验证工作还促成了 11 个不变量的制定，这些不变量如今定义了协议的安全边界。Solana 质押池团队迅速响应，修复了所有关键问题并及时实施了补丁。

Solana 质押池程序

其核心功能是聚合用户的 SOL，将其分散委托给验证者，并分配质押奖励。

其表面上的简单性掩盖了巨大的复杂性：

• 它必须直接与 Solana 质押程序 交互，处理其无法完全控制的验证者和临时质押账户。这包括一个准备金质押账户，池子用于质押 SOL 的存入和提取。
• 这些账户可能因集群重启、奖励累积甚至劫持（恶意攻击者可重新初始化或重新利用未初始化的账户）而改变状态。

为了正确处理所有这些事件，池子执行详细的内部记账，以跟踪准备金和验证者质押账户。内部记账不仅跟踪余额，还跟踪验证者质押的状态，即质押是正在激活还是停用，是否准备好移除等。验证者质押账户的状态决定了其余额中有多少实际上被质押。虚拟记账（池子的内部记录）和物理记账（链上实际 lamports）之间的这种微妙互动正是证明质押池正确性具有挑战性的原因。

不变量如何揭示复杂系统

形式化验证通过使用不变量来帮助揭示像质押池程序这样的复杂系统。不变量是关于状态的数学属性，这些属性必须在协议操作的每个可能序列下都成立，即任何可通过某些计算到达的状态，该不变量必须为真。

Certora 的 FV 审计关注的一个这样的不变量是偿付能力，即系统的资产能否覆盖其所有债务。就质押池而言，简单来说，这转化为“程序发行的份额数小于或等于程序管理的总资金”。偿付能力至关重要，因为它通过保证质押池始终能够兑现提款，来保护用户免受资金损失。

由于系统的复杂性，该属性的形式化并不直接。我们首先需要识别并区分验证者实际持有和池子虚拟记账的资产与份额。

为此，我们定义了一些相关术语 $t$，其中后缀 $t_v$ 表示由质押池跟踪的虚拟数量，后缀 $t_p$ 表示物理数量。我们有：

• $shares_p$ —— 质押池发行的份额数
• $validatorBalance_v$ —— 池子对验证者质押账户（包括激活和临时账户）中资金的虚拟记账
• $validatorBalance_p$ —— 验证者质押账户中持有的 lamports
• $reserveBalance_p$ —— 准备金质押账户中持有的 lamports
• $totalLamports_v$ —— 池子内部控制资金的内部记账
• $totalLamports_p$ —— 池子控制的总 lamports，定义为准备金中的 lamports 与池子交互的所有验证者质押账户中 lamports 之和，即 $totalLamports_p \equiv reserveBalance_p + \sum validatorBalance_p$。

现在可以将偿付能力精确地表达为以下属性：

$shares_p \leq totalLamports_p$。

为了实现该属性的证明，我们组合了三个将虚拟记账与物理记账相关联的不变量，这些不变量蕴含了 Solana 质押池程序的偿付能力：

(不变量 1) $shares_p \leq totalLamports_v$ —— 将份额与池子的虚拟资产记账相关联。

(不变量 2) $totalLamports_v \leq reserveBalance_p + \sum validatorBalance_v$ —— 将虚拟记账与准备金质押账户中的物理记账以及验证者的虚拟余额相关联。熟悉质押池程序技术细节的读者可能能够看出为什么这里不存在严格相等。

(不变量 3) 对每个验证者，$validatorBalance_v \leq validatorBalance_p$ —— 补充了连接虚拟记账与物理记账的缺失部分。

不变量 1-3 不仅蕴含了偿付能力，还在质押账户的物理状态与池子的虚拟记账之间形成了清晰的数学关系。

请注意，证明 Solana 质押池满足不变量 1-3 需要建立许多额外的不变量，这些不变量将质押账户的状态与其余额相关联。其中最值得注意的是以下不变量：

(不变量 4) 池子必须始终能够从准备金质押账户中提取。

不变量 4 看起来可能很简单，但对于发现高严重性问题至关重要！

使用不变量发现缺陷

当根据不变量 4 评估质押池时，它被 WithdrawStake 指令违反了。考虑以下代码片段：

if *stake_split_from.key == stake_pool.reserve_stake {

    // 检查验证者质押账户是否有可提取的质押

    if has_transient_stake || has_active_stake {

        msg!(

            "Error withdrawing from reserve: validator stake accounts have lamports available, please use those first."

        );

        return Err(StakePoolError::StakeLamportsNotEqualToMinimum.into());

    }

当要从准备金质押账户提取质押时，协议会检查准备金质押账户是否有足够的最低余额用于租金。然而，协议未能确保准备金不会被完全耗尽。

确保准备金质押账户永远不会被完全耗尽至关重要，因为存在攻击者可能劫持它的可能性：一旦账户的 lamports 被耗尽，Solana 运行时会在交易结束时将其移除。然而，攻击者可以在交易结束前向已关闭的账户空投，防止其删除。因此，攻击者可以复活该质押账户并恶意与质押池交互。

完全耗尽准备金账户允许攻击者劫持并控制准备金质押账户。这可能会带来严重后果。例如，攻击者可以向准备金存入质押，导致质押池为攻击者铸造新份额。然而，由于攻击者仍然能够从准备金中提取 lamports，这些份额基本上是无偿发行给攻击者的。攻击者现在有能力操纵份额价格。除了上述攻击向量外，攻击者还可以窃取受害者存入准备金质押的任何资金。

结论

Certora 对 Solana 质押池的审计展示了形式化验证如何超越传统审计。仅仅通过建立重要属性并勾勒出它们的证明，就有助于识别仅通过对代码库进行逻辑剖析才能发现的严重攻击向量。

得益于协议偿付能力不变量的数学证明，我们识别出了表面测试无法发现的深层结构风险。最终结果：共发现 15 个问题，并制定了 11 个数学不变量，这些不变量将指导质押池程序未来的变更。

有了这些不变量，Solana 久经考验的质押协议现在也通过了形式化验证。有关不变量和发现的详细讨论，请参阅完整报告：https://www.certora.com/reports/solana-stake-pool

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