一种代币智能合约的形式化建模与验证方法

欧阳恒一,熊 焰,黄文超

(中国科学技术大学 a.网络空间安全学院; b.计算机科学与技术学院,合肥 230026)

0 概述

智能合约是一种无需中介、自我验证、自动执行合约条款的计算机交易协议,近年来随着区块链技术的日益普及而备受关注。区块链技术去中心化和数据防篡改等特性,解决了智能合约的信任问题,因此使得智能合约更适合在区块链上进行实现。智能合约[1-3]作为一种能自动执行合约条款的计算机程序,需要尽量避免语法和语义错误,并且对于正确性及其他属性具有较高要求,以保证用户的财产安全。由于现有通过专家审计和人工复查生成可信合约代码的方法很难确保代码的绝对安全,因此导致智能合约存在安全隐患。2016年,恶意攻击者通过以太坊Solidity[4]语言中的递归调用漏洞对运行在以太坊公有链上的The DAO[2-3]智能合约进行攻击,导致360万以太币被盗。2017年,以太坊Parity电子钱包因多重签名漏洞导致数亿美元资金遭到冻结[5]。2018年,黑客利用ERC-20标准代币合约整数溢出漏洞攻击了美链BEC的智能合约,导致BEC货币急剧贬值,价值几乎归零。同年,BAI和EDU智能合约出现重大漏洞,其代币(token)可被随意转走。可见,智能合约已成为区块链应用安全的重灾区,但是到目前为止能够对智能合约漏洞进行完备性和安全性分析的方法仍未被提出,当前对于智能合约的安全保障主要依靠专家审计和人工复查,然而该方式不能保证代码的绝对安全。

形式化方法[6]的本质是基于数学的方法来描述目标软件系统属性的一种技术,适用于计算机软硬件系统的规范、开发和验证。……