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

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

链 1.0 能够验证交易过程中的合理性而无需再依赖第三方机构的监督. 比特币自 2009 年以来的成功刺激了其他
基于区块链应用程序的发展, Buterin 在 2013 年提出了以太坊 [3] 区块链平台, 标志着区块链进入 2.0 时代, 以太坊
作为分布式计算平台 [4] , 用户可以在其中创建和执行高级脚本, 这些脚本被称为智能合约 [5] , 它们运行在以太坊虚
拟机 (Ethereum virtual machine, EVM) 上, 智能合约 [6] 大多是基于 Solidity 编写的计算机程序, 可自动执行或强制
执行其合同条款 [7] .
由于智能合约具有去中心化、去信任等特殊性质, 不同于使用其他编程语言 (例如 C/Java), 如果对底层语义
模型理解有误, 编写程序时容易产生安全漏洞, 且 Solidity 语言的多种设计 (例如 fallback 回退函数) 进一步恶化了
这种情况. 近年来智能合约的安全问题日益突出, 并且通常管理价值数百万美元的数字资产, 因此其中的安全漏洞
会导致巨大的损失. 一个著名的智能合约安全问题是 DAO 攻击 [8] , 攻击者利用了 DAO 合约中与回退函数和重入
属性相关的漏洞 [9] 非法获得了 6 000 万美元. 此外, 由于区块链的特点, 智能合约一旦部署就不能被篡改, 因此在将
智能合约部署到区块链之前对其进行验证显得非常重要.
对智能合约安全分析方法主要有 5 种, 包括形式化验证法、符号执行法、模糊检测法、中间表示法和深度学
习法 [10] , 其中形式化验证法是通过形式化语言, 把合约中的概念、判断、推理转化成形式化模型, 从而消除合约
中的歧义性和不通用性, 配合严谨的逻辑和证明, 验证智能合约函数功能的正确性和安全性. 目前有学者采用形式
化方法对面向合同的智能合约进行形式化定义, 进而消除智能合约与商务合同之间的歧义 [11] . 但这些方法存在一
种问题: 如何保证形式化模型与智能合约之间的等价性.
在以往的工作中, 基于 MSVL (modeling, simulation and verification language) 与 PPTL (propositional projection
temporal logic) 进行了智能合约的形式化验证工作 [12,13] , 开发了自动化建模工具 SOL2M 将 Solidity 程序转换为
MSVL 程序, 并在 UMC4M [14] 中进行验证, 实现了对 Solidity 可重入漏洞的检测. 不过该工作缺乏对 Solidity 语义
以及 Solidity 与 MSVL 语义等价性的研究. 因此, 本文研究了 Solidity 的语法, 定义了 Solidity 表达式及语句的操
作语义, 并基于 Solidity 与 MSVL 的操作语义, 证明了 Solidity 程序与转换后的 MSVL 程序之间的等价性, 为基于
MSVL 的验证提供理论基础, 保证了建模过程的可信性和可验证性. 通过建立形式化语言和 Solidity 之间基于语
义的严格映射关系, 也为基于形式化方法的智能合约安全验证奠定了更形式化的理论基础.
本文提出了一种基于大步语义的 Solidity 子集的操作语义, 并给出了其与 MSVL 操作语义的等价性证明. 首
先分析 Solidity 语言的语法结构, 给出了语义元素与求值规则的定义, 进一步给出了表达式与语句的操作语义定
义. 然后, 定义了 Solidity 与 MSVL 的状态、表达式和语句之间的等价关系, 并通过结构归纳法证明了表达式操作
语义的等价性, 进一步通过规则归纳法证明了语句操作语义的等价性.
本文第 1 节将回顾 MSVL 语法与操作语义. 第 2 节在回顾 Solidity 语法基础上给出 Solidity 语言特性以及操
作语义. 第 3 节基于 SOL2M 的转换规则给出 Solidity 与 MSVL 操作语义的等价性证明. 第 4 节给出相关工作, 第
5 节是总结及展望.
1 MSVL 语法与操作语义

MSVL 是一种时序逻辑程序设计语言, 初始版本是 Framed Tempura [15] , 在引入了等待语句和非确定选择语句
之后, 得到了建模、仿真与验证语言. MSVL 是投影时序逻辑 (projection temporal logic, PTL) 的可执行子集, 具有
与高级程序设计语言类似的语法. MSVL 操作语义借鉴于文献 [16−18].

1.1 MSVL 语法
MSVL 的语法类似 C 语言, 除了顺序语句、循环语句等基本语句外, 还加入了时序操作和投影相关语句, 相
较 PTL 对软硬件系统有了更强的表达能力. 与其他高级编程语言一样, MSVL 提供了各种数据类型, 包含了无符
号字符 (char)、无符号整数 (int)、和浮点数 (float), 此外还定义了数组 (array)、结构体 (struct)、指针 (pointer) 等.
详情见文献 [19]. MSVL 的表达式归纳定义如下: