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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(9):4006−4035 [doi: 10.13328/j.cnki.jos.007222] [CSTR: 32375.14.jos.007222] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
Solidity 到 MSVL 转换的等价性研究

王小兵, 常家俊, 李春奕, 杨潇钰, 赵 亮

(西安电子科技大学 计算机科学与技术学院, 陕西 西安 710071)
通信作者: 赵亮, E-mail: lzhao@xidian.edu.cn

摘 要: 智能合约是运行在以太坊区块链上的脚本, 能够处理复杂的业务逻辑. 大多数的智能合约采用 Solidity 语
言开发. 近年来智能合约的安全问题日益突出, 为此提出了一种采用时序逻辑程序设计语言 (MSVL) 与命题投影
时序逻辑 (PPTL) 的智能合约形式化验证方法, 开发了 SOL2M 转换器, 实现了 Solidity 程序到 MSVL 程序的半自
动化建模, 但是缺乏对 Solidity 与 MSVL 操作语义等价性的证明. 首先采用大步语义的形式, 从语义元素、求值规
则、表达式以及语句这 4 个层次详细定义了 Solidity 的操作语义. 其次给出了 Solidity 与 MSVL 的状态、表达式
和语句之间的等价关系, 并基于 Solidity 与 MSVL 的操作语义, 使用结构归纳法对表达式操作语义进行等价证明,
同时使用规则归纳法对语句操作语义进行等价证明.
关键词: 智能合约; Solidity; 程序转换; 操作语义; 等价性证明
中图法分类号: TP311

中文引用格式: 王小兵, 常家俊, 李春奕, 杨潇钰, 赵亮. Solidity到MSVL转换的等价性研究. 软件学报, 2025, 36(9): 4006–4035. http://
www.jos.org.cn/1000-9825/7222.htm
英文引用格式: Wang XB, Chang JJ, Li CY, Yang XY, Zhao L. Research on Equivalence of Solidity to MSVL Conversion. Ruan Jian
Xue Bao/Journal of Software, 2025, 36(9): 4006–4035 (in Chinese). http://www.jos.org.cn/1000-9825/7222.htm
Research on Equivalence of Solidity to MSVL Conversion

WANG Xiao-Bing, CHANG Jia-Jun, LI Chun-Yi, YANG Xiao-Yu, ZHAO Liang
(School of Computer Science and Technology, Xidian University, Xi’an 710071, China)
Abstract: Smart contracts are scripts running on the Ethereum blockchain capable of handling intricate business logic with most written in
the Solidity. As security concerns surrounding smart contracts intensify, a formal verification method employing the modeling, simulation,
and verification language (MSVL) alongside propositional projection temporal logic (PPTL) is proposed. A SOL2M converter is developed,
facilitating semi-automatic modeling from the Solidity to MSVL programs. However, the proof of operational semantic equivalence of
Solidity and MSVL is lacking. This study initially defines Solidity’s operational semantics using big-step semantics across four levels:
semantic elements, evaluation rules, expressions, and statements. Subsequently, it establishes equivalence relations between states,
expressions, and statements in Solidity and MSVL. In addition, leveraging the operational semantics of both languages, it employs
structural induction to prove expression equivalence and rule induction to establish statement equivalence.
Key words: smart contract; Solidity; program conversion; operational semantics; equivalence proof
[1]
2008 年, 比特币概念首次在中本聪的文章《比特币: 一种点对点的电子现金系统》 中被提出, 中本聪认为互
联网上的交易几乎完全依赖于可信任的第三方 (如金融机构) 来处理电子支付问题, 由于第三方机构不可避免需
要调解纠纷, 这导致在交易过程中成本上升, 因此他提出了一种基于加密证明的无需可信第三方的电子交易系统,
该交易系统中使用的货币就是比特币. 2009 年比特币正式上线, 比特币是第一个实现去中心化和去信任的数字货
币, 逐渐被多个大型商务网站作为支付方式之一 [2] , 同时区块链 1.0 也随之诞生, 作为区块链技术的初级版本, 区块

* 基金项目: 陕西省重点研发计划 (2023-YBGY-229); 西安市科技计划 (22GXFW0025)
收稿时间: 2023-09-21; 修改时间: 2024-01-18, 2024-04-02; 采用时间: 2024-05-10; jos 在线出版时间: 2024-07-03
CNKI 网络首发时间: 2024-07-08