Page 121 - 《软件学报》2025年第9期
P. 121
4032 软件学报 2025 年第 36 卷第 9 期
2017 年, Hildenbrandt 等人 [32] 提出了 EVM 的第 1 个完全可执行的正式语义, 称为 KEVM, 是在 K 框架 [27]
中定义的正式严格的可执行语义. 抽象了区块链系统本身的一些细节, 使用所定义的语义自动生成了正式派生的
EVM 解释器, 可以在合理的执行时间内运行完整的以太坊虚拟机测试套件, 并通过了 40 689 个 EVM 合规性测试
套件, 展示了解释器良好的性能. 为 EVM 提出了语义优先的形式化验证方法, 使用了为 K 框架开发的可达性逻辑
证明程序 [33] , 该证明程序以一个 K 定义和一组逻辑可达性声明作为输入来验证, 验证者在假设语义的情况下, 自
动证明语言执行空间上的可达性定理. 文献 [32] 给出了两个实例的完整验证, 第 1 个实例验证了合约中算术操作
的实际重要属性, 所验证的属性包含 EVM 源程序的功能正确性和 gas 复杂性, 第 2 个实例以以太坊生态系统中被
广泛使用的令牌标准 ERC20 的传递函数为例, 验证其正确操作, 通过两个实例证明了该方法的可行性.
2018 年, Grishchenko 等人 [34] 提出了一种 EVM 字节码的完整小步语义 (small-step semantics), 该语义在 Luu
等人 [31] 提出的字节码的基础上, 做了大量修改, 处理了部分缺失的指令, 例如合约调用和调用创建, 并正式定义了
智能合约的一些核心安全属性, 例如调用完整性、原子性和独立于矿工控制的参数. 文献 [34] 将提出的语义在 F*
中形式化, F*针对程序验证进行了优化, 并允许利用 SMT 求解器执行手动证明和自动证明. 在 F*中的形式化严格
遵循了提出的小步语义, 最终通过将 F*编译为 OCaml, 使用官方以太坊测试套件验证了所提出的可执行语义. 在
F*中的形式化公开可用, 促进了 EVM 字节码静态分析技术的设计及其稳健性证明.
2018 年, Amani 等人 [35] 在字节码级别上扩展了 Isabelle/HOL 中现有的 EVM 形式化, 该方法以非结构化字节
码为目标, 独立于高级编程语言 (如 Solidity), 一方面减少对高级工具正确性的依赖, 另一方面字节码是以太坊实
际编程语言, 区块链上的所有智能合约均基于该语言. 该方法首先扩展了 Isabelle/HOL 定理证明中的 EVM 形式
化, 涵盖了智能合约的正确属性, 其次给出了健全的程序逻辑, 能够在字节码级别验证智能合约, 之后提供了
Isabelle 策略, 以支持使用逻辑规则自动生成验证条件, 最后以托管协议智能合约为例, 生成了相应的 EVM 字节
码, 并使用所提出的程序逻辑验证了 EVM 字节码的功能正确性, 证明了该方法的可行性和适用性.
综上所述, 目前对于智能合约语义的研究工作集中在以太坊字节码语义和 Solidity 高级语义上, 文献 [31,34,35]
重点研究的是 EVM 操作语义, 这为 Solidity 高级语言操作语义的定义提供了参考价值. Solidity 操作语义的定义
与其应用的形式化方法息息相关, 文献 [20,21,25–28,30] 对 Solidity 语言的操作语义进行了研究, 其中文献 [25–28,30]
重点关注 Solidity 语言的可执行语义, 其目的是能够在 K 框架、Coq 或 Isabelle/HOL 中执行语义并对智能合约进
行形式化验证.
5 总结与展望
为了更好地对智能合约进行安全验证, 之前的工作基于 MSVL 与 PPTL 对智能合约进行形式化验证 [12,13] , 开
发了 SOL2M 转换器, 实现了对 Solidity 程序的半自动化建模, 进而使用 UMC4M 实现了 Solidity 的可重入漏洞检
测. 该转换器在制定转换规则时重点关注 Solidity 与 MSVL 的词法及语法. 本文从数学角度出发, 制定基于大步语
义风格的 Solidity 子集的操作语义, 并从 MSVL 和 Solidity 的操作语义出发, 使用结构归纳法以及规则归纳法证明
两者操作语义的等价性, 建立形式化语言和 Solidity 之间基于语义的映射关系, 为基于形式化方法的智能合约安
全验证奠定理论基础. 目前定义的操作语义只针对 Solidity 的一个子集, 囊括了主要语法但仍存在未定义的结构,
如 require 语句等, 后续将进一步扩充该子集. 同时, 随着 Solidity 的版本迭代, 需要根据新特性语句的开始与结束
状态变化, 不断完善其操作语义及等价性证明. 本文研究工作为 SOL2M 转换器提供了严格的数学依据, 从操作语
义等价的角度为基于 MSVL 的智能合约形式化验证提供了理论基础, 据此可对 SOL2M 转换器进行持续的优化和
扩展. 进一步, 随着 Solidity 操作语义与等价性证明的不断扩展, 将对更多版本的 Solidity 智能合约进行研究, 并将
该方法应用到基于其他语言的智能合约验证.
References:
[1] Nakamoto S. Bitcoin: A peer-to-peer electronic cash system. 2008. https://bitcoin.org/bitcoin.pdf

