软件学报

作者：王小兵，常家俊，李春奕，杨潇钰，赵亮

单位：王小兵，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007111,常家俊，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007102,李春奕，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007103,杨潇钰，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007104,赵亮，西安电子科技大学 计算机科学与技术学院, 陕西 西安 71007105

关键词：智能合约;Solidity;程序转换;操作语义;等价性证明

基金：陕西省重点研发计划(2023-YBGY-229); 西安市科技计划(22GXFW0025)

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

来源：2025年第9期

《软件学报》期刊编辑部

查看软件学报杂志2025年第9期