面向MSVL的智能合约形式化验证

作者：王小兵; 杨潇钰; 舒新峰; 赵亮^*

来源：软件学报, 2021, 32(06): 1849-1866.

DOI：10.13328/j.cnki.jos.006253

• 区块链
• 智能合约
• 形式化方法
• MSVL

智能合约是运行在区块链上的计算机协议,被广泛应用在各个领域中,但是其安全问题层出不穷,因此在智能合约部署到区块链上之前,需要对其进行安全审计.然而,传统的测试方法无法保证智能合约所需的高可靠性和正确性.说明了如何使用建模、仿真与验证语言(MSVL)和命题投影时序逻辑(PPTL)对智能合约进行建模和验证:首先介绍了MSVL与PPTL的理论基础;之后,通过分析和对比Solidity与MSVL语言的特性,开发了能够将Solidity程序转换为MSVL程序的SOL2M转换器,并详细介绍了SOL2M转换器的设计思路;最终,通过投票智能合约和银行转账智能合约两个实例,给出了SOL2M转换器的执行结果.使用PPTL从功能一致性、逻辑正确性以及合约完备性这3个方面描述了合约的性质,给出了使用统一模型检测器(UMC4M)对合约进行验证的过程.

• 单位
  西安电子科技大学; 西安邮电大学