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