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

王小兵 等:面向 MSVL 的智能合约形式化验证 1865

合约中的安全属性进行定理证明,验证其可满足性.以上方法属于定理证明,需要一定的人工证明,验证效率受
到一定影响.
Luu 等人提出一种基于符号执行的智能合约安全性漏洞检测方法 [16] ,开发了符号执行工具 Oyente,并非针
对智能合约语句 Solidity,而是直接将 EVM 字节码和当前以太坊的全局状态输入工具,使用 Z3 求解器来判定可
满足性.Oyente 能够在合约部署前检测其漏洞,该方法属于符号执行,一般只考虑符号路径的可满足性,自动化
程度较高.当合约中的判断条件较多时,符号执行路径数量就会呈现指数级增长,且符号执行过度依赖约束求解
器的求解能力,从而影响验证效率.
Kalra 等人开发了一种基于抽象解释和符号模型检测智能合约安全性的工具 ZEUS [17] ,其中包含一个能够
将合约源代码转换为 LLVM 位码的代码转换器,同时也能够将 XACML 格式的待验证性质转换为 LLVM 位码.
最后,将与合约及其性质等价的 LLVM 程序作为输入,使用 CHCs 工具进行了符号模型检测.胡凯等人提出了通
过 Promela 建模语言结合 SPIN 工具对智能合约安全性进行验证的方法 [18] ,使用 Promela 对智能合约进行建模,
使用 LTL 描述待验证性质,在 SPIN 中自动化验证模型是否满足所期待的性质,最终给出代码是否与需求一致的
结论.以上方法属于模型检测,由于自动化程度较高,因此能够很好地避免验证成本较大和效率低下的问题.
K框架是一个语言无关、基于可达性的逻辑验证框架,KEVM 使用 K 框架来描述智能合约的形式化语义 [19] ,
并实现了语义分析工具,例如 Gas 分析工具、语义调试器、程序验证器等.KEVM 较难实现完整的程序分析,且
需要投入较多的人力.本文采用基于 MSVL 的智能合约安全性的模型检测方法,性质描述采用的时序逻辑 PPTL
具有完全正则表达能力,严格强于 LTL.验证过程由模型检测器 UMC4M 自动完成,当状态空间过大时会产生状
态空间爆炸问题 [20] .但是智能合约一般并非大型软件系统,因此该方法能够降低验证成本并提高验证效率.

6 总结与展望

为了更好地在智能合约部署之前对其进行安全验证,本文提出了面向 MSVL 与 PPTL 对智能合约进行安全
性验证的模型检测方法,开发了 SOL2M 转换器,用于将智能合约 Solidity 程序转换为 MSVL 程序,即实现了对智
能合约的自动化建模.使用 PPTL 公式从功能一致性、逻辑正确性以及合约完备性这 3 个方面描述了智能合约
模型的性质.通过投票智能合约与银行转账智能合约两个实例来说明方法的可行性.目前阶段的转换是 Solidity
语言的子集,因此仍需继续对 SOL2M 转换器进行扩展和完善.另外,本文所给出的转换规则是基于两个语言的
词法规则和语法规则所制定,将来的研究工作包括从数学角度证明 Solidity 与 MSVL 在表达式和基本语句上的
语义等价性.

References:
[1] Nakamoto S. Bitcoin: A Peer-to-Peer Electronic Cash System. White Paper, 2008.
[2] Szabo N. Formalizing and securing relationships on public networks. First Monday, 1997,2(9).
[3] Wood G. Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper, 2014,151(2014):1−32.
[4] Androulaki E, Barger A, Bortnikov V, Cachin C, Christidis K, De Caro A, Enyeart D, Ferris C, Laventman G, Manevich Y.
Hyperledger fabric: A distributed operating system for permissioned blockchains. In: Proc. of the 13th EuroSys Conf. 2018. 1−15.
[5] Halstead MH. Elements of Software Science. New York: Elsevier Science Inc, 1977.
[6] Dannen C. Introducing Ethereum and Solidity. Berkeley: Apress, 2017.
[7] Bartoletti M, Pompianu L. An empirical analysis of smart contracts: Platforms, applications, and design patterns. In: Proc. of the
Int’l Conf. on Financial Cryptography and Data Security. 2017. 494−509.
[8] Mehar MI, Shier C, Giambattista A, Gong E, Fletcher G, Sanayhie R, Kim HM, Laskowski M. Understanding a revolutionary and
flawed grand experiment in blockchain: The DAO attack. Journal of Cases on Information Technology (JCIT), 2019,21(1):19−32.
[9] Ma YT, Duan ZH, Wang XB, Yang XX. An interpreter for framed tempura and its application. In: Proc. of the 1st Joint IEEE/IFIP
Symp. on Theoretical Aspects of Software Engineering. Shanghai: IEEE Press, 2007. 251−260.
[10] Shu XF, Zhang N, Wang XB, Zhao L. Efficient decision procedure for propositional projection temporal logic. Theoretical
Computer Science, 2020,838:1−16.