Page 284 - 《软件学报》2021年第6期

1858 Journal of Software 软件学报 Vol.32, No.6, June 2021

的转换规则将 Solidity 代码转换为与其功能等价的 MSVL 代
读取Solidity源程序
码;转换后的 MSVL 代码被暂存在预先创建的 Java 集合对象
提取Solidity程序的语义信息 中,待语法分析结束后,遍历暂存集合并写入到 MSVL 程序文
语
义 Solidity代码转换为MSVL代码 件(msvl.m)中.设 m 表示 Solidity 程序中变量声明的数量,n 表
分 示语句数,p 表示每条语句中包含表达式的平均数,不难证
析
MSVL代码暂存到集合容器中 明,SOL2M 转换流程的时间复杂度是 O(n×p+m).通常,Solidity
程序中一条语句的表达式数量、变量声明数量均不会超过一
遍历暂存集合输出到MSVL文件 个常数,因此,SOL2M 转换流程的时间复杂度为 O(n).UMC4M
Fig.10 Basic flow of program conversion 验证 MSVL 程序基于 PPTL 的判定算法 [10] :设 PPTL 公式的长
图 10 程序转换的基本流程 度为 l,包含的命题组成集合ϕ,则该算法的时间复杂度为
|ϕ|
O(l×2 ).
4 实例验证

本文使用 SOL2M 转换器对智能合约进行自动化建
模,并提出了一种面向 MSVL 和 PPTL 的形式化验证方 智 UMC4M
能 1. 模型 MSVL程序 m文件
法.MSVL 是 PTL 的可执行子集,PPTL 是 PTL 的可判定 合
开始 约 2. 性质 exe文件
子集,因此可以将 MSVL 与 PPTL 统一在 PTL 的框架中 源 PPTL公式 p文件
程 ...
进行自动验证.验证流程如图 11 所示,具体为:使用 MSVL 序
对智能合约进行自动建模,存放在 m 文件中;使用 PPTL 否 4. 排查 是 执行exe
描述智能合约待验证性质并存放在 p 文件中;将建模程 结束 是 满足? 否 报错? 3. 验证
序与待验证性质输入统一模型检测器 UMC4M 进行验
Fig.11 Basic flow of program conversion
证;若智能合约模型出错,则对 m 文件进行修改;若是待验
图 11 程序转换的基本流程
证性质出错,则对 p 文件进行修改;若验证成功,UMC4M
检测器会给出模型是否满足性质的结果,或给出反例以便排查智能合约漏洞.
本节将通过两个具体智能合约实例,使用 SOL2M 转换器对合约进行建模,使用 PPTL 公式描述合约需要满
足的性质,最后在 UMC4M 统一模型检测器中完成验证.
4.1 投票智能合约的建模与验证
本小节以投票智能合约为例,给出 SOL2M 对其进行建模的详细流程以及验证过程.如图 12 所示,该投票协
议主要包括状态变量、结构体和函数这 3 部分.合约名称为 voteContract,合约内部首先声明了候选者 Candidate
结构体,包含候选者名称与所获票数两个成员变量;其次创建了一个从候选者到票数的映射类型,以及使用结构
体类型的数组 Candidate[ ]来存储所有候选者;合约内还声明了两个函数——vote( )函数实现了为特定候选者
投票的功能,winner( )函数从所有候选者中选择出票数最高的获胜者.
首先对投票智能合约进行建模,将投票智能合约作为 SOL2M 转换器的输入被自动存入 solidity.sol 文件中,
如图 13 所示,将 Solidity 代码转换为 MSVL 代码,结果存放在 msvl.m 文件中.建模之后,使用 PPTL 描述投票智
能合约的性质,PPTL 公式中常用的时序操作符见表 5.本文将智能合约的性质归纳为 3 个层面:功能一致性、逻
辑正确性以及合约完备性.下面从这 3 个方面描述投票智能合约应该满足的性质.
(1) 功能一致性.
每一个智能合约应满足的基本要求,是指智能合约的函数功能与合约设计要求之间的一致性,即待验证合
约的功能应当符合实际要求.对于投票智能合约来说,其 winner 函数需要从所有候选者中选择出票数最高的赢
家,若最终存在比赢家的票数更高的候选者,则说明 winner 函数没有实现实际要求,即不满足功能一致性.因此,
描述性质 1 为:投票结束后,不存在比赢家票数更高的候选者.从原子命题、命题逻辑与时序逻辑这 3 个方面对
性质 1 进行描述见表 6,最终使用 PPTL 公式描述性质 1 为 fin(!m).