Page 120 - 《软件学报》2025年第9期

王小兵 等: Solidity 到 MSVL 转换的等价性研究 4031

4 相关工作

目前, 国内外学者针对智能合约操作语义的研究主要分为两种, 分别是对于 EVM 操作语义的研究和对于
Solidity 操作语义的研究.
2018 年, Zakrzewski [20] 提出了 Solidity 子集的形式化规范, 给出了 Solidity 的核心数据模型和函数修饰符等特
殊功能的形式化规范, 对 Solidity 的形式化更注重于动态语义, 采用的是一元函数大步语义 (big-step semantics). 提
供了对于 Solidity 语言特性的准确描述和一些核心结构的动态语义, 所提出的语义在 Coq 中以可执行的形式
给出.
2019 年, Yang 等人 [25] 提出了一种定义在 Coq 中的 Solidity 子集的形式语义, 称为 Lolisa. 首先将 Solidity 程序
翻译成 Lolisa, 使用词法分析器对智能合约进行分析, 生成 Solidity token 流, 并根据 Lolisa 的语法糖, 词法分析器
生成相应的 Lolisa token 流. 之后将 Solidity token 流作为解析器参数, 生成智能合约的语法树. 然后将 Lolisa 的
token 流作为语法树的 token, 通过语法分析器重建 Lolisa 语法树, 并输出由 Lolisa 重写的形式智能合约. 此外
Yang 等人 [26] 还为 Lolisa 在 Coq 中实现了一个经过正式验证的解释器, 称为 FEther, FEther 严格遵循基于 GERM
框架的 Lolisa 的形式语法和语义, 保证了智能合约与其正式模型之间的一致性. FEther 是以太坊第一个支持 Coq
混合验证技术的证明引擎, 将符号执行与高阶逻辑定理证明相结合, 包含一组专有的自动策略, 以高度自动化的方
式执行和验证 Coq 中的智能合约.
2020 年, Jiao 等人 [27,28] 为 Solidity 开发了一种结构化操作语义 (structural operational semantics, SOS). 在
Solidity 类型、表达式和语句的规则之下, 抽象出了 K 框架 [29] 中 Solidity 的可执行语义, 能够涵盖官方 Solidity 文
档所指定的大部分语义. 重点在于 Solidity 存储 (storage) 和内存 (memory) 访问的语义计算上, 并在 K 框架中实现
了所提出的结构化操作语义, 提供了一个可达性逻辑证明. 此外, 以 DAO 攻击的 4 种变体为实例, 模拟了其在区
块链中的行为, 结果表明生成的 Solidity 语义是可执行的, 并且可以通过可执行语义检测到智能合约中的一些漏
洞, 有助于验证智能合约中的安全属性.
2020 年, Velasco [21] 提出了一种可以在 Maude 中实现的 Solidity 语义. 基于大步语义给出了 Solidity 的高级语
义定义, 在一定程度上参考了“Executable operational semantics of Solidity” [27] , 重点关注 Solidity 的内存模型, 给出
了详细的语法规则. 给出一个初始规则, 作为其余所有规则的起始点, 当智能合约部署到区块链时会分配一个新地
址, 同时得到一个初始状态实例 σ. 依据规则从初始状态 σ 开始执行, 之后给出了访问和更新 Solidity 存储
(storage)、表达式、基本语句、变量声明和函数调用的操作语义.
2021 年, Marmsoler 等人 [30] 提出了一个在 Isabelle/HOL 中可执行的 Solidity 语义, 这种形式化语义为 Solidity
程序建立了交互式程序验证环境的基础, 并允许通过符号执行来检查 Solidity 程序. 该方法首先在 Isabelle/HOL 中
为 Solidity 子集提供了可执行的表示性语义, 然后提出了基于语法的模糊框架, 可以自动验证以太坊区块链的正
式语义, 其次使用 Isabelle 的代码生成器从所提出的形式化语义自动生成 Solidity 求值器, 并使用 Haskell 作为代
码生成器的目标平台, 为 Solidity 程序构建集成的验证和符号执行环境, 并展示了对常数折叠和内存优化两个例
子的形式化验证.
2016 年, Luu 等人 [31] 提出了一种用于 EVM 字节码的静态分析工具, 它依赖于符号执行对智能合约的安全性
漏洞进行检测. 静态分析方法的优势是为可以静态确认的合约属性实现完全自动化. Oyente 忽略了与智能合约调
用和创建相关的几个重要命令, 提供了简化的 EVM 字节码语义. Oyente 是使用 Python 进行开发的符号执行引擎,
支持大多数 EVM 操作码, 将智能合约字节码反编译成控制流图, 并执行控制流分析, 使用 Z3 作为求解器来评估
其满足性. Oyente 支持检测多个常见的智能合约安全漏洞, 如交易顺序依赖漏洞、时间戳依赖、异常障碍和重入
漏洞. 从区块链中收集了 19 366 份智能合约作为实例, 验证了 Oyente 工具的可行性, 并对其准确率和误判率进行
了统计分析. 作为 Solidity 安全性验证的开源工具, Oyente 工具增加了以太坊开发者创建安全可靠的分散式应用
程序的能力, 也为其他研究人员奠定了理论基础.