技术摘要：SpecTrum

问题陈述

以太坊的共识安全性依赖于独立客户端实现（如 Lighthouse、Lodestar、Nimbus、Prysm、Teku）对每一次状态转换达成一致。这些实现之间的分歧可能导致网络分叉、最终性停滞或严重的攻击。目前，合规性是通过官方 Python 参考实现（consensus-spec）和手工构建的测试套件（spectests）进行验证的。

识别出的核心局限性在于：consensus-spec 通过运行时行为（例如，因溢出、断言失败或越界访问而抛出异常）隐式地定义有效性，而非将其定义为显式的逻辑条件。因此：

1. 隐式有效性： 有效性条件隐藏在诸如变量修改、条件跌落（fallthrough）或运行时异常等实现细节背后。
2. 测试不足： 现有的差异化模糊测试工具在选择变异目标时，并未参考这些隐式有效性条件，导致无法充分覆盖共识漏洞经常出现的边界情况。
3. 覆盖率盲区： 标准的代码级覆盖率指标无法捕捉这些隐式条件，因为它们不会在控制流中表现为显式的分支。

方法论

作者提出了 SpecTrum，这是一个规范引导的差异化模糊测试框架，旨在暴露隐式有效性条件并生成测试以评估这些条件。该框架分为三个主要阶段：

1. 机械化规范 (Consensus-SpecTec)

SpecTrum 的基础是 Consensus-SpecTec，这是使用 SpecTec 领域特定语言（DSL）编写的以太坊共识算法的机械化规范。这一阶段将隐式的 Python 实现转化为显式的形式化模型：

• 显式变异语义： 状态修改操作被定义为关系（relations），其结论明确列出了被修改的字段。
• 显式分支结构： 每个执行路径都被编码为一个独立的规则，消除了重叠 if 块带来的歧义。
• 显式异常边界： 隐式的运行时异常（例如，算术溢出、数组索引越界）被转换为显式的 if-premises（守卫条件）。例如，一个隐式的溢出检查变成了显式的条件 if total_bal <= $UINT64_MAX / 2。

2. 前提覆盖率分析 (Premise Coverage Analysis)

作者定义了 前提覆盖率（premise coverage），这是一种结构化指标，用于追踪测试套件是否对机械化规范中的每个 if-premise 都进行了 true 和 false 的评估。

• 目标识别： 系统分析官方的 spectests 以识别“目标前提”——即从未被评估为 false（未被证伪）的条件。
• 过滤： 排除不可证伪的前提（恒真式或闭合分支）和未尝试的前提（从未到达），从而留下需要测试的可证伪条件集。

3. 规范引导的测试生成

测试生成器利用机械化规范来创建能够证伪目标前提的输入：

• 溯源传播： 系统将运行时值追溯到其在输入 JSON（状态或区块）中的源字段，以确定哪些字段影响了特定的前提。
• 建议提取： 对于评估为 true 的目标前提，生成器通过否定该条件（例如，将 <= 改为 >）来确定证伪该条件所需的约束。
• 变异应用： 生成器从由否定约束派生的区间中采样数值，包括边界值、过渡值和内部值，以产生变异后的测试用例。
• 差异化测试： 生成的测试在五个主要的客户端和参考实现之间执行。输出结果的不一致（接受/拒绝、后状态差异或崩溃）将被报告为分歧。

核心贡献

1. Consensus-SpecTec： 首次将 SpecTec 方法应用于非编程语言软件，将以太坊共识算法的隐式有效性条件显式化为 if-premises。
2. 前提覆盖率： 一种定义在 if-premises 之上的新结构化覆盖率指标，能够识别标准代码覆盖率无法捕捉且被官方套件测试不足的有效性条件。
3. 规范引导生成器： 一个能够追踪输入溯源并提取约束的工具，将前提覆盖率从 46.3% 提升至 91.1%。
4. 实证评估： 通过全面的评估证明了该框架在发现跨客户端分歧方面的有效性及其在协议分叉中的实用性。

结果

应用于五个主要的以太坊共识客户端（Lighthouse, Lodestar, Nimbus, Prysm, Teku）的 Capella 分叉配置：

• 分歧发现： SpecTrum 在六个根因类别中识别出 27 个跨客户端分歧案例：前提违反、有损解码、配置不一致、数值下溢/上溢、状态更新不一致以及不变性强制执行不一致。
• 分类：
  • A 类（共识失败）： 4 个案例中，客户端在完全验证下计算出不同的后状态，存在导致链分叉的风险。
  • B 类（活性失败）： 23 个案例中，客户端虽然对接受/拒绝达成一致，但在内部状态或提议者行为上存在分歧，导致奖励丢失或区块生产无效。
• 对机械化的依赖： 27 个案例中的 22 个 如果没有 Consensus-SpecTec 插入的显式前提，是无法被发现的。
• 基准对比：
  • 与官方 spectests 相比，SpecTrum 将前提覆盖率从 46.3% 提高到了 91.1%。
  • 在同等预算下，与无引导的变异策略（随机和极端策略）相比，SpecTrum 发现了更多的分歧（27 个对比 12 个和 16 个），并且找出了所有的 4 个 A 类失败案例。
  • 代码级分支覆盖率仅略有增加（例如，consensus-spec 中仅增加了 1 行），这凸显了前提覆盖率能够捕捉到标准分支指标无法察觉的有效性条件。
• 跨分叉可复现性： 所有 27 个案例在 Deneb 分叉配置下均能完全一致地复现。将机械化规范从 Capella 扩展到 Deneb 仅需 26 行更改（约 1%），证明了极低的维护成本。

重要意义

本文认为，以太坊共识客户端中的跨客户端分歧最有可能产生于那些参考实现留下的隐式有效性边界，且现有测试套件未能系统性地练习这些边界。通过将规范机械化以使这些条件显式化，SpecTrum 提供了一种系统的方法来评估它们，从而揭示了传统差异化模糊测试和代码覆盖率所遗漏的漏洞。该框架被视为一种实用的工具，通过识别潜在故障，在这些故障演变为网络故障之前提高以太坊网络的韧性。所有识别出的分歧均已向以太坊协议漏洞赏金计划报告。