AI 中文总结
SpecTrum是一个规范引导式差异模糊测试框架，通过机械化以太坊共识规范、定义前提覆盖率、生成针对性测试输入，识别出5个主流以太坊共识客户端间的27个跨客户端分歧案例，其中22个为新增发现。
AI 中文摘要
以太坊的共识安全性依赖于独立的共识客户端实现对每一次状态转换达成一致。当它们因实现错误而出现分歧时，网络可能发生分叉、最终性停滞，甚至可能遭受严重攻击。为防止此类共识分歧，以太坊提供了Python参考实现（consensus-spec）作为规范，以及手工构建的官方测试套件（spectests）。然而，作为可执行实现，以太坊的规范通过运行时行为隐式定义有效性，因此缺乏确保所有有效性条件都得到充分评估的系统方法。我们提出SpecTrum，一个分三个阶段解决该问题的框架：第一，我们引入Consensus-SpecTec，即以太坊共识算法的机械化规范，它将有效性条件明确为if前提；第二，我们定义前提覆盖率，即衡量spectests在跨测试中被评估为真和假的if前提的指标；第三，我们开发一个基于规范的测试生成器，它提取spectests未评估为假的前提的约束，并生成输入以评估这些前提。将SpecTrum应用于五个主要以太坊共识客户端，我们识别出27个跨客户端分歧案例，其中22个在未插入我们机械化的前提时无法被发现。所有27个案例在分叉版本间均可复现，且将机械化规范扩展至新分叉所需工作量与规范差异成正比，规模适中。
英文摘要
Ethereum's consensus safety relies on independent consensus client implementations agreeing on every state transition. When they diverge due to implementation errors, the network can fork, finality can stall, and severe attacks are possible. To prevent such consensus divergences, Ethereum provides a Python reference implementation (consensus-spec), which acts as a specification, and a hand-crafted official test suite (spectests). However, as an executable implementation, Ethereum's specification defines validity implicitly through runtime behavior. As a result, it lacks a systematic way to ensure that all validity conditions are thoroughly evaluated. We present SpecTrum, a framework that addresses this problem in three stages. First, we introduce Consensus-SpecTec, a mechanized specification of the Ethereum consensus algorithm, which makes validity conditions explicit as if-premises. Second, we define premise coverage, a metric that measures which if-premises are evaluated to true and false across spectests. Third, we develop a specification-based test generator that extracts constraints on premises not evaluated to false by spectests and generates inputs to evaluate them. Applying SpecTrum to five major Ethereum consensus clients, we identify 27 cross-client divergence cases, 22 of which cannot be found without the premises inserted in our mechanization. All 27 cases reproduce across fork versions, and extending the mechanized specification to a new fork takes modest effort proportional to the specification difference.
Comments12 pages. Accepted at the 41st IEEE/ACM International Conference on Automated Software Engineering (ASE 2026)
