研究文章

使用 Event-B 形式化验证区块链共识机制

144 次观看

⸱

DOI：

10.3791/70193

⸱

2026年5月8日

 ,  , 
1Department of Computer Science & Engineering, Pranveer Singh Institute of Technology, AKTU, 2Department of Computer Science & Engineering, Institute of Engineering & Technology

本文内容

摘要

本研究提出了一种针对区块链共识机制与智能合约的形式化验证框架，采用Event-B方法。该方法结合了表示抽象、基于不变量的证明以及时间模型检验，可在部署前对安全性、活性以及抗双重支付能力进行形式化验证。

摘要

本研究利用 Event-B 和 Rodin 平台，建立了一个形式化基础的区块链共识机制与智能合约行为验证框架。与以往主要依赖仿真或针对孤立合约进行案例验证的方法不同，本工作融合了有限状态机（FSM）抽象、基于不变量的证明、精细化建模以及时序逻辑验证，用于分析工作量证明（PoW）、权益证明（PoS）以及防止双重支付的机制。Solidity 智能合约被抽象为有限状态机，并编码为 Event-B 模型，从而实现对状态转换和安全性约束的形式化描述。安全性属性——包括交易唯一性、状态一致性、访问控制执行以及账本不变量的保持——通过 Rodin 中自动生成的证明义务进行验证。共生成 312 项证明义务，其中 287 项（92%）被自动解除，25 项通过交互式证明完成，实现了完整的不变量覆盖。活性属性使用计算树逻辑（CTL）进行形式化描述，并通过模型检测进行验证，确认了在 PoS 条件下系统无死锁且最终能选出验证者。双重支付的防范通过状态一致的账本建模得以形式化实施，其唯一性约束在所有可达状态中均被证明成立。PoW 与 PoS 的协议级共识逻辑经过三个抽象层次的精细化建模，通过逐步精细化确保了区块完整性与验证者行为的正确性。结果表明，机器检查的证明能够提供超越基于仿真的评估的可验证正确性保障，建立了一条严格且可复现的验证流程，增强了区块链系统在正确性保障和协议级鲁棒性方面的可信度。

引言

区块链技术已发展为一种分布式账本范式，能够在无需依赖中心化机构的情况下实现去中心化的记录保存。通过在参与节点之间复制账本状态，并借助共识机制达成一致，区块链系统在开放且存在对抗的环境中提供了完整性、透明性和防篡改性。正如 Yaga 等人所述1，区块链架构结合了密码学原语、分布式共识协议和点对点通信，以确保已验证的交易在计算上极难被篡改。核心共识机制（如工作量证明（PoW）和权益证明（PoS））用于管理验证者的选取、区块验证以及账本同步。此外，智能合约通过嵌入可编程逻辑，能够自动执行预定义规则，从而扩展了区块链的功能，支持在金融、医疗和治理等多个领域的去中心化应用。随着区块链技术在高价值、安全关键环境中的部署日益广泛，确保共识机制和智能合约行为的正确性已成为维持系统运行可靠性的关键2。

尽管区块链系统具有去中心化的特性，但仍容易受到逻辑层面和协议层面漏洞的影响。当账本一致性约束未被严格实施时，可能发生双重支付攻击。共识层的弱点，例如验证者选择逻辑错误或区块验证规则存在缺陷，以及智能合约漏洞（如重入攻击和不恰当的访问控制），已在已部署的平台中导致重大财务损失。尽管经验测试和仿真框架被广泛用于评估工作量证明（PoW）和权益证明（PoS）协议的行为，但这些方法仅能提供示例性观察结果，无法提供全面的正确性保证。基于仿真的验证无法证明在所有可达状态下的不变性保持，也无法确保在所有执行路径下的安全性和活性属性。这一局限性凸显了对具有数学基础的验证技术的需求，此类技术能够对区块链系统进行超越观察分析的严格推理。

形式化方法通过数学逻辑实现系统建模与验证，为系统正确性提供了坚实基础3,4。Event-B 通过逐步精化扩展了这一范式，将系统表示为抽象状态机，其中系统状态受不变式约束，状态转换则建模为带有保护条件的事件5。Rodin 平台可自动生成证明义务，并支持其验证，从而实现对不变式保持性和状态一致性的机器检查验证6。经典的建模范式，如 B 方法7 和 Z8，展示了基于不变式的推理与形式化精化如何确保系统在不同开发阶段的正确性。这些方法已被广泛应用于任务关键和安全关键系统中，以在部署前确保系统的正确性9,10,11,12,13。进一步的扩展方法，如 UML-B 和图形化精化框架，进一步证明了基于精化的建模方法在复杂工业系统中的可扩展性14,15,16,17,18,19。这些进展表明，以精化驱动的形式化建模能够在有效管理系统复杂性的同时，保持强有力的正确性保障。

针对区块链系统，形式化验证方法也已得到探索。基于SMT的合约验证技术可自动检查Solidity程序中的断言，并在出现逻辑违规时生成反例20。诸如VERISOL等工具采用有限状态抽象进行智能合约验证2，而定理证明方法则将合约转换为F*等形式化推理框架21。此外，以太坊虚拟机的语义形式化使得对执行语义和漏洞检测的严格推理成为可能22。类似地，Coq等定理证明环境已被用于分析与共识相关的安全属性及事务正确性23。尽管这些方法提供了有价值的洞察，但它们通常仅独立关注合约层面的正确性或共识层面的属性。系统层面的账本不变量、共识状态转换与智能合约行为很少被整合到统一的基于精化的框架中，该框架需在不同规格层级与验证产物之间保持可追溯性。此外，许多现有方法侧重于漏洞检测或逻辑断言检查，而非跨多个精化层级的系统性不变量保持。

本研究通过提出一种统一的形式化验证框架，解决了这一方法论上的空白。该框架将 Solidity 智能合约的有限状态机（FSM）抽象、Event-B 精化建模以及在 Rodin 平台内由机器检查的证明义务消解相结合。与将合约验证与共识建模视为独立问题的传统方法不同，本框架在一个结构化的统一模型中，对工作量证明（PoW）和权益证明（PoS）的协议级状态转换、账本完整性约束、交易唯一性条件以及智能合约状态演化进行了形式化描述。安全性属性——包括不变量保持、交易唯一性、受控的状态转换以及账本一致性——被表达为 Event-B 不变量，并通过自动生成的证明义务加以验证。时序性和执行顺序相关的属性则使用计算树逻辑（CTL）进行描述，并通过模型检测进行验证，以确保超越静态不变量的正确性。本方法论的一项关键贡献在于建立了跨抽象层次的显式可追溯性：Solidity 函数被抽象为 FSM 转换，FSM 转换被编码为 Event-B 事件，而不变量与时序规范则直接关联至已消解的证明义务和模型检测结果。这种结构化映射确保每一项正确性声明均有机器验证的证据支持，并清晰区分了基于证明的保证与基于仿真的观察。

本研究的范围经过刻意限定，以确保精确性和分析清晰度。建模重点涵盖共识机制的协议级状态转换、账本完整性约束、交易唯一性属性以及智能合约的状态行为。网络层面的内容，如消息传播延迟、拜占庭对抗策略、分叉解决机制以及以太坊虚拟机（EVM）的详细Gas语义，均不在所定义的抽象边界之内。通过明确界定这些建模假设，该框架确保了验证结论与形式化验证的证明证据保持一致。本文其余部分将介绍抽象方法论、Event-B建模与精化过程、不变式与时序性质的验证程序，以及最终的验证结果。通过将区块链协议与智能合约的验证建立在基于精化的形式化建模和机器可检查证明的基础之上，本研究增强了方法论的严谨性，并提升了去中心化账本系统在部署前的正确性保障水平。

访问受限。请登录或开始试用以查看此内容。

方案

研究输入
本研究中使用了两个 Solidity 智能合约作为验证输入。第一个是简易的 DAO 风格合约，用作重入攻击的案例研究；第二个是经过简化的账本/状态转移合约，旨在测试针对双重支付的合约级约束。原始的 Solidity 源代码作为本协议中定义的抽象与验证过程的输入。此类合约所采用的通用转换过程如图1所示，该图展示了 Solidity 源代码在验证过程中逐步转换为有限状态机（FSM）、Event-B 和 SMV 模型的过程。

建模边界
形式化建模重点关注智能合约的控制流逻辑，包括函数的进入与退出行为、内部执行过程以及合约层面的状态转换。函数可见性（public、external、internal 和 private）与重入性分析相关的调用栈行为一并表示。抽象转换的类型（调用、发送、转账）被视为以太币转移的操作。

在抽象边界内，通过定义合约级不变量来确保交易的唯一性并防止双重支付。为了表示验证选择和区块完整性要求，协议逻辑抽象层基于工作量证明和权益证明的协议级状态转换进行定义。

抽象边界未包含网络层元素，包括待传递消息的调度、由任意数量跳数引起的时间延迟、分叉解决、采用拜占庭策略的网络对手、以太坊虚拟机语义、由网络节点控制的Gas语义、异常传播、异步执行、复杂的回退行为以及网络层面的最终性。因此，双重支付判定的结果仅适用于合约层面的不变性条件，而不构成网络层面关于最终性的共识。

工具与配置
Rodin 平台被用于对 Event-B（版本 3.7.0）模型进行建模、精化、生成证明义务以及完成证明，该平台启用了 PP、ML、SMT 和 Atelier-B 定理证明器，以实现证明的自动与交互式验证。nuXmv 版本 2.0.0 在生成的 SMV 模型上以完整的 CTL 探索模式运行，以执行 CTL 模型检验。

所有验证执行均在受控的计算环境中进行，使用 Ubuntu 22.04 LTS、OpenJDK 11 和 Python 3.10.12。采用 Web3（7.6.0）、NetworkX（3.4.2）、Matplotlib（3.8.0）、Graphviz（0.20.3）、NumPy（1.26.4）和 Pandas（2.2.2）实现模拟与可视化功能。该设计确保在相同执行条件下运行时，形式化验证与模拟结果均可复现。

转换工作流程
该验证过程包含四个阶段。首先将 Solidity 合约转换为有限状态机（FSM-SC）表示形式。随后，将 FSM-SC 模型编码至 Event-B 中，并明确定义其不变式和精化层级。接着，FSM-SC 抽象被转换为 nuXmv 中的 SMV 模型。验证结果以证明义务的履行情况统计和 CTL 模型检验结果进行报告，同时提供反例作为具体案例。

有限状态机构建
每个合约被抽象为一个有限状态机，定义如下：

用于计算过程分析的有限状态机符号表示方程。

其中：
S = 状态集合
S₀ = 初始状态
T = 转移关系
V = 可见性映射
G = 守护谓词
A = 动作/状态更新

算法 1：从 Solidity 构建有限状态机
输入：Solidity 源代码
输出：FSM-SC

1) 解析 Solidity 合约的抽象语法树。
2) 根据构造函数定义创建初始状态 S₀。
3) 对于每个 Solidity 函数 f，创建一个独立的控制状态 S_f，并记录其可见性 V(f) ∈ {public, external, internal, private}。
4) 对于函数 f 中的每条语句，通过从 require/assert 条件中提取守卫谓词，并从状态变量更新中提取动作，推导出一个转移 t。
5) 将转移 t 添加到 T 中。
6) 为 Ether 转移操作（call、send、transfer）、内部和外部调用、delegatecall、selfdestruct、tx.origin 使用、条件分支以及循环结构创建显式的转移类型。
7) 返回 FSM-SC = (S, S₀, T, V, G, A)。

每个 Solidity 函数都与一个不同的有限状态机（FSM）控制状态相关联。为了理解漏洞，与漏洞相关的执行流（例如，包含外部调用后跟余额更新的执行流）被显式地抽象为有序的转换。图 2 展示了一个 SimpleDAO 风格合约的 FSM-SC 图表示例，说明了在此构建阶段如何抽象出入口状态、外部调用转换以及状态更新序列。

将 FSM 编码为 Event-B
FSM 状态转移被表示为 Event-B 结构。所有转移均对应于 Event-B 事件，包括特定的保护条件和动作。

算法 2：FSM 转换为 Event-B 编码
输入：FSM-SC
输出：Event-B 机器与上下文

1) 在合约上下文中定义 STATE_SET 和 FUNCTION。
2) 声明表示 FSM 控制状态和合约级别状态的变量。
3) 使用 current_state ∈ STATE_SET 表示每个 FSM 控制状态 s ∈ S。
4) 对于每个转换 (s → s′, g, a)，创建一个 Event-B 事件 E_t，其条件为：
5) WHERE current_state = s ∧ g
6) THEN current_state := s′ ∥ apply(a)
7) 使用从 V(f) 推导出的保护条件编码可见性约束。
8) 定义不变式 inv1–inv9 以捕获安全性和一致性属性。
9) 通过赋值 S₀ 和默认值来定义 INITIALISATION。

状态集合、当前状态、函数可见性、调用栈、交易时间戳、以太币转移状态、代理调用标志、自毁标志以及验证条件是 Event-B 模型中捕获的一些变量。不变式（inv1-inv9）和初始化操作（act1-act6）与形式化规范中的定义保持一致。图3 还以图形方式展示了与漏洞相关的关键事件（特别是与重入相关的状态转移）在 Event-B 编码中是如何被维护的。该图说明了图2所示 FSM-SC 模型的结构模式是如何映射为可验证的 Event-B 事件的。

精化策略
实施了两个层次的精化。高层的合约控制流和核心不变式在抽象层次上表示。精化层次增加了合约特有的限制，包括调用栈限制、可见性限制以及重入预防条件。

算法 3：精化与证明义务的完成
输入：抽象机与精化后的机器
输出：已完成的证明义务及统计信息

1) 在 Rodin 中为抽象机生成证明义务。
2) 执行可用的自动证明器并记录证明 discharged 的结果。
3) 为精化后的机器生成精化证明义务。
4) 对精化证明义务应用自动证明器。
5) 在必要时交互式地完成剩余义务的证明。
6) 导出证明统计信息和状态报告。

证明报告包含不变量的数量、精化层级、生成的证明义务、自动解除率、交互式解除率以及最终解除率。

CTL 属性规范与模型检验
FSM-SC 抽象被转换为 SMV 模型，用于在 nuXmv 中进行分支时间时序验证。

算法 4：FSM 转换为 SMV 及 CTL 检查
输出：PASS/FAIL 验证结果及反例轨迹（如有）

1. 将有限状态机（FSM）的控制状态记录为一个枚举型 SMV 变量 state。
2. 将 FSM 状态转换转换为带有保护条件的 next(state) 赋值语句。
3. 为与漏洞相关的条件（例如外部调用和余额更新）设置标志位。
4. 在 nuXmv 中编码 CTL 属性并执行模型检测。
5. 如果某属性不成立，则生成代表 FSM 状态转换序列的反例轨迹。

CTL 检查包括重入顺序要求、在传输操作后完成状态更新、限制对临界区的无约束递归进入，以及避免死锁。

已验证的安全属性
通过不变式和 CTL 约束，确认了采用简单 DAO 风格的合约在外部调用与状态更新之间具有安全的执行顺序，从而防止重入攻击。在允许的情况下，这些保护机制检查了访问控制约束，确保未经授权的状态转移受到不变式的限制。简化的账本模型验证了交易唯一性和账本一致性这两项不变式，其验证层级位于合约内部的预防机制层面。

报告的输出
结果部分提供了关于 FSM 结构度量、Event-B 模型度量以及证明义务和 CTL 验证的统计信息。形式化证明的结果与 CTL 模型检验的结果分别给出，以区分由不变式提供的正确性保证证据，以及通过时序验证提供的时间属性验证证据。

访问受限。请登录或开始试用以查看此内容。

结果

本研究的成果结合了Event-B的形式化验证结果与CTL模型检验，并融合了来自区块链仿真的可执行信息。这些多层次输出的结合，在设计的有限示例范围内，支持对智能合约的关键行为、其共识系统以及账本健全性限制的验证。

环境设置与依赖项验证
用于模型转换、验证和仿真的执行环境已成功启动，且无依赖冲突。通过使用 Web3、NetworkX、Matplotlib、Graphviz、NumPy 和 Pandas，所有密码学、数学及区块链交互相关的软件包均已加载。如图4所示的控制台输出表明，所有必需模块在执行时均已被识别并存在。这验证了在开展验证与仿真操作前，计算环境的正确性。

验证产物度量与可扩展性指标
在 Event-B 模型的所有抽象与精化层次中，共生成了 312 个证明义务。其中，287 个通过 Rodin 内置的集成证明器自动完成证明，25 个通过交互式方式完成证明，总体证明完成率达到 10...

访问受限。请登录或开始试用以查看此内容。

讨论

形式化验证与基于仿真的验证表明，本研究所采用的多层验证系统能够在明确定义的抽象边界下验证智能合约行为、共识机制的正确性以及账本完整性属性。Event-B 以不变量和基于精化的逻辑，为安全性属性、状态流以及重入预防逻辑提供了具有数学基础的表示方法5,6。较高的证明消解率表明，所建模的系统在内部具有逻辑一致性，并符合利用形式化技术验证关键系统正确性的已知实践9,10,11,12。对权益证明（PoS）和工作量证明（PoW）的仿真也验证了系统动态在静态和事件调制情况下均保持稳定，且形式化规约与执行层面观察到的行为一致。这些结果还与先前在区块链验证方面的研究相吻合，其中形式化推理已被应用于智能合约分析、执行语义以及协议级安全属性的研究2

访问受限。请登录或开始试用以查看此内容。

披露

作者声明无任何利益冲突。

材料

本文使用的材料清单
姓名公司目录编号评论
Rodin 平台 (v3.7.0)Rodin Team / Eclipse Foundationhttps://www.event-b.org/install.htmlEvent-B 建模、精化以及证明义务的生成与验证
Event-B 方法南安普顿大学 / Rodin 社区https://www.event-b.org/用于不变式规约与系统精化的形式化建模框架
nuXmv 模型检测工具 (v2.0.0)FBK（Bruno Kessler 基金会）https://nuxmv.fbk.eu/CTL 属性的符号模型检测
Graphviz (v0.20.3)Graphviz 团队https://graphviz.org/有限状态机可视化与图形渲染
Python (v3.10.12)Python 软件基金会https://www.python.org/downloads仿真与执行环境
Web3.py (v7.6.0)以太坊基金会 / 贡献者https://web3py.readthedocs.io/区块链交互与交易仿真
NetworkX (v3.4.2)NetworkX 开发团队https://networkx.org/区块链与有限状态机结构的图建模
Matplotlib (v3.8.0)Matplotlib 开发团队https://matplotlib.org/绘制挖矿时间与验证者分布图
NumPy (v1.26.4)NumPy 开发者https://numpy.org/数值计算
Pandas (v2.2.2)Pandas 开发团队https://pandas.pydata.org/数据分析与处理
OpenJDK 11Oracle / OpenJDK 社区https://openjdk.org/projects/jdk/11/Rodin 平台所需的运行环境
Ubuntu 22.04 LTSCanonical Ltd.https://ubuntu.com/download所有实验所用的操作系统
Solidity以太坊基金会https://soliditylang.org/作为输入使用的智能合约源语言
nuXmv 输入语言 (SMV)FBKhttps://nuxmv.fbk.eu/documentation.html用于 CTL 验证的中间模型表示

参考文献

  1. Yaga, D., Mell, P., Roby, N., Scarfone, K. Blockchain Technology Overview. , National Institute of Standards and Technology. Gaithersburg, MD, USA. (2018).
  2. Wang, Y., et al. Formal specification and verification of smart contracts for Azure Blockchain. arXiv preprint. , (2019).
  3. Huth, M., Ryan, M. Logic in Computer Science: Modelling and Reasoning About Systems. , Cambridge University Press. Cambridge, U.K. (2004).
  4. Baier, C., Katoen, J. P. Principles of Model Checking. , MIT Press. Cambridge, MA, USA. (2008).
  5. Abrial, J. R. Modeling in Event-B: System and Software Engineering. , Cambridge University Press. Cambridge, U.K. (2010).
  6. Abrial, J. R., et al. Rodin: An open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12 (6), 447-466 (2010).
  7. Abrial, J. R. The B-Book: Assigning Programs to Meanings. , Cambridge University Press. Cambridge, U.K. (1996).
  8. Jacky, J. The Way of Z: Practical Programming with Formal Methods. , Cambridge University Press. Cambridge, U.K. (1996).
  9. Verma, S., Yadav, D., Chandra, G. Introduction of formal methods in blockchain consensus mechanism and its associated protocols. IEEE Access. 10, 66611-66621 (2022).
  10. Guha, S., Nag, A., Karmakar, R. Formal verification of safety-critical systems: A case study in airbag system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 107-116 (2021).
  11. Karmakar, R. Formal verification techniques: A comparative analysis for critical system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 93-102 (2022).
  12. Karmakar, R. Symbolic model checking: A comprehensive review for critical system design. Adv. Data Inf. Sci. , Springer. Singapore. 693-703 (2022).
  13. Said, M. Y., Butler, M., Snook, C. A method of refinement in UML-B. Softw. Syst. Model. 14 (4), 1557-1580 (2015).
  14. Snook, C. F., Butler, M. J. UML-B: A plug-in for the Event-B tool set. Proc. ABZ 2008: Abstract State Machines, B and Z, , Springer. 344-358 (2008).
  15. Ben Younes, A., Ben Ayed, L. From UML activity diagrams to Event-B for the specification and the verification of workflow applications. Proc. IEEE 32nd Int. Conf. Computer Software and Applications, , 643-648 (2008).
  16. Morris, K. V., Snook, C. Reconciling SCXML Statechart Representations and Event-B Lower Level Semantics. , Sandia National Laboratories. Livermore, CA, USA. (2016).
  17. Butler, M. Decomposition structures for Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. 20-38 (2009).
  18. Butler, M. Incremental design of distributed systems with Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. (2009).
  19. Le, T. C., Garriga, M., Pautasso, C., Stankovic, M. Proving conditional termination for smart contracts. Proc. ACM Workshop Blockchains, Cryptocurrencies, and Contracts, , (2018).
  20. Alt, L., et al. SMT-based verification of Solidity smart contracts. Proc. ISoLA 2018: Leveraging Applications of Formal Methods, , Springer. Cham, Switzerland. 376-388 (2018).
  21. Bhargavan, K., et al. Formal verification of smart contracts. Proc. ACM Workshop Programming Languages and Analysis for Security, , 91-96 (2016).
  22. Grishchenko, I., Maffei, M., Schneidewind, C. A semantic framework for the security analysis of Ethereum smart contracts. Formal Methods Secure Software Systems (PoST 2018), , Springer. Cham. 243-269 (2018).
  23. Nielsen, J. B., et al. Smart contract interactions in Coq. arXiv preprint. , (2019).

访问受限。请登录或开始试用以查看此内容。

重印与许可

申请许可以重复使用本 JoVE 文章的文本或图表

申请许可

标签

B

相关文章