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

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

[1]
2008 年,Satoshi Nakamoto 首次提出了区块和链的概念 ,指出了当前的线上交易几乎都需要依赖可信第三
方,这增加了交易成本且扩大了不必要的交易规模.因此,中本聪提出了一种点对点的数字货币交易系统,也就
是比特币系统,这也标志着区块链时代的到来.区块链本质上是分布式的数据账本,使用了加密算法、共识机制
等技术,保证了用户的隐私且在交易期间不再依赖可信第三方的支持.早在 1994 年,Nick Szabo 就提出了智能合
[2]
约的概念 ,并将其定义为可以自动执行复杂业务操作的数字合约.但由于无法保证在没有第三方介入的情况
下正确执行合约条款,因此智能合约一直没有在实际中应用,直到区块链的出现.区块链所具备的去中心化、公
开共享、可信性、集体维护以及不可篡改的特质,使其成为智能合约天然的执行平台.
[3]
目前,智能合约已在许多区块链系统上成功实现,比较著名的系统有以太坊(Ethereum) 和超级账本
[4]
(hyperledger) .以太坊在 2013 年由俄罗斯学者 Vitalik Buterin 所推出的《以太坊:下一代智能合约和去中心化
[5]
应用平台》 中被首次提出,是目前最大的区块链平台.在以太坊中,大多数智能合约程序由图灵完备语言
[6]
Solidity 编写 ,然后编译为以太坊虚拟机(Ethereum virtual machine,简称 EVM)的字节码,并运行在 EVM 之上.
随着区块链技术的出现和发展,智能合约已经被应用于医疗(如存储电子病历和基因数据)、金融(如 P2P 网络借
[7]
[8]
贷)、资产管理等领域,但其安全性问题却层出不穷 .2016 年,攻击者利用 The Dao 智能合约的脚本代码漏洞 ,
从中窃取了 300 多万以太币.2018 年,BEC 智能合约出现重大漏洞,攻击者利用批量转账函数中的整数溢出问题
无限生成代币,造成了约 60 亿人民币的损失.
在实际应用中,智能合约涉及了大量用户的数字财产,一旦出现漏洞,就会造成无法挽回的损失.因此,在智
能合约被部署到区块链平台之前,需要对其进行漏洞排查.传统的测试方法不能达到保证智能合约正确性和高
可靠性的需求,国内外许多学者提出了使用形式化方法对智能合约进行验证的方式,主要包括定理证明、符号
执行以及模型检测这 3 种.
本文提出一种基于时序逻辑语言(modeling, simulation and verification language,简称 MSVL)的智能合约安
全性的模型检测方法:首先,使用 MSVL 对智能合约程序进行建模,为了减少建模时大量的人工操作,开发了将
智能合约语言 Solidity 转换为 MSVL 的转换器工具 SOL2M,实现了智能合约建模程序的自动化生成;然后,使用
命题投影时序逻辑(propositional projection temporal logic,简称 PPTL)公式描述该智能合约的安全性性质;最后,
在统一模型检测器(unified model checker for MSVL,简称 UMC4M)中自动化验证建模程序是否满足给定的安
全性性质,并通过实例说明该方法运用到智能合约验证中的可行性和实用性.
本文第 1 节将回顾 MSVL 与 PPTL 相关理论.第 2 节将介绍 Solidity 语言特性以及智能合约的安全问题.
第 3 节将给出 SOL2M 转换器的研究与实现.第 4 节将给出使用 MSVL 对智能合约建模和验证的应用实例.第 5
节将给出相关工作.第 6 节将给出总结及展望.

1 MSVL 与 PPTL

1.1 MSVL
[9]
MSVL 的初始版本是 Framed Tempura ,在引入了等待语句和非确定选择语句之后,得到了建模、仿真与验
证语言 MSVL.MSVL 是投影时序逻辑(projection temporal logic,简称 PTL)的可执行子集,具有与高级程序设计
语言类似的语法.下面介绍 MSVL 的基本语句.
(1) 区间长度语句:empty,skip,len(n);
(2) 区间框架语句:frame(x);
(3) 并行语句:p||q;
(4) 顺序语句:p;q;
(5) 非确定选择语句:p or q;
(6) 合取语句:p and q;
(7) 等待语句:await(b);
(8) 立即赋值语句:x<=e;