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

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

的函数,实现了无限转账.
4.3 对比实验
实验环境为 64 位 Windows 7 系统,3.2GHz Intel(R) Core(TM) i5 处理器,32GB 内存.为了展示 SOL2M 工具
将 Solidity 程序转换为 MSVL 程序的能力,如表 12 所示挑选了 9 个典型 Solidity 程序.程序列给出了 Solidity 程
序的名称,LOC 列给出了 Solidity 程序的规模(行),LOM 列给出了从 Solidity 程序转换而来的 MSVL 程序的规
模,时间列显示了完成转换任务所花费的时间.实验结果表明:对于这些典型的 Solidity 程序,SOL2M 工具都可以
有效地转换为 MSVL 程序,生成的 MSVL 程序的规模约是 Solidity 程序的 2.25 倍.

Table 12 SOL2M 转换的实验结果
表 12 Experimental results of SOL2M conversion

程序 LOS LOM 时间(ms) 增长倍数
overflow.sol 18 72 30 4.00
votecontract.sol 29 121 69 4.17
crowdfunding.sol 41 137 91 3.34
govermental.sol 44 114 73 2.59
racecondition.sol 49 110 55 2.24
reentrancy.sol 54 132 78 2.44
safemath.sol 65 128 75 1.97
sushirestaurant.sol 110 156 256 1.42
multisigwallet.sol 118 219 124 1.86

下面通过与 Oyente 工具进行比较,来分析 UMC4M 的有效性.从以上 9 个程序中挑选 5 个进行实验,表 13
给出了验证的实验结果.程序列给出了 Solidity 程序的名称,堆栈深度攻击漏洞、交易订单依赖、时间戳依赖、
可重入漏洞列给出了验证的安全性质,每列下分别给出了 UMC4M 和 Oyente 的验证结果.√表示智能合约不存
在该安全漏洞,而×表示存在该安全漏洞.验证时间列给出了 UMC4M 和 Oyente 验证所花费的时间.实验结果表
明:UMC4M 和 Oyente 的验证结果大部分相同,但前者能发现 governmental.sol 的堆栈深度攻击漏洞和时间戳依
赖,且能发现 racecondition.sol 的交易订单依赖,后者均不能发现这些安全漏洞.另外,UMC4M 的验证时间已经包
含了 Solidity 程序到 MSVL 程序的转换时间,只占 Oyente 的 31%.
Table 13 UMC4M 与 Oyente 对比结果
表 13 Comparison results of UMC4M and Oyente
堆栈深度攻击漏洞 交易订单依赖 时间戳依赖 可重入漏洞 验证时间(ms)
程序
UMC4M Oyente UMC4M Oyente UMC4M Oyente UMC4M Oyente UMC4M Oyente
overflow.sol √ √ √ √ √ √ √ √ 811 1 158
votecontract.sol √ √ √ √ √ √ √ √ 836 6 786
governmental.sol × √ √ √ × √ √ √ 787 2 190
racecondition.sol √ √ × √ √ √ √ √ 837 888
reentrancy.sol √ √ √ √ √ √ × × 820 2 175
5 相关工作

目前,国内外学者针对智能合约安全问题给出了多种形式化验证方法,主要分为 3 类:定理证明、符号执行
以及模型检测.
Bhargavan 等人提出了智能合约验证框架 [14] 并开发了 Solidity*工具,将 Solidity 智能合约源代码转换为等
价的 F*程序,在源代码级别上来验证合约安全性.同时开发了 EVM*工具,在字节码级别上反编译 EVM 字节码,
分析字节码属性并产生等价的 F*程序,然后进行交互式证明.杨霞等人提出一种面向智能合约的高度自动化的
形式化验证系统及方法,将智能合约开发语言自动化转换为中间层语言 M+代码,然后通过形式化验证辅助器
对其进行验证.在此基础上,提出一种基于定理证明的以太坊智能合约形式化验证方法,使用辅助验证工具 Coq
与 Isabelle 分别实现对 Solidity 源代码以及以太坊智能合约字节码的形式化验证 [15] .一方面,在 Coq 工具中建立
源代码的形式化模型;另一方面,基于形式化操作码集在 Isabelle 中建立智能合约字节码的形式化模型,之后对